It's a hard problem. Most type-systems forbid the kind of program people write in Clojure
For example (if (keyword? x) ....using the fact that x is a keyword... would not be typable in many languages. (Or there would be hundreds of special cases) There is a category of type systems, that can handle this kind of thing: Dependant Types. (But I am a bit biased, I am a researcher in Dependant Types) With this kind of type systems, you can formalize something like "(keyword? x) = true => x : keyword" But they are still research projects, and most of them needs a lot of type annotations. (Agda is nice, if yo want to try it, though) It is not very hard to have a type-checker for a sub-cases of correct programs in Clojure. (Something like ML + protocols, for example) If other people want to do something, I would happily get involved. But most programs won't be typable except with a very clever type-checker (more clever than the state of the art). At least, it could be helpful in simple code, to put annotations. Best, Nicolas. -- 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
