Hindley–Milner (HM) is a classical type system for the lambda calculus with parametric polymorphism. If you want to know what HM is and why it is cool, please read Daniel Spiewak’s article “What is Hindley-Milner? (and why is it cool?)”

There are multiple implementations of HM in many different languages.

• The Hindley-Milner Algorithm (Perl)
• Hindley-Milner type inference in Scala
• A Hindley-Milner type inference implementation in Python

I reimplemented the algorithm in OCaml guided by Scala and Python implementations. All these implementations are based on the Modula-2 implementation of the Cardelli 1987 paper. Because the algorithm described in the paper depends on mutable states for optimization, it is not easy to implement it directly in a purely functional programming language like Haskell.

The program implements a small functional programming language with no concrete syntax. The language consists of identifier, lambda, application, let and let rec. The type inference algorithm reconstructs the type of the given example expressions in the context of some predefined types. The program produces the following results when executed:

letrec factorial = fn n => cond zero n 1 times n factorial pred n in factorial 5 : int
fn x => pair x 3 x true : Type mismatch bool != int
pair f 4 f true : Undefined symbol f
let f = fn x => x in pair f 4 f true : (int * bool)
fn f => f f : Recursive unification
let g = fn f => 5 in g g : int
fn g => let f = fn x => g in pair f 3 f true : (a -> (a * a))
fn f => fn g => fn arg => g f arg : ((c -> d) -> ((d -> b) -> (c -> b)))