Just a link to the Gilad Bracha post Richard Cole is referring to: Types Are Anti-Modular<http://gbracha.blogspot.it/2011/06/types-are-anti-modular.html> .
Il giorno lunedì 23 dicembre 2013 02:24:08 UTC+1, Richard Cole ha scritto: > > The things is that dynamically typed languages are easier to implement > than statically typed languages. Static typing comes down to making > statements about the program and deriving other statements from them. It > leads to all sorts of interesting work including I think into systems like > Z. However theorem provers are limited in what they can do, and it can be > both limiting and a big distraction to you as programmer to get into a > dialogue with the theorem prover about your program. It can distract you > from your original intention which was to write a program to do something > in particular. > > So simply put, dynamic languages are better than static ones because they > don't distract you with type discussions that can end up being unprofitable > or limiting. Static languages are better because sometimes the type > discussions lead to early and convenient detection of bugs and can also in > some cases make it easier for other people to understand you program or how > to use your library. Static types I think also help refactoring tools. > > Having optional typing in clojure is very nice. It allows for a lot of > experimentation and research on type systems and for them to be used to the > extent that people find them useful in their work. > > It is why I guess Alan Kay said that lisp is not a language, it's a > building material. > > If you want to know what are the current problems in static typing you > going to have to start learning what people are doing in that field, e.g. > is their foreign function interface from Haskel to Java? Why not? Can a > well typed program still exhibit bugs? If the type checking is so powerful > why do bugs persist? You might also look at what Gilhad Brakka was > attempting to do with newspeak and his notions of types being anti-modular. > You are not going to find a proof that that line of enquirely is fruitless, > you'll instead find what people can do today in that field and where > they're pushing the bounds. > > regards, > > Richard. > -- -- 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.
