Hindley–Milner: Inference Without a Single Annotation
Fresh type variables, constraints, unification, and one clever step — generalization at `let` — buy whole-module inference with a principal type. Then subtyping, overloading and mutable references each break it in a different way.
How does an ML compiler type a whole module with no annotations at all, and why did my language not do that?
The program plus two things it did not have: a supply of *type variables* standing for the unknowns, and a set of equality *constraints* between type terms collected by one walk over the tree. The question this form answers: is the constraint set satisfiable, and if so, what is the most general substitution that satisfies it? “Most general” is the whole point — the answer is not *a* type but the *principal* type, from which every other valid type for the expression is an instance.
Generalization at a let binding is legal only for type variables that are not free in the environment. A variable that is constrained elsewhere must not be quantified, or the same variable gets two incompatible instantiations and the system is unsound. In a language with mutable references that condition is not sufficient: the *value restriction* additionally forbids generalizing any binding whose right-hand side is not a syntactic value, because ref [] allocates one cell that must not be given a polymorphic type.
Key points
- Three moves: fresh type variables and constraints, unification to solve them, generalization at
letwith instantiation at each use. - Generalization at
letis what makesid 1andid trueboth work; without it the two uses share one variable and conflict. - The payoff is the principal-types property: every typeable expression has a single most general type, so inference is deterministic and complete.
- Generalization is legal only for variables not free in the environment; with mutable references even that is insufficient, hence the value restriction.
- HM cannot do subtyping, overloading, polymorphic recursion or higher-rank types. Each of those either destroys principal types or decidability.
- Haskell recovered overloading with type classes; Rust with traits. Both are constrained polymorphism, not plain HM.
- Rust and TypeScript are not Hindley–Milner, and reasoning about their inference as if they were predicts the wrong failures.
- Algorithm W is near-linear in practice and EXPTIME-complete in the worst case; nested
lets can double the type size at each level.
Three moves, one worked example
let (and not at lambda parameters) is the defining restriction of the Hindley–Milner system and is what makes inference decidable with principal types. Removing the restriction gives System F, where inference is undecidable (Wells, 1994) — which is why languages with higher-rank types, including Haskell with RankNTypes, require annotations for exactly those positions.Hindley–Milner is three ideas that only work together. Constraint generation: walk the tree, invent a fresh type variable for every unknown, and record an equality wherever a rule requires two types to agree. Unification: solve the equalities, producing a substitution — the subject of [[unification]]. Generalization and instantiation: at a let binding, quantify the variables that remain free, turning a *type* into a *type scheme*, and at each use of that binding, make a fresh copy of the scheme.
The third move is the one worth understanding in detail, because it is what makes the system useful rather than merely automatic. Without it, the example below fails.
STEP 1 Generate constraints for fun x -> x
x gets a fresh variable x : α
the body is just x body : α
so fun x -> x : α → α
constraints collected: none
STEP 2 GENERALIZE at the let
α is not free in Γ (nothing else mentions it)
so quantify it: id : ∀α. α → α
id is now a SCHEME, not a type.
STEP 3 INSTANTIATE at the first use, id 1
fresh copy: id : β → β
constraint from T-App: β = int
result: int
STEP 4 INSTANTIATE at the second use, id true
a DIFFERENT fresh copy: id : γ → γ
constraint from T-App: γ = bool
result: bool
STEP 5 the pair (int, bool) ✓
WITHOUT step 2, α is a single shared variable:
id 1 forces α = int
id true forces α = bool
int = bool → TYPE ERROR
That is why it is called LET-polymorphism: the
polymorphism is created by the let binding, not by
the lambda. A lambda-bound name is never generalized.Algorithm W, conceptually
Milner’s Algorithm W is the standard presentation: a recursive function taking an environment and an expression, returning a substitution and a type. Its structure follows the typing rules exactly, with one addition per rule — where a rule demanded two types be equal, W calls unify and threads the resulting substitution onward.
The thing to understand about W is not the code but the *invariant*: at every point, the substitution accumulated so far is the most general one consistent with everything seen so far. That invariant is what delivers principal types, and it is also why the order in which W visits the tree affects only where errors are reported, never which programs are accepted.
Its cost is worth knowing honestly. W runs in near-linear time on ordinary code and is EXPTIME-complete in the worst case — Kfoury, Tiuryn and Urzyczyn showed that a chain of nested lets can double the size of the inferred type at each level, so let a = (x, x) in let b = (a, a) in let c = (b, b) in ... produces a type whose printed form is exponential in the program length. This is not a theoretical curiosity in generated code.
- W is a fold over the tree that threads a substitution; every rule contributes constraints and every constraint is discharged immediately by unification.
- A variant, Algorithm J, defers unification into a mutable union-find store instead of composing substitutions — same results, far better constant factors, and what real implementations use. See
[[unification]]. - Generalization is
∀over the free variables of the type *minus* the free variables of the environment. Computing that difference naively is a scan of Γ; production implementations use level or rank numbering to make it O(1). - Instantiation is a fresh copy of the quantified variables at each use site, which is exactly why the two uses of
idabove do not interfere.
What Hindley–Milner cannot do
HM’s guarantees come from what it excludes. Every feature below breaks the principal-types property or decidability, and every language that wanted the feature had to extend or abandon the system.
| Feature | Why HM cannot | What real languages do |
|---|---|---|
| Subtypingspec | With S <: T there is generally no single most-general type for an expression used at both, so principal types cease to exist and unification must become subtype constraint solving | ML-family languages simply do not have subtyping. OCaml has structural object and polymorphic-variant subtyping via explicit coercions, never implicit. Languages that wanted it (Java, Scala, TypeScript) built a different inference engine — see [[subtyping]] |
| Overloading / ad-hoc polymorphismspec | + would need more than one type, so unification has no single answer and solving becomes search | Haskell added type classes, which turn overloading into constrained polymorphism: (+) :: Num a => a -> a -> a, resolved by dictionary passing. Rust’s traits are the same idea — see [[ad-hoc-polymorphism]] |
| Polymorphic recursionspec | Inferring a recursive function used at different types inside its own body is undecidable | Allowed, but only with an explicit signature. Haskell and OCaml both accept it when you write the type and reject it when you do not |
Higher-rank types (∀ under an arrow)spec | Inference for System F is undecidable, so ∀ may only appear at the outermost position of a scheme | Haskell’s RankNTypes and OCaml’s explicit universal annotations accept them with a mandatory signature |
| Mutable referencesspec | Naive generalization of ref [] gives ∀α. α list ref, and one physical cell then gets two element types | The value restriction: only syntactic values are generalized. Standard ML made this the rule in 1996 after weak type variables proved too complicated to explain |
The value restriction, concretely
'_weak1 in OCaml and ''a-style in older SML dialects. The underlying restriction is the same; the precise set of accepted programs differs by implementation and version.This is the sharpest of the five and the one that most often confuses people meeting ML for the first time, because the error it produces looks like the compiler being obstinate about something obviously fine.
Consider let r = ref []. Naively, [] has type ∀α. α list, so ref [] would generalize to ∀α. α list ref. But ref allocates exactly one cell. Instantiate the scheme at int to write an integer into it, then instantiate it at string to read a string out of it, and you have produced a string from an int with no cast, in a system claiming to be sound.
The fix Standard ML adopted in 1996 — and OCaml uses a relaxed version of — is syntactic and blunt: generalize only if the right-hand side is a *value* (a literal, a variable, a lambda, a constructor applied to values). ref [] is a function application, so it is not generalized; its type variable stays unresolved and gets fixed by the first use. The rule rejects some perfectly safe programs, and it is kept because every attempt at a more precise rule — imperative type variables, weak polymorphism with ranks — proved harder to explain than the thing it was replacing.
The general lesson transfers well beyond ML: polymorphism and mutable state interact badly, and every sound system pays for the combination somewhere. Java pays with [[variance]] restrictions and a runtime array-store check. Rust pays with invariance on &mut T and Cell<T>. ML pays with the value restriction. There is no design that gets all three of mutation, polymorphism and full inference for free.
1(* If `ref []` were generalized to ∀α. α list ref ... *)2let r = ref [] (* pretend: r : ∀α. α list ref *)3 4r := [1];; (* instantiate α = int — writes ints *)5List.hd !r ^ "oops";; (* instantiate α = string — reads a string *)6 7(* One cell. Two element types. An int read as a string. *)8(* What OCaml actually reports for `let r = ref []`: *)9(* val r : '_weak1 list ref *)10(* The underscore marks an ungeneralized variable that *)11(* the FIRST use will pin down permanently. *)The weak type variable is not an error — it is the value restriction declining to generalize. The confusing part for newcomers is that the program compiles and then a later, apparently unrelated line fails, because that line tried to use r at a second type.
Rust and TypeScript are not Hindley–Milner
Both are routinely described as “using Hindley–Milner inference”, and both statements are wrong in ways that matter when you are debugging an inference failure.
Rust requires signatures on every fn, which HM does not. It has subtyping — over lifetimes, where a longer lifetime is a subtype of a shorter one — which HM cannot have. It has ad-hoc polymorphism through traits, which plain HM cannot have and which requires a separate trait-resolution engine running alongside unification. What Rust does use is unification with a union-find store *inside a function body*, plus region inference and trait selection, and the interaction between those three is where the genuinely hard inference errors come from. Calling that HM predicts the wrong things: it predicts no annotations are needed, and it predicts trait ambiguity errors cannot happen.
TypeScript is further away still. It has structural subtyping, so principal types do not exist in general; its generic inference works by collecting *candidates* from argument positions and picking one, rather than by solving a constraint set to a most general solution; it uses contextual typing to push expectations down; and it is deliberately unsound in places. There is no generalization step, no ∀-quantified scheme in the HM sense, and no principality guarantee. When TypeScript infers something surprising from a generic call, looking for the HM explanation will not find it — the answer is in candidate inference and its priority rules.
The languages that genuinely implement HM or a close extension are Standard ML, OCaml, Haskell (HM plus type classes, plus a great many opt-in extensions that each require annotations), Elm, PureScript and F#. That set is small, and it is small for the reasons in the previous two sections.
How it works
The steps, in the order the compiler takes them.
- Walk the expression tree with an environment mapping names to type schemes.
- At a variable, look up its scheme and *instantiate*: replace each quantified variable with a fresh one.
- At a lambda, invent a fresh variable for the parameter, extend the environment with it un-quantified, and infer the body.
- At an application, infer both sides, invent a fresh result variable, and unify the function’s type with
argument → result. - At a
let, infer the right-hand side, apply the substitution so far to the environment, then *generalize*: quantify the type’s free variables minus the environment’s free variables. - Extend the environment with the resulting scheme and infer the body.
- Apply the value restriction before generalizing: if the right-hand side is not a syntactic value, quantify nothing.
- At the end, apply the accumulated substitution to every node so the tree carries concrete types for lowering.
How it breaks
What the engineer observes when it goes wrong — not what goes wrong internally.
- The error is reported in a completely different function from the mistake, phrased in terms of type variables the programmer never wrote — the defining complaint about ML-family error messages.
- A binding is silently monomorphised by the value restriction, compiles fine, and then a second use at a different type fails with a message about a weak type variable that names nothing in the source.
- A type printed in an error message is pages long, because nested lets doubled it at each level and the printer expanded the whole thing.
- An engineer adds a signature to “help” the compiler, the signature is more specific than the principal type, and callers that used to work now fail — the annotation constrained rather than clarified.
- Inference succeeds with a more general type than intended, a downstream module uses that generality, and later narrowing the implementation becomes a breaking change nobody meant to make.
- Compile time on one generated module goes from a second to minutes, because the constraint set grew exponentially in a way that never occurs in hand-written code.
When it helps
- Writing ML, OCaml, Haskell, Elm or F#, where understanding generalization is the difference between reading an error message and guessing at it.
- Understanding why your language demands an annotation in a specific place: it is almost always a position where inference would have to go beyond HM — a higher-rank type, a polymorphic recursion, an ambiguous class constraint.
- Implementing inference for a DSL or config language, where HM is a well-trodden, small, correct starting point and every deviation from it should be a deliberate decision.
- Evaluating a claim that a language “has Hindley–Milner inference”, which is usually a claim about ambition rather than about the algorithm.
When it hurts
- As a mental model for Rust, TypeScript, Scala, Kotlin or Swift. All five have subtyping or overloading or both, and their inference behaves differently in exactly the places it matters.
- When it produces a beautifully general type nobody wanted.
∀α β. (α → β) → [α] → [β]is lovely and, as an inferred public signature, is a contract you did not choose to publish. - On generated or macro-expanded code, where the worst-case complexity stops being hypothetical.
- When debugging: the principal-type guarantee says nothing about *where* the contradiction is found, and that is the number everyone actually cares about.
What it costs
Every one of these is paid by something.
- Whole-module inference buys zero required annotations and pays in error locality — a mistake is discovered at the first conflicting constraint, which may be in another function, another file, or a use site the author has never seen.
- The principal-types guarantee buys determinism and completeness, and pays by excluding subtyping and overloading outright. Every mainstream object-oriented language declined the guarantee rather than the features.
- Type classes recover overloading and pay in dictionary passing at runtime (an extra hidden argument and an indirect call per constrained operation) unless specialization removes it, which costs code size instead — see
[[monomorphization]]. - The value restriction buys soundness in the presence of mutation and pays by rejecting safe programs, forcing eta-expansion or explicit annotations in idiomatic code that has nothing to do with mutation.
- Union-find-based implementations (Algorithm J) buy large constant-factor speedups over composing substitutions and pay in a mutable global store that makes backtracking — needed for good error recovery — substantially harder to implement.
What else you could do
What a different compiler or language does instead, and when that is better.
- Bidirectional typing with mandatory signatures: no constraint set, no generalization, errors always attributable to a written annotation. This is what most modern languages chose — see
[[type-inference]]. - Local type inference (Pierce and Turner): infer within an expression from surrounding context, keep subtyping, require annotations at function boundaries. The design underlying Scala, Kotlin and C#’s generic method inference.
- Constraint-based inference with subtyping — MLsub and the algebraic-subtyping line of work — which recovers principal types in the presence of subtyping at the cost of type representations most programmers find unreadable when printed.
- Candidate-based generic inference, as TypeScript does: collect inference candidates from each argument position, prioritise, pick. Not principal, not complete, and it handles structural types and overloads that no principled system does.
- System F with explicit type application: no inference at all, full expressive power, and every polymorphic call site writes its type arguments. Used as a compiler *core* (GHC’s System FC) precisely because nobody wants to write it.
See it for yourself
The flag, dump or tool that shows you this directly.
ghcithen:type +v exprprints the inferred type with its constraints;:set -fprint-explicit-forallsshows exactly which variables were generalized.- OCaml: the top level prints the inferred scheme for every binding. Bindings showing
'_weak1are the value restriction declining to generalize, visible immediately. ocamlc -i module.mlprints the inferred signature for a whole module without compiling it — the fastest way to see what HM concluded about your code.- GHC’s
-ddump-tc-traceprints constraint generation and solving step by step; enormous output, and the only way to see why a particular constraint was created. - For the exponential case: write four nested
lets each pairing the previous binding with itself and ask for the type. The printed result doubles every level. - Our type-inference stepper at
/compilers/typesruns constraint generation, unification and generalization one step at a time on a small ML-like language.
Plausible wrong readings
Stated the way a confident engineer states them.
- “Hindley–Milner means no annotations are ever needed.” It means none are needed for the fragment it covers. Polymorphic recursion, higher-rank types and ambiguous class constraints all require them, in every language that offers them.
- “Rust uses Hindley–Milner.” Rust requires signatures, has lifetime subtyping and has trait-based overloading. It uses unification inside a body; that is not the same claim.
- “The value restriction is a compiler limitation.” It is a soundness requirement. Without it you can read an
intas astringthrough a single mutable cell, with no unsafe construct anywhere. - “Generalizing more would accept more programs.” Generalizing a variable that is free in the environment accepts *unsound* programs. The condition is not conservatism, it is the correctness argument.
- “HM is slow because it is exponential.” It is near-linear on human-written code. The exponential case requires deliberately nested lets and shows up in generated code, not in the average module.
Misconceptions
The claim, and what is actually true.
Num a => a -> a is a constrained scheme — and adds a dictionary-passing implementation strategy underneath.let, not at lambda parameters. A parameter’s type variable stays un-quantified for the whole body, which is what lets the body constrain it — and what makes the system decidable.ref.let f = List.map g is the case that surprises people, and the fix is eta-expansion: let f x = List.map g x.Go deeper
The same idea at increasing depth. Stop wherever it stops being useful.
overview
Hindley–Milner is how ML, OCaml and Haskell type entire programs with no annotations. It gives every unknown a placeholder variable, collects equations between them while walking the code, solves the equations, and — the clever part — at each let binding quantifies the leftover variables so that different uses of the same function can have different types. That last step is why let id = fun x -> x can then be applied to both a number and a boolean. The system is decidable and always finds the most general answer, and it achieves that by excluding subtyping and overloading, which is why most languages you use do not have it.
practical
If you write ML or Haskell, two behaviours account for most confusion. First, errors are reported where a contradiction was found, not where the mistake was — so when a message points at a call site, suspect the definition, and add a signature to the function you believe is right in order to move the blame. Second, a binding whose right-hand side is a function call is not generalized, so let f = List.map g gets a weak type variable that the first use fixes forever. The fix is to eta-expand — let f x = List.map g x — which turns it into a syntactic value and restores generalization. Writing top-level signatures voluntarily is worth it for both reasons: it localises errors and it stops inference from publishing a contract you did not choose.
advanced
The interesting question is why the four exclusions are exclusions. Subtyping and overloading both destroy the property that makes HM work — that the constraint set has a single most-general solution — but they destroy it differently. Subtyping replaces equality constraints with inequalities, so the solution set is a lattice with no canonical element; the algebraic-subtyping line of work (Dolan’s MLsub) shows principal types can be recovered, at the cost of types whose printed form nobody wants to read. Overloading replaces one solution with several, turning solving into search; type classes recover determinism by requiring that the constraint be resolved by a *unique* instance, which is why overlapping instances are a controversial extension and why coherence is the property Haskell guards most jealously. Polymorphic recursion and higher-rank types both fall to the same fact: inference for System F is undecidable, so ∀ cannot appear in arbitrary positions without an annotation. Seen together, these are not four separate limitations but one: HM is exactly the largest fragment of System F for which inference is decidable and principal, and every extension is a negotiation about which half of that guarantee to give up.
internals
A production implementation looks quite different from the textbook. Substitutions are never composed explicitly; instead every type variable is a mutable cell in a union-find structure and unification is a destructive link with path compression — the union-find structure from DSA, used here for exactly the reason it exists. Generalization is where the interesting engineering is: computing “free in the type but not in the environment” by scanning Γ is O(|Γ|) per let and dominates on large modules, so implementations assign each variable a *level* recording the let-nesting depth at which it was created, and generalize precisely those variables whose level exceeds the current one. Unification updates levels as it links, which is a small piece of bookkeeping that turns a scan into a comparison. On top of that sits the machinery nobody writes papers about: recording which constraint came from which span so errors can be attributed, occurs-check failures reported as recursive types rather than as compiler hangs, and a type printer that shares structure so the exponential case prints as a graph instead of a page.
How much this depends on
Nothing in this domain is true of every compiler. These say how much.
let bindings, and the resulting principal-types property, are defining features of the Hindley–Milner system as formalised by Damas and Milner (1982). Lifting the restriction gives System F, whose type inference Wells proved undecidable in 1994. This is why every language offering higher-rank types requires an annotation for them rather than inferring them.If you were asked this in an interview
- Walk me through how
let id = fun x -> x in (id 1, id true)type-checks, and say what breaks if you remove the generalization step. - Why can Hindley–Milner not handle subtyping?
- What is the value restriction, and what unsoundness does it prevent? Give the concrete counterexample.
- Is Rust’s inference Hindley–Milner? Defend your answer with two specifics.
Connections
- Programming Languages & Runtime Internals — Dictionary passing at runtime: how a type-class constraint becomes a hidden argumentType classes recover overloading for HM, and their default implementation strategy is a runtime one — an extra argument holding a record of functions. What that costs at execution time is the runtime’s subject; this lesson needs only that the strategy exists.