Type inference: Encyclopedia II - Type inference - Hindley-Milner type inference algorithm

Type inference - Hindley-Milner type inference algorithm

The common algorithm used to perform the type inference is the one now commonly referred to as Hindley-Milner or Damas-Milner algorithm.

The origin of this algorithm is the type inference algorithm for the simply typed lambda calculus, which was devised by Haskell B. Curry and Robert Feys in 1958.

In 1969 Roger Hindley extended this work and proved that their algorithm always inferred the most general type.

In 1978 Robin Milner, independently of Hindley's work, provided an equivalent algorithm,

In 1985 Luis Damas finally proved that Milner's algorithm is complete and extended it to support systems with polymorphic references.

Type inference - The Algorithm

The algorithm proceeds in two steps. First, we need to generate a number of equations to solve, then we need to solve them.

The algorithm used for generating the equations is similar to a regular type checker, so let's consider first a regular type checker for the typed lambda calculus given by

and

where E is a primitive expression (such as "3") and T is a primitive type (such as "Integer").

We want to construct a function f of type , where ε is a type environment. We assume that this function is already defined on primitives. The other cases are:

whenever the binding is in Γ

whenever where and .

where and Γ' is Γ extended by the binding .

Note that so far we do not specify what to do when we fail to meet the various conditions. This is because, in the simple type *checking* algorithm, the check simply fails whenever anything goes wrong.

Now, we develop a more sophisticated algorithm that can deal with type variables and constraints on them. Therefore, we extend the set T of primitive types to include an infinite supply of variables, denoted by lowercase greek letters α,β,...

This is a limited overview. For now, refer to Types and Programming Languages by Benjamin Peirce, Sections 22.1-4 .

Solving the equations proceeds by unification. This is - maybe surprisingly - a rather simple algorithm. The function u operates on type equations and returns a structure called a "substitution". A substitution is simply a mapping from type variables to types. Substitutions can be composed and extended in the obvious ways.

Unifying the empty set of equations is easy enough: , where is the identity substitution.

Unifying a variable with a type goes this way: , where is the substitution composition operator, and C' is the set of remaining constraints C with the new substitution applied to it.

Of course, .

The interesting case remains as .

Adapted from the Wikipedia article "Hindley-Milner type inference algorithm", under the G.N U Free Docmentation License. Please also see http://en.wikipedia.org/wiki