Hindley-Milner in Clojure
All sarcasm aside, the above diagram has a kernel of truth. The important thing to note is that the intersection between "Proponents of dynamic typing" and "People familiar with type theory" is very small.
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.
Background
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 Lisp's
eval.
Implementation
I based my implementation on a paper called Algorithm W Step by Step 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.
This implementation uses no in-place mutation, instead using a "substitution style" which is slightly harder to read. It is, however, easier to write and prove correct.
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 eval. 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.
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:
(fn [a b c d e f] 1) => (fn a (fn b (fn c (fn d (fn e (fn f 1))))))
and
(+ 1 2) => ((+ 1) 2)
I'm pretty sure the syntactic transformation is completely safe. All of my tests still type check.
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 if as a function. The only special forms are
let and fn.
Where to find it
You can find the code in the 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.
What I learned
Type unification is why the error messages of most type inferencers are
so bad. Unification by default only has local knowledge and is
commutative (unify a b == unify b a). 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.
Let polymorphism is useful and I'm glad that Haskell has it.
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.
Your turn
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.
If you think it would be helpful, have a look at my implementation. Like I said, pull requests are welcome.
