Here's the Hindley-Milner implementation (in Haskell) from a toy compiler project of mine. It was really enlightening to write it and surprisingly simple.<p><a href="https://github.com/rikusalminen/funfun/blob/master/FunFun/TypeChecker.hs" rel="nofollow">https://github.com/rikusalminen/funfun/blob/master/FunFun/Ty...</a><p>This was also the first time I used monad transformers and almost the first non-IO monad application (I've used ST and Parsec before) I have dealt with. If you compare my code with the book source (Peter Hancock's type checker in Peyton-Jones' "Implementation of Functional Programming Languages", link in source code comment), my version using monads is a lot simpler to follow than the original, written in a pre-Haskell functional programming language called Miranda with no monads.<p>The type checker is a "pure function", it has inputs and outputs but no side-effects but in the code you need to 1) generate unique "names" 2) bail out early on type errors. I solved this problem using Error and State monads. The Miranda code used an infinite list of numbers for unique names and cumbersome tricks to handle type errors.
I find it curious that the venn diagram seems to indicate that a sizable subset of people who are familiar with type theory don't advocate either static typing or dynamic typing.
Disagree about the idea that those who are unfamiliar with type theory prefer dynamic typing.<p>Typing preferences are usually due to trends in language usage having little to do with knowledge.<p>Plenty of java programmers use static typing without ever having to understand type theory.<p>But looking to history of language designers/implementers<p>Dan Friedman<p>Gilad Bracha
<a href="http://www.infoq.com/presentations/functional-pros-cons" rel="nofollow">http://www.infoq.com/presentations/functional-pros-cons</a><p>Guy Steele<p>Rich Hickey<p>All of these guys have worked on static languages,
have a keener understanding of type theory than most,
and yet they seem to promote dynamic languages
at least when it comes to their pet languages.
Why not both?<p>ghc compiler in Haskell has -fdefer-type-errors flag. SBCL Common Lisp implementation has option to turn type warnings into errors. Extending -fdefer-type-errors function and creating better type checker for dynamic languages could achieve best of both worlds.
All this talk about formal type theory, but where are the references to the relevant studies? Where's the data? The few studies[1][2][3][4] I've found are inconclusive one way or the other and none of them focus on error rates. I found another conversation about how to go about studying error rate in dynamically vs statically typed languages, but all I really found was this article studying the affect of hair style on language design[5].<p>[1] <a href="http://pleiad.dcc.uchile.cl/papers/2012/kleinschmagerAl-icpc2012.pdf" rel="nofollow">http://pleiad.dcc.uchile.cl/papers/2012/kleinschmagerAl-icpc...</a> - maintainability<p>[2] <a href="http://dl.acm.org/citation.cfm?id=2047861&CFID=399382397&CFTOKEN=13654132" rel="nofollow">http://dl.acm.org/citation.cfm?id=2047861&CFID=399382397&CFT...</a> - development time<p>[3] <a href="https://courses.cs.washington.edu/courses/cse590n/10au/hanenberg-oopsla2010.pdf" rel="nofollow">https://courses.cs.washington.edu/courses/cse590n/10au/hanen...</a> - development time, take 2<p>[4] <a href="http://pleiad.dcc.uchile.cl/papers/2012/mayerAl-oopsla2012.pdf" rel="nofollow">http://pleiad.dcc.uchile.cl/papers/2012/mayerAl-oopsla2012.p...</a> - usability<p>[5] <a href="http://z.caudate.me/language-hair-and-popularity/" rel="nofollow">http://z.caudate.me/language-hair-and-popularity/</a>
<i>I think you should implement Hindley-Milner in the language of your choice for a small toy λ-calculus.</i><p>Did this a little while ago (as a stepping stone to building an inference system for a more complicated calculus).<p><a href="https://gist.github.com/jrslepak/6158954" rel="nofollow">https://gist.github.com/jrslepak/6158954</a>
As an aside, if you just want curried functions in Clojure, try poppea.<p><a href="https://github.com/JulianBirch/poppea" rel="nofollow">https://github.com/JulianBirch/poppea</a>
I'm familiar with type theory and (often) a proponent of dynamic typing.<p>It depends on what you're doing. If you're building cathedrals-- high-quality, performance-critical software that can never fail-- then static typing is a great tool, because it can do things that are very hard to do with unit testing, and you only pay the costs once in compilation. There are plenty of use cases in which I'd want to be using a statically typed language like OCaml (or, possibly, Rust).<p>If you're out in the bazaar-- say, building a web app that will have to contend with constant API changes and shifting needs, or building distributed systems designed to last decades without total failure (that may, like the Ship of Theseus, have all parts replaced) despite constant environmental change-- then dynamic typing often wins.<p>What I like about Clojure is that, being such a powerful language, you can get contracts and types and schemas but aren't bound to them. I like static typing in many ways, but Scala left me asking the question, any time someone insists that static typing is necessary: <i>which</i> static type system?