Hindley-Milner type inference
Hindley-Milner type inference is the algorithm that enables a compiler to deduce the most general — or principal — type of any expression without requiring explicit type annotations from the programmer. Discovered independently by J. Roger Hindley in 1969 and Robin Milner in 1978, it is the mathematical engine behind the type systems of ML, OCaml, Haskell, and F#, and its influence extends to modern languages through TypeScript's structural typing, Rust's trait system, and Scala's implicits. Hindley-Milner is not merely a convenience feature. It is a theorem about the relationship between syntax and semantics: given any well-typed expression, there exists a unique most general type, and the algorithm computes it.
The Algorithm: Unification and Generalization
The core mechanism of Hindley-Milner is unification, a process of solving equations between types. When the compiler encounters a function application — say, `f x` — it knows that `f` must have a function type `a → b` and that `x` must have type `a`, and that the result has type `b`. It does not know what `a` and `b` are yet; they are type variables, placeholders to be filled in by unification. As the compiler traverses the program, it accumulates constraints — `a` must equal `int`, `b` must equal `string` — and solves them by substituting concrete types for variables.
The second key mechanism is generalization, which turns a type into a polymorphic type. When a `let` binding is encountered, the compiler generalizes any type variables that are not constrained by the surrounding context, producing a polymorphic type that can be instantiated differently at each use site. This is let-polymorphism, and it is what allows the identity function `let id x = x` to be used as `id 5` (type `int → int`) and `id "hello"` (type `string → string`) without explicit type annotations. The type of `id` is inferred as `'a → 'a` — the most general type, a function from any type to the same type.
Principal Types and the Limits of Inference
A principal type is the most general type compatible with all uses of an expression. If an expression can be typed at all, Hindley-Milner finds its principal type; if it cannot, the algorithm reports a type error. This completeness — the guarantee that every well-typed expression has a principal type and that the algorithm will find it — is what makes Hindley-Milner so powerful. It is not heuristic; it is exact.
But this exactness comes with limits. Hindley-Milner requires that polymorphism be introduced only at `let` bindings, not inside lambda abstractions. This restriction — the value restriction — prevents unsound generalization of mutable references. More fundamentally, Hindley-Milner does not handle subtyping, overloading, or higher-rank polymorphism, where a function takes another polymorphic function as an argument. Languages that extend Hindley-Milner with these features — Haskell with type classes, OCaml with polymorphic variants and objects — sacrifice complete inference for expressiveness, requiring partial type annotations where the algorithm would otherwise fail.
Hindley-Milner and the Curry-Howard Correspondence
The connection between Hindley-Milner and logic runs deep. The algorithm is a computational realization of proof search in intuitionistic logic: type variables correspond to propositional variables, unification corresponds to the resolution of equations between propositions, and the principal type theorem corresponds to the completeness of natural deduction. The Curry-Howard correspondence identifies well-typed programs with proofs, and Hindley-Milner identifies type inference with automated proof construction.
This is not a metaphor. When the OCaml compiler infers that `fun x -> x` has type `'a -> 'a`, it is constructing a proof that the identity combinator corresponds to the logical axiom `A → A`. When it rejects `fun x -> x x` — the self-application that leads to paradox in untyped lambda calculus — it is detecting a circularity that has no proof in intuitionistic logic. The type system is a logic, and the inference algorithm is a theorem prover.
Hindley-Milner is the most underappreciated theorem in computer science. It demonstrates that a programming language can be simultaneously untyped in its surface syntax and strongly typed in its semantics — that the programmer can write as if types did not exist, while the compiler ensures that types are never violated. Every language that claims to "reduce boilerplate" by inferring types is standing on Hindley-Milner's shoulders, and most of them do not even know it. The languages that require explicit type annotations for generic functions are not being "explicit"; they are being redundant, repeating information that a fifty-year-old algorithm could have computed for free.