Type Inference: Hindley-Milner

OCaml, Haskell, Elm, F# - write a function body with no type annotations and the compiler produces a precise, sound type. No guessing. No runtime checks. This is Algorithm W, first published by Robin Milner in 1978 and formalized by Luis Damas in 1982. The same algorithm, with extensions, ships inside GHC today. Understanding it means understanding how a compiler can be smarter about types than the programmer.

• **Haskell / OCaml:** full type inference - entire programs can be written without annotations, and the compiler will infer everything
• **Rust:** the borrow checker uses unification to infer lifetimes, and trait bounds extend HM constraints
• **TypeScript:** `const x = [1, 2, 3].map(n => n * 2)` - the type `number[]` is inferred automatically via flow analysis inspired by HM

Предварительные знания

• Static vs Dynamic Typing

Hindley-Milner: type inference without annotations

In 1969 mathematician J. Roger Hindley proved the principal type theorem for combinatory logic: every well-typed term has a unique most general type, of which all other valid types are instances. Robin Milner independently rediscovered this result in 1978 while building the ML language - and implemented it as Algorithm W. Luis Damas completed the formal proof and generalization rules in his 1982 paper 'Principal type-schemes for functional programs' with Milner. The result: a language where the programmer writes zero type annotations and the compiler infers a provably correct type for every expression. Hindley-Milner is the type-theoretic foundation of OCaml, Standard ML, Haskell 98, Elm, F#, and parts of Rust. TypeScript chose bidirectional inference instead to preserve JavaScript compatibility - the trade-off is expressiveness versus inference completeness.

Unification - solving type equations

When `f(x) = x + 1` is written, the compiler must determine the type of `f` without a single annotation. How? It builds **type equations** and solves them - exactly the way a system of equations is solved in algebra.

**Unification** is an algorithm for finding a substitution that makes two types equal. If `τ₁ = α → Int` and `τ₂ = Bool → β`, then the substitution `{α ↦ Bool, β ↦ Int}` unifies them: both become `Bool → Int`.

Formally, a substitution is a mapping `S: TypeVar → Type`. Applying substitution `S` to type `τ` is written as `S(τ)`. Unifying two types `τ₁` and `τ₂` finds an `S` such that `S(τ₁) = S(τ₂)`.

**Occurs check** - a critical step in unification. If the variable `α` appears inside the type `τ`, then the equation `α = τ` has no finite solution. For example, `α = List α` would require an infinite type `List (List (List ...))`. Without the occurs check, the algorithm would loop forever.

Let-polymorphism

Consider the identity function: `let id = λx.x`. What is its type? It takes anything and returns the same thing. Intuitively the type is `∀a. a → a` (for any type `a`, it takes `a` and returns `a`). This is a **polymorphic** type.

But polymorphism does not arise everywhere. **Let-polymorphism** (also called Damas-Milner) states: generalization happens only at `let`-bindings. Variables bound via `λ` remain **monomorphic** inside the λ body.

**Generalization rule:** after inferring type `τ` for `let x = e`, all free type variables in `τ` that do NOT appear in the environment (context) are generalized with the `∀` quantifier. This turns `id: α → α` into `id: ∀α. α → α`.

Constraint Solving - generating and solving constraints

Type inference can be split into two phases: **(1) constraint generation** from the expression and **(2) solving** those constraints via unification. This separation makes the algorithm modular and extensible.

In the first phase we traverse the AST, assign fresh type variables, and generate equations of the form `τ₁ = τ₂`. In the second phase we unify all equations in sequence, accumulating a substitution.

**The constraint-based approach** is used in modern compilers (GHC, OCaml, Rust) instead of pure Algorithm W because it scales better: constraints can be collected in parallel and solved in an optimal order. Type error messages are also more informative.

Damas-Milner Algorithm W

**Algorithm W** is a formal type inference algorithm published by Luis Damas and Robin Milner in 1982. It combines constraint generation and unification into a single recursive procedure that traverses the AST.

The key property of Algorithm W: it always finds the **principal type** (most general type). If an expression has type `Int → Int` but also `∀a. a → a`, the algorithm returns `∀a. a → a` - every other valid type is an instance of the principal type.

**Generalize** in Case 4 (Let) is what distinguishes `let` from `λ`. Free type variables in `τ₁` not appearing in context `Γ` are generalized with `∀`. This is why `let id = λx.x` yields the polymorphic `∀a. a→a`, while `λf. f 1; f true` is a type error.

Algorithm W is used (with extensions) in **Haskell** (GHC - OutsideIn with type classes), **OCaml**, **Rust** (partially, with trait bounds), **F#**, **Elm**, **PureScript**. TypeScript is inspired by HM but uses structural typing and bidirectional inference.

**Algorithm W complexity:** O(n) in typical cases, but theoretically can be exponential (DEXPTIME-complete). In practice this is not an issue - pathological cases require deeply nested let-expressions, which rarely appear in real code.

Key ideas

• **Unification** solves type equations via substitution - if `α = Int → β` and `β = Bool`, then `α = Int → Bool`
• **Occurs check** prevents infinite types: `α = List α` has no finite solution
• **Let-polymorphism** generalizes types only at `let`-bindings - λ-bound variables remain monomorphic
• **Algorithm W** recursively traverses the AST and guarantees finding the **principal type** - the most general type of the expression
• Modern compilers use the **constraint-based** variant of HM for better error diagnostics and extensibility

Related topics

Type inference is a central topic in programming language theory, connected to type systems, formal logic, and compiler design:

• Type systems — HM is a specific type system with full inference; more expressive systems (System F, dependent types) require annotations
• Lambda calculus — HM types the simply-typed λ-calculus with let-polymorphism - this is the formal foundation of the ML family
• Generics and parametric polymorphism — HM let-polymorphism is parametric polymorphism; generics in Java/C# are inspired by this idea

Вопросы для размышления

• Why did the Hindley-Milner designers choose let-polymorphism over the full polymorphism of System F? What trade-off does this represent?
• If Algorithm W finds the principal type, why is it still recommended to write type annotations for top-level functions in real code?
• TypeScript uses structural typing and bidirectional inference instead of classic HM. What are the advantages and disadvantages compared to OCaml/Haskell?

Связанные уроки

• plt-03-static-vs-dynamic — Static typing concepts are prerequisite - HM is a specific static type system
• plt-02-type-systems — Type system foundations needed before diving into HM inference mechanics
• plt-05-gradual — Gradual typing extends HM to integrate with dynamically typed code - needs HM as foundation
• plt-07-algebraic-types — ADTs combined with HM inference is the core of OCaml/Haskell - this lesson unlocks that pairing
• plt-42-dsl-compilers — DSL type checking in compilers applies the same constraint generation + unification pipeline
• alg-21-dp