<p> <center>

&lt;a href="http://ro-che.info/ccc/17" title="Why static vs dynamic typing battles are rarely interesting."&gt;&lt;img src="/img/typing.png" alt="Typing Comic from Cartesian Closed Comics" /&gt;&lt;/a&gt; &lt;/center&gt; &lt;/p&gt; &lt;p&gt;All sarcasm aside, the above diagram has a kernel of truth. The important thing to note is that the intersection between &quot;Proponents of dynamic typing&quot; and &quot;People familiar with type theory&quot; is very small.&lt;/p&gt; &lt;p&gt;In an effort to increase the size of that intersection, I decided to familiarize myself with a little more type theory. I developed an implementation of Hindley-Milner which operates on a simple Lisp-like λ-calculus with let polymorphism. Everything you need for Hindley-Milner Algorithm W.&lt;/p&gt; &lt;h3 id="background"&gt;Background&lt;/h3&gt; &lt;p&gt;Hindley-Milner is a type system that is used by ML and Haskell. Algorithm W is a fast algorithm for inferencing Hindley-Milner which is syntax-directed (meaning it is based on the type of expression) and recursively defined. In this way, it is similar to &lt;a href="Lisp's">http://www.paulgraham.com/rootsoflisp.html">Lisp's &lt;code&gt;eval&lt;/code&gt;&lt;/a&gt;.&lt;/p&gt; &lt;h3 id="implementation"&gt;Implementation&lt;/h3&gt; &lt;p&gt;I based my implementation on a paper called &lt;a href="Algorithm">http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733klzzwxh:0004rep=rep1klzzwxh:0005type=pdf">Algorithm W Step by Step&lt;/em&gt;&lt;/a&gt; which implemented it in Haskell. My implementation started very similar to that implementation and diverged as I refactored it into a more Clojure-esque style.&lt;/p&gt; &lt;p&gt;This implementation uses no in-place mutation, instead using a &quot;substitution style&quot; which is slightly harder to read. It is, however, easier to write and prove correct.&lt;/p&gt; &lt;p&gt;In addition to the type inferencer, I wrote an interpreter for the same language, just because. My original intent was to expose (to myself) the similarities between syntax-driven type inference and &lt;code&gt;eval&lt;/code&gt;. There might be some, but the full clarity I desire is yet many refactorings away. Note that the interpreter and type inferencer are completely independent, except that both apply to the same set of expressions.&lt;/p&gt; &lt;p&gt;I added a couple of minor luxuries to the language having to do with currying. Writing fully parentheisized function applications for curried functions is a pain, as is writing a hand-curried function with multiple arguments. I added two syntax transformations which transform them into a more Lispy style. For example:&lt;/p&gt; &lt;pre&gt;&lt;code&gt;(fn [a b c d e f] 1) =&gt; (fn a (fn b (fn c (fn d (fn e (fn f 1))))))&lt;/code&gt;&lt;/pre&gt; &lt;p&gt;and&lt;/p&gt; &lt;pre&gt;&lt;code&gt;(+ 1 2) =&gt; ((+ 1) 2)&lt;/code&gt;&lt;/pre&gt; &lt;p&gt;I'm pretty sure the syntactic transformation is completely safe. All of my tests still type check.&lt;/p&gt; &lt;p&gt;The final luxury is that it is a lazily-evaluated language. That's not strictly necessary, but it is strictly cool. It builds up thunks (Clojure delays and promises) and a trampoline is used to get the values out. This lets me define &lt;code&gt;if&lt;/code&gt; as a function. The only special forms are &lt;code&gt;let&lt;/code&gt; and &lt;code&gt;fn&lt;/code&gt;.&lt;/p&gt; &lt;h3 id="where-to-find-it"&gt;Where to find it&lt;/h3&gt; &lt;p&gt;You can find the code in the &lt;a href="ericnormand/hindley-milner">https://github.com/ericnormand/hindley-milner">ericnormand/hindley-milner Github repo. I don't promise that it has no bugs. But it does have a small and growing test suite. Pull requests are welcome and I will continue to expand and refactor it.&lt;/p&gt; &lt;h3 id="what-i-learned"&gt;What I learned&lt;/h3&gt; &lt;p&gt;Type unification is why the error messages of most type inferencers are so bad. Unification by default only has local knowledge and is commutative (&lt;code&gt;unify a b == unify b a&lt;/code&gt;). No preference is given to either argument. A lot of work must have gone into making the error messages of Haskell as good as they are.&lt;/p&gt; &lt;p&gt;Let polymorphism is useful and I'm glad that Haskell has it.&lt;/p&gt; &lt;p&gt;Hindley-Milner is powerful, but it does not by itself work magic on a languageq. A language still requires a lot of good design and a well-chosen set of types.&lt;/p&gt; &lt;h3 id="your-turn"&gt;Your turn&lt;/h3&gt; &lt;p&gt;I think you should implement Hindley-Milner in the language of your choice for a small toy λ-calculus. There is a lot to learn from it, even if you never program using a Hindley-Milner language. At the very least, you'll know what the fuss is about.&lt;/p&gt; &lt;p&gt;If you think it would be helpful, have a look at &lt;a href="my">https://github.com/ericnormand/hindley-milner">my implementation&lt;/a&gt;. Like I said, pull requests are welcome.&lt;/p&gt;