Hindley-Milner type system

The pure Hindley-Milner type system combines function types, type inference and let polymorphism. It solves constraints by type unification and generalizes eligible type variables at let bindings. Robin Milner's 1978 paper presents Algorithm W and proves its soundness for the paper's language; it also acknowledges Roger Hindley's earlier work on finding general types. ^[ref]

Inference of a principal type in the Hindley-Milner type system uses fresh type variables and type unification to satisfy the constraints imposed by expressions. A successful result describes every valid monomorphic instance through type substitution; generalization at suitable bindings forms a type scheme for later instantiation.

Algorithm W performs type inference by traversing the program's abstract syntax tree, introducing fresh type variables, combining type substitutions obtained by type unification, and generalizing eligible let bindings. It distinguishes fresh instances of a type scheme from the shared monomorphic types of parameters to a lambda abstraction.

Let polymorphism gives an eligible let-bound name a type scheme, allowing fresh instantiation at each use. In the pure Hindley-Milner type system, generalize the inferred type's type variables that are free in that type and not free in the current typing context. The identity function example under type variable meets this condition. A lambda abstraction's parameter receives one monomorphic type shared by its uses. Languages with mutation, such as Standard ML with ML reference types, need additional restrictions on generalization.