Really Getting Hindley-Milner

Really Getting Hindley-Milner

Hindley-Milner is a type system used as a basis for the types in ML, Haskell and F#. Along with the formal definition is an inference algorithm "Algorithm W" that can deduce the most general type of an expression. Being hugely important component in functional programming it was something I really wanted to understand.

Having read the Wikipedia article, the original paper and several blog posts on it, in addition to implementing a simple unification based type-checker, I still wasn't able to fully comprehend how it all hung together. The next step was obviously to implement the famous Algorithm W and see what happened at the tricky bits.

So last summer working mostly from wikipedia and the original paper, and checking my work as I went against the excellent article "Algorithm W Step by Step" by Martin Grabmüller, I finally managed to crack it. It was the perfect "ah-ha" moment when all the components I understood seperately suddenly came together in an elegant way.

I've put the code I wrote for this up on github. I ended up modifying my code as I went to more closely follow the (better thought out) typeclasses of the article above. The actual algorithm is in Inference.hs (named w for the original paper) but most of the supporting plumbing is in Types.hs. It was also another opportunity to use the Parsec parsing and HUnit unit testing libraries which consistently impress me.

Checking over it recently I noticed that it doesn't support recursive parameterised types (eg. List a) but it's just a small issue with the constructor parsing and building, the algorithm implementation should support it. It can do parameterised types (Maybe a, Either a b), and recursive types (IntegerList = Empty | Cons Int IntegerList), separately though.

So if you're still in the "I want to get HM, but I'm just not quite there", I'd definitely recommend having a go at it yourself.

comments powered by Disqus