I am now allergic to integrated type systems mostly because of the lack of efficiency that they impose, at least in my world.
If I can spare some time, I would like to immerse myself in Haskell to see if I can cope with its type system on a daily basis. Still I would think twice before switching to a language that imposes one on me again. Clojure.type looks to me reasonable because it's optional and annotations have no effect on the running code. My academic track record is thin, I always preferred to deliver projects than work on academic studies and this taints my opinion. I do not reject academic thinking, it's needed at some point to create new foundations for practical applications. Clojure is a good example of this interaction. However I am always cautious about debates like this vs real life project comparisons, like any tool they are limits to what theory can prove. Program correctness has been in their air for several decades however in real projects, its applicability has been scarce to non-existent. I know of a Swiss engineer that was building bridges using concrete and none of his designs could be proven by mathematical models in his lifetime. He was using 1/3 of the concrete is competitors were using... Is bridge designs are elegant and sophisiticated. I think there is still a huge gap between academic thinking and real life software projects in general. This is not a criticisim, theory as to lead practical applications, however proofing has to be based on facts otherwise discussions are circling around. A solid basis for a real debate would require some extensive survey of software projects and maintenance with a number of facets (cost, timeline, #bugs, language used, ....) Luc P. > 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 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. > -- Softaddicts<lprefonta...@softaddicts.ca> sent by ibisMail from my ipad! -- -- 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.
