Hindley-Milner

How Hindley-Milner works

You hand the compiler an expression like \x -> x + 1 with no type annotations. How does it figure out the type is Int -> Int?

Hindley-Milner walks the expression as an AST and does three things at each node:

1. Fresh type variables. Every unknown gets a placeholder — α, β, γ. The parameter x starts with α.
2. Constraints. The expression's structure imposes equality constraints. x + 1 forces α to equal the input type of +, which is Int.
3. Unification. Solve the constraint set. The result is a substitution from type variables to types, which gets applied back to every type expression.

For \x -> x + 1:

// Step 1: fresh type variables
x : α     // parameter, fresh
+ : Int → Int → Int   // operator's known type
1 : Int   // literal

// Step 2: constraints from x + 1
//   x has type α
//   the left operand of + must be Int
//   ⇒ α = Int

// Step 3: unify
//   {α ↦ Int}

// Step 4: substitute back
//   x : Int
//   x + 1 : Int
//   \x -> x + 1 : Int → Int

The inferred type Int -> Int is the principal type — every other valid type for this expression is an instance of it. There's no instance of Int -> Int that's more general; conversely every more specific type (like Int -> Int itself) is reachable from the principal type by substitution. Damas and Milner proved in 1982 that this principal-type property always holds for HM-typeable expressions.

Algorithm W

The canonical inference algorithm. Recursive over the AST. Returns a substitution and an inferred type at each node.

// Algorithm W (Damas-Milner 1982)
// W(Γ, e) returns (substitution σ, type τ)

W(Γ, x):                        // variable
    let σ = id
    let τ = instantiate(Γ(x))   // fresh tvars for ∀ quantifiers
    return (σ, τ)

W(Γ, λx. e):                    // lambda abstraction
    let α = fresh()
    let (σ, τ) = W(Γ[x := α], e)
    return (σ, σ(α) → τ)

W(Γ, e1 e2):                    // application
    let (σ1, τ1) = W(Γ, e1)
    let (σ2, τ2) = W(σ1 Γ, e2)
    let α = fresh()
    let σ3 = unify(σ2 τ1, τ2 → α)
    return (σ3 ∘ σ2 ∘ σ1, σ3 α)

W(Γ, let x = e1 in e2):         // let-binding
    let (σ1, τ1) = W(Γ, e1)
    let σ1Γ = σ1 Γ
    let scheme = generalize(σ1Γ, τ1)   // close over free type vars
    let (σ2, τ2) = W(σ1Γ[x := scheme], e2)
    return (σ2 ∘ σ1, τ2)

The interesting case is let. After inferring the type of e1, the algorithm generalizes — quantifies free type variables. let id = \x -> x in ... gives id the polytype ∀α. α → α. At each subsequent use of id, the quantifier is instantiated with a fresh type variable. So id 5 uses α₁ → α₁ unified with Int → α₁ — yielding Int → Int; id "foo" uses α₂ → α₂ unified with String → α₂ — yielding String → String. Same definition, two different types. That's let-polymorphism.

Unification

The engine of HM. Given two types, find a substitution that makes them syntactically identical.

unify(τ1, τ2):
    if τ1 == τ2:
        return identity_substitution
    elif τ1 is a tvar α:
        if α occurs in τ2:
            error "occurs check failed — infinite type"
        return {α ↦ τ2}
    elif τ2 is a tvar β:
        return unify(τ2, τ1)
    elif τ1 = (A1 → B1) and τ2 = (A2 → B2):
        σ1 = unify(A1, A2)
        σ2 = unify(σ1 B1, σ1 B2)
        return σ2 ∘ σ1
    else:
        error "type mismatch"

The occurs check is critical. Without it, unifying α with α → β creates an infinite type — α = α → β = (α → β) → β = .... Most ML implementations forbid it; OCaml allows it as -rectypes for recursive types like 'a t = Node of 'a t list.

HM vs subtyping vs bidirectional

	Hindley-Milner	Subtyping	Bidirectional
Inference scope	Whole expression — no annotations	Limited — usually needs annotations	Local — propagates from annotations
Polymorphism	Let-polymorphism (rank-1)	Subtype polymorphism	Whatever surface language has
Principal types	Yes (Damas-Milner theorem)	Often no — many incomparable types	No — depends on annotation placement
Composes with overloading	Poorly — needs type classes	Yes	Yes
Composes with subtyping	Poorly	Native	Yes
Error messages	Often cryptic — "expected α, got Int"	Clearer — type mismatches localized	Clearer — context-sensitive
Complexity	O(n) typical, EXPTIME worst	P or undecidable, depends on system	O(n)
Used by	SML, OCaml, Haskell, F#, Elm	Java, C#, Scala (mixed)	TypeScript, Rust, Swift, Kotlin

HM gives you the strongest theoretical guarantee — principal types — and the most freedom from annotations. Bidirectional inference is more flexible but requires annotations at function boundaries. Real-world languages mix both: OCaml is HM with optional annotations; Rust is bidirectional but locally HM-like.

When HM matters for you

• Writing Haskell, OCaml, F#, or Elm. When a function inferrer "can't figure out" the type, you're hitting HM's limits — typically polymorphic recursion or rank-2 types.
• Designing a language. HM is the gold standard for inference. Even if you ultimately want subtyping or rank-N polymorphism, HM is the baseline to compare against.
• Reading inference error messages. "Couldn't match expected type α with Int → Bool" is Algorithm W reporting a unification failure. Understanding what α is gives you the actionable hint.
• Writing a type-driven analysis tool. Linters, refactorers, and search-by-type tools (Hoogle for Haskell) all use HM's principal-type property to find functions by their signatures.

Haskell example

-- Inferred without annotations
compose f g x = f (g x)
-- Inferred type: ∀a b c. (b -> c) -> (a -> b) -> a -> c

-- The classic identity function
identity x = x
-- Inferred type: ∀a. a -> a

-- A let-polymorphic use
example = let id = \x -> x
          in (id 5, id "hello", id True)
-- The single id is used at three different types:
--   id 5      :: Int
--   id "hello":: String
--   id True   :: Bool

-- An expression that won't infer (rank-2 polymorphism needed)
-- bad f = (f 5, f "hi")   -- ERROR: parameter f must be polymorphic
-- Haskell requires explicit forall to type this:
-- bad :: (forall a. a -> a) -> (Int, String)
-- bad f = (f 5, f "hi")    -- needs RankNTypes extension

Complexity and practical cost

• Algorithm W typical case: O(n) for typical programs — the constraint graph is balanced and unification operates in O(1) per edge using union-find.
• Pathological worst case: Mairson 1990 — a program of n lines whose inferred type has size 2^2^n. Real human-written programs never hit this; the construction nests let-bindings each doubling the prior type's size.
• GHC's HM kernel: infers types for ~50,000 lines of Haskell per second on a modern laptop. Full GHC compile times are dominated by core-to-STG translation and code generation, not type inference.
• OCaml's type inference: ~100,000 lines/second — faster than GHC because OCaml has a simpler type system (no type classes).
• Memory: O(n) substitution table + O(depth) recursion. A 100,000-line program uses ~50 MB of inferrer state.
• Practical EXPTIME blow-ups: Real-world reports are rare. The Haskell wiki has perhaps a dozen historical issues. Modern compilers add a "type size limit" check to abort before runaway types.

Common HM pitfalls

• Polymorphic recursion. A recursive function whose recursive call uses itself at a different type — HM can't infer this without annotations. let rec f x = f (f x) with a different polymorphism per recursive call requires an explicit type signature.
• Value restriction. SML and OCaml restrict generalization to "syntactic values" (lambdas, constants) to preserve type safety with mutable references. let r = ref [] in r := [1]; r := ["a"] would be unsound; the value restriction prevents r from being typed as ∀α. α list ref.
• Rank-N polymorphism. HM only allows polymorphism at let-binding sites (rank-1). Functions taking polymorphic functions as arguments need rank-2 — Haskell's RankNTypes extension lifts this, but inference becomes undecidable.
• Occurs check failures look weird. "Infinite type α = [α]" usually means you wrote a function trying to operate on its own result type — typically an accidental missing function-call or argument.
• HM doesn't compose with overloading. Haskell's type classes solve this by adding constraint contexts (Num α => ...). Without type classes, HM forces you to pick concrete types where overloading would be natural.