Hindley-Milner Type Inference

A few years ago I lost access to my web site and the Proof-toys people very kindly offered to host this description of Hindley-Milner type inference, including the brilliantly written 1982 paper by Damas and Milner, Principal Type Schemes for Functional Programs, describing the soundness and completeness proofs. There is also a file of the purely functional (but nevertheless buggy! See below.) Standard ML implementation. I am posting this here just to increase the number of links to it.

There are a couple of errors. One is a serious misapprehension I was under. Despite having implemented the algorithm in (apparently working) code, I still thought that resolution happened under universal quantification. That is not so. All quantifiers are stripped before resolving the type-schemes. The mistake is in the last-but-two paragraph on page 12 where I state:

If the assumptions include a type-scheme for x, then the result is simply the generic instantiation of the type-scheme to new variables. Otherwise the algorithm fails.

The other error is in the implementation of capture-avoiding substitution in the function tssubs: it fails when there are free variables in the assumptions Gamma, because an over-enthusiastic optimisation means it doesn't rename below a binder of the variable being alpha-converted. Capture-avoiding substitution is a simple idea, but a bit tricky to implement efficiently, and you probably shouldn't try to implement it in just 22 lines of code!