I support the sentiment expressed in your email. +1 Type systems are nice, just don't force them upon anyone. Keep the C++ at bay.
--
Please do not email me anything that you are not comfortable also sharing with
the NSA.
On Oct 6, 2013, at 7:16 AM, Chris Zheng <z...@caudate.me> wrote:
> Thanks Mike for your reminder to be pragmatic. It is definitely the way to
> go. Clojure's an incredible language for this.
>
> This is going to be a longish post as I should better explain my position. It
> is just a brief sketch of the problem but I think that we should be thinking
> about it more as a fun exercise rather than a way to troll the
> haskell/scala/ml mailing lists.
>
> I'm not the type of person to get overly academic but I still want to have
> `faith` in the tools that I'm using. In Indian traditions of philosophy, the
> term `shraddah` is translated as `faith` but it literally means `that which
> binds you` or `that which is unwavering`. Logical foundations of practices
> and beliefs are debated by practitioners and scholars alike. To debate and
> win against those in opposition, one has to have a good reason to believe in
> their practice. In other words, academics is a VERY powerful tool for faith.
>
> Because of the vast amounts of academic work around types, we now have a
> `type` priesthood and an increasingly mass of `type converts` who are very
> inflammatory against anything non-typed languages. The cult of haskell will
> always look down on the cult of lisp/javascript/python/ruby, laugh and say
> `you guys suck because you don`t have A, B, C which are features of type
> inference`.
>
> Now with the `cult of clojure`, we can say YES WE DO (Typed Clojure)… but not
> only that, we should also be able to say:
>
> "Because we have optional typing, here are a bunch of problems that we can
> solve very easy because X, Y and Z are not restricted by type inference."
>
> Now The the debate actually moves forward, so that we ask ourselves whether
> type-inference is suitable for solving a particular class of problems rather
> than putting ourselves into opposite camps.
>
> I have to come back to Godel's work as it is (quoting the lecturer) `The most
> profound result to have come out of logic for the last 2000 years, ever since
> the time of Aristotle`. What Godel did, was to write a hack that crashed a
> what was thought to be an uncrashable system.
>
> Principia Mathematica (PM) was a huge book which described how one can of
> about using a subset of mathematics to reason without running into Russell`s
> Paradox (which is the mathematical equivalent of saying `this statement is
> false`). It was found that ANY system that referred back to oneself had the
> potential to have this problem and so all of this circular referencing had to
> be eliminated. The reason why the book was so thick was because most of the
> book was devoted to teaching people how to write mathematics without using
> circular reference. It was dense.
>
> Godel constructed an equivalent system of calculation to that of PM and
> showed that anytime the `+` operator was in the system, then it was possible
> to get the system to talk about itself. Therefore, the phrase `This statement
> is unprovable using our system` will result in a paradox in a system that was
> thought the be free of them. Thus, Godel used the logic presented in the
> framework itself to cause its own downfall.
>
> This result put mathematics in its place, not as the single source of truth
> as Russell and Whitehead, the authors of PM had wanted, but as an incredibly
> tool despite its inconsistencies. It also eliminated the need for future
> mathematicians to waste their time in order to build a complete system of
> mathematics - Godel had proved beyond a shadow of a doubt that this was an
> impossible task.
>
> I see history repeating itself with the offspring of PM (type theory). Like
> PM, It is brilliant and to be honest, it is too abstract for me. However, it
> is my understanding that a lot of the leading research is repeating that of
> PM but with an emphasis on computation. To avoid Russell`s paradox, types are
> always hierarchical, never circular. To express circular referencing of types
> in a none circular way requires a lot of time of a lot of smart people.
>
> There is therefore a lot of pomp and ceremony in order to create a `correct`
> and `complete` system of programming I don't think any of the researchers
> claim this but it is sure marketed that way.
>
> I believe that we have to put type theory in its proper place as a tool for
> programmers and not as the saviour for programming (that mantle belongs to
> lisp of course =p ) For example:
> - one area that is difficult using types is to define multiple hierarchies
> over objects - like properies of can-fly, can-swim, can-run over birds,
> mammals and reptiles.
> - Another area is with partial data. That is, when does a rose not become a
> rose? when it looses its colour? fragrance? shape?. For example… can {:colour
> :red} be considered a rose, even though a rose may be red?
>
>
>
>
>
>
> On 06/10/2013, at 6:02 PM, Mikera <mike.r.anderson...@gmail.com> wrote:
>
>> I suspect you are going to have zero success "proving" the superiority of
>> dynamic languages (in an academic proof sense). For a start, people are even
>> going to disagree about the precise definition of "better". What matters
>> more: Runtime performance? Flexibility with respect to changing
>> requirements? Ease of learning? Minimisation of typing? Ease of language
>> implementation? Etc..... Any such "proof" based on your own definition of
>> "better" isn't likely to convince others who hold different views.
>>
>> My suggestion: just don't worry about it, be pragmatic and use whatever you
>> find helps you to build useful software. Ultimately, that is the main
>> measure of success for a practical general purpose programming language.
>>
>> In particular, I suggest ignoring anyone who launches a "barrage of abuse".
>> Language trolls probably aren't going to give you a sensible conversation in
>> any case.
>>
>> On Sunday, 6 October 2013 11:35:20 UTC+8, zcaudate wrote:
>> I'm a little bit miffed over this current craze of `types` and `correctness`
>> of programs. It smells to me of the whole `object` craze of the last two
>> decades. I agree that types (like objects) have their uses, especially in
>> very well defined problems, but they have got me in trouble over and over
>> again when I am working in an area where the goal is unclear and
>> requirements are constantly changing.
>>
>> BTW... This is no means a criticism of all the type system work that is
>> going on in the clojure community. I am a huge fan of Ambrose's Typed
>> Clojure project because it gives me the option of using types... not shoving
>> it down my throat. I like the freedom to choose.
>>
>> My experience of programming in clojure has freed me from thinking about
>> types and hierarchies and this article rings so true:
>> http://steve.yegge.googlepages.com/is-weak-typing-strong-enough.
>>
>> However, everywhere I look, there are smug type-weenies telling me that my
>> dynamically typed program is bad because it cannot be `proven correct` and
>> not `checked by the compiler`. This question on SO really makes me angry....
>> http://stackoverflow.com/questions/42934/what-do-people-find-so-appealing-about-dynamic-languages....
>> because no one is defending dynamic languages on there. The reason is very
>> simple..... because we don`t have a theory to back us up!
>>
>> I do want to put up an counter argument against this barrage of abuse
>> against dynamic languages. And I want to put some academic weight behind
>> this. The only counter I could come up with was to use Godel's
>> incompleteness theorem. For those that don't know... here is an introduction
>> to the man and his theory. http://www.youtube.com/watch?v=i2KP1vWkQ6Y.
>> Godel's theorem, invalidated Principia Mathematica as a complete system of
>> description. Principia Mathematica btw.... effectively led to Type Theory.
>>
>> According to http://en.wikipedia.org/wiki/Type_theory. "The types of type
>> theory were invented by Bertrand Russell in response to his discovery that
>> Gottlob Frege's version of naive set theory was afflicted with Russell's
>> paradox. This theory of types features prominently in Whitehead and
>> Russell's Principia Mathematica. It avoids Russell's paradox by first
>> creating a hierarchy of types, then assigning each mathematical (and
>> possibly other) entity to a type. Objects of a given type are built
>> exclusively from objects of preceding types (those lower in the hierarchy),
>> thus preventing loops."
>>
>> I'm hoping to collect a few more `proofs` from the clojure community... for
>> example... if there is a paper on "why are type systems so bad at
>> classifying animals"... then please forward it on.
>>
>> --
>> --
>> You received this message because you are subscribed to the Google
>> Groups "Clojure" group.
>> To post to this group, send email to clojure@googlegroups.com
>> Note that posts from new members are moderated - please be patient with your
>> first post.
>> To unsubscribe from this group, send email to
>> clojure+unsubscr...@googlegroups.com
>> For more options, visit this group at
>> http://groups.google.com/group/clojure?hl=en
>> ---
>> You received this message because you are subscribed to a topic in the
>> Google Groups "Clojure" group.
>> To unsubscribe from this topic, visit
>> https://groups.google.com/d/topic/clojure/0I7u5yn01qU/unsubscribe.
>> To unsubscribe from this group and all its topics, send an email to
>> clojure+unsubscr...@googlegroups.com.
>> For more options, visit https://groups.google.com/groups/opt_out.
>
>
> --
> --
> You received this message because you are subscribed to the Google
> Groups "Clojure" group.
> To post to this group, send email to clojure@googlegroups.com
> Note that posts from new members are moderated - please be patient with your
> first post.
> To unsubscribe from this group, send email to
> clojure+unsubscr...@googlegroups.com
> For more options, visit this group at
> http://groups.google.com/group/clojure?hl=en
> ---
> You received this message because you are subscribed to the Google Groups
> "Clojure" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to clojure+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
signature.asc
Description: Message signed with OpenPGP using GPGMail
