Unification and the Hindley–Milner Inference Algorithm

A language with explicit types makes the programmer write the same information twice: once in the annotation and once in the code that must satisfy it. Hindley–Milner inference removes the annotation without giving up static checking, and it does so with a single constraint-solving mechanism applied to a small language of type expressions. The algorithm is worth understanding in detail because its limitations — the ones that force annotations back into a program — follow directly from how the solver works.

Types as first-order terms

The type language is deliberately tiny. A type is either a type variable α, a type constructor C applied to arguments, or a function type τ₁ → τ₂. A type scheme σ is either a plain type or a type with universally bound variables, ∀α. σ. The distinction between the two is the whole point of the system: ∀α. α → α is the type of a function that works at every type, while α → α is the type of a function that works at one, currently unknown, type. Inference produces the second and generalizes to the first at binding sites.

The judgment being computed is Γ ⊢ e : τ, read as: in environment Γ, expression e has type τ. Γ maps variables to schemes, not types, which is what allows a name to be used at several different types in one expression. The inference algorithm returns a substitution — a finite map from type variables to types — together with a type. Applying the substitution to the environment must make the judgment hold.

Unification is the only solver required

There is exactly one constraint form: two types must be equal. Solving it is unification, and because the type language is first-order and has no binding constructs of its own, the problem has a most general unifier — a single substitution that every other unifier of the same two types factors through — whenever any unifier exists.

The algorithm walks both types while resolving variables that have already been bound. When both sides are the same variable, nothing happens. When one side is a variable, the variable is bound to the other side, provided the occurs check passes. When both sides are applications of the same constructor, the arguments are unified pairwise. Anything else fails.

The occurs check is not optional. Unifying α with α → β has no finite solution: substituting gives (α → β) → β, then ((α → β) → β) → β, and so on. A checker without the check either loops or builds a cyclic structure that later operations treat as an infinite type. In a real implementation the check is a traversal of the candidate type looking for the variable, so a binding costs time proportional to the size of the type it binds.

A compact implementation makes the mechanics concrete:

class Var:
    _next = 0
    def __init__(self):
        self.id = Var._next; Var._next += 1
        self.link = None          # substitution entry once bound

class App:                        # e.g. List a, or a -> b as App('->', a, b)
    def __init__(self, name, *args):
        self.name, self.args = name, args

def walk(t):
    while isinstance(t, Var) and t.link is not None:
        t = t.link
    return t

def occurs(v, t):
    t = walk(t)
    if t is v: return True
    if isinstance(t, App): return any(occurs(v, a) for a in t.args)
    return False

def unify(a, b):
    a, b = walk(a), walk(b)
    if a is b: return
    if isinstance(a, Var):
        if occurs(a, b): raise TypeError('infinite type')
        a.link = b; return
    if isinstance(b, Var):
        if occurs(b, a): raise TypeError('infinite type')
        b.link = a; return
    if a.name != b.name or len(a.args) != len(b.args):
        raise TypeError('cannot unify')
    for x, y in zip(a.args, b.args):
        unify(x, y)

Binding a variable to a structure rather than composing substitutions keeps each unification step cheap. The alternative — an explicit substitution map applied eagerly to the environment — costs a full traversal of the environment per binding and turns inference quadratic in the size of the program’s type annotations. With the union-find representation above and path compression added in walk, a sequence of unifications costs close to linear time; real checkers add the traversals described below on top of that baseline.

Walking the algorithm over a term

Consider inferring the type of λf. λx. f (f x) with no annotations. Fresh variables α and β are assigned to f and x. Inferring the body f (f x) proceeds inside-out: f has type α and x has type β, so the inner application forces α to be a function type, say β → γ. The application itself then has type γ, and the outer application forces α to equal γ → δ.

Two constraints now sit on α: it is both β → γ and γ → δ. Unifying them equates β with γ and γ with δ, so all three collapse to one variable, and the type of the whole term becomes (β → β) → β → β. Generalizing at the top level yields ∀β. (β → β) → β → β, which is the principal type: every other type the term can have is an instance of this one.

Nothing in that walk required a search. Each syntactic construct generates constraints in a fixed order, and each constraint has at most one solution up to renaming. That is why the algorithm is deterministic and why its result is principal.

Generalization, instantiation, and levels

At a let binding, the inferred type of the right-hand side is closed over the variables that do not appear free in the environment: gen(Γ, τ) = ∀(ftv(τ) \ ftv(Γ)). τ.

The subtraction is essential. A variable that appears in the environment is shared with the surrounding scope and cannot be universally quantified without breaking the constraints already placed on it. At each use of a let-bound name, the scheme is instantiated with fresh variables, so successive uses are independent.

Computing ftv(Γ) naively means traversing the entire environment at every let, which is quadratic in the number of bindings. Production checkers avoid this with a level discipline, associated with the work of Didier Rémy. Each unification variable carries an integer level, and the level of a variable is the nesting depth at which it was created. Entering the right-hand side of a let increments the current level, so variables created inside are born at the inner level. When unification binds a variable at the outer level to a type mentioning a variable at a higher level, the higher-level variable is not lowered by a constraint check; the binding is instead recorded as traversing the level adjustment, which is the smallest level among the outer variables it meets. On leaving the let, only variables whose level exceeds that adjustment and which still appear in the inferred type are candidates for generalization, and they can be collected in one pass without inspecting the environment.

The level discipline also explains a common diagnostic. A variable that was created inside a let but is bound into an outer type by a constraint ends up with a lower adjustment than the level it was created at, so it is not generalized. It keeps its identity, and the printed type shows it as a weak or underspecified variable rather than a bound one. The rules governing when that happens are the subject of let-generalization and the value restriction.

Where the cost actually appears

Unification itself is cheap; the expensive part of a real checker is everything around it.

Occurs-check traversals. Each binding walks the candidate type. For deeply nested types the walk dominates. Some implementations defer the check and detect cycles lazily when a type is printed, which is faster but converts a compile-time error into a diagnostic at an unexpected point.

Error reporting. Unification is destructive: once a variable is bound, the reason for the binding is gone. A checker that reports only the two failing types produces messages that name internal variables and omit the source location that introduced them. Practical checkers therefore attach provenance to constraints or re-run inference with a different constraint ordering to localize the conflict. This is bookkeeping cost, not asymptotic cost, but it is where most of the engineering effort goes.

Worst-case complexity. ML typability — deciding whether a term of the core language has a type — is complete for deterministic exponential time, a result due to Kfoury, Tiuryn, and Urzyczyn. The hardness construction builds programs specifically to force the solver through exponentially many orderings of the same constraints. Ordinary code does not have that shape, so the practical running time stays far below the bound. The theoretical result matters for adversarial input, not for a compiler processing a module. When the language adds overloading or records to the constraint language, the solver changes shape entirely, and the alternatives are described in type classes as dictionary passing.

Sharing of inferred types. If two occurrences of a variable in the source are checked against the same inferred type object, a later unification mutates what an earlier error message described. This is a real source of confusing diagnostics and the reason some checkers copy types before printing them.

What the algorithm cannot express

Three boundaries are structural, not incidental.

The system has no subtyping. τ₁ is either equal to τ₂ or incompatible; there is no ordering between types. Adding one changes the solver from unification to constraint entailment, which is a different algorithm and a different complexity class. Record types therefore cannot be given a width-subtyping rule, and languages that want it must either extend the type language with rows, as described in row polymorphism, or give up inference at record boundaries.

Generalization happens only at let. A variable bound by a lambda is monomorphic within the body of that lambda, so any single lambda cannot use its argument at two different types. This is not a limitation of the solver but a deliberate restriction that keeps inference decidable and sound in the presence of mutable state.

Type constructors are injective. Unifying List α with List β yields α = β, and there is no way to express that two different instantiations of a constructor are the same type. Languages that need that express it through newtypes or through explicit abstraction, not through the inference engine.

The result is a checker that is predictable and produces principal types — at the cost of requiring annotations exactly where the type language runs out of expressive power.