Weekly Paper Notes — the Seminal Paper of the Week for the 2026-10-31 digest. Area: Programming Languages.

Author: Robin Milner (University of Edinburgh) Published: Journal of Computer and System Sciences 17(3), December 1978, pp. 348–375. DOI: 10.1016/0022-0000(78)90014-4

Why the paper still matters

In the mid-1970s you could have a type system that caught errors or one that let you write generic code. Pascal and Algol 68 were checked but monomorphic, so a list-reversal function had to be written once per element type. Lisp let you write it once and found the type errors at run time, if at all.

Milner needed both. He was building LCF, a proof assistant at Edinburgh, and its tactics were written in a meta-language, ML. The soundness of the whole system rested on ML’s type checker: a value of type thm could only be built by the inference rules, so the type system was the guarantee that no one forged a theorem. He also wanted users to write small higher-order functions like map and compose them freely without declaring types.

The 1978 paper is how he got both. It defines a polymorphic type discipline for a small functional language, gives an algorithm that infers types with no annotations at all, and proves that any program the algorithm accepts is free of a whole class of run-time failure. The paper’s slogan is still quoted in PL courses: “well-typed programs cannot go wrong.”

The setup

The language is deliberately small: variables, application, λ-abstraction, conditionals, a fixpoint operator for recursion, and let x = e1 in e2. Types are built from base types (int, bool), function arrows and type variables (α, β). A type scheme quantifies some of those variables, as in ∀α. α → α.

Milner gives the language a denotational semantics in which one value, wrong, stands for a run-time type error such as applying an integer as a function. That makes “cannot go wrong” a precise statement rather than a hope.

Two results

Semantic soundness. If an expression has a type under the paper’s typing rules, its meaning is never wrong. Today this is usually proved syntactically, as progress plus preservation (Wright and Felleisen, 1994), but Milner’s version is the first statement of type safety as a theorem about a polymorphic language.

Algorithm W. W walks the expression, assigns fresh type variables to unknowns, and solves equality constraints between types using Robinson’s 1965 unification algorithm. W is syntactically sound: whatever type it returns is a valid typing. Completeness, that W finds the principal (most general) type whenever one exists, came four years later in Damas and Milner (POPL 1982). Roger Hindley had proved the principal-type property for combinatory logic in 1969, without let; that’s why the system is called Hindley–Milner.

The paper also gives Algorithm J, an imperative variant that keeps one global substitution and updates it in place. It’s closer to what real compilers implement.

The algorithm, walked through

Algorithm W on let id = λx. x in (id 3, id true): infer α → α, generalise to ∀α. α → α at the let, instantiate fresh variables at each use, unify one copy with int and the other with bool, and conclude int × bool.

The interesting part is let, shown in the diagram above. W infers the type of the bound expression first, here α → α for the identity function. Then it generalises: any type variable that isn’t free in the surrounding environment is quantified, giving id : ∀α. α → α. In the body, each occurrence of id is instantiated with fresh variables, so id 3 and id true unify against independent copies and both succeed.

Bind id with λ instead ((λid. (id 3, id true)) (λx. x)) and both uses share one monomorphic α, which can’t be int and bool at once, so the program is rejected. That restriction is what keeps inference decidable. Full System F, where λ-bound variables can be polymorphic, has undecidable type inference (Wells, 1994). Limiting polymorphism to let gives up a little expressiveness and gets complete, annotation-free inference in return.

Why this design has outlasted everything around it

ML spread out of LCF into Standard ML, Caml and OCaml, and Hindley–Milner went with it. Haskell built type classes on top of it (Wadler and Blott, 1989). F# is HM over .NET. Rust, Swift, Scala and Kotlin don’t do global HM inference, since subtyping, traits and overloading complicate it, but their local inference is unification over type variables in the same style, and every Rust user who has watched let v = Vec::new() acquire its element type three lines later has seen it work.

The design has been patched over the years, not replaced. Mixing generalisation with mutable references turned out to be unsound, and SML and OCaml settled on Wright’s 1995 value restriction to generalise only syntactic values. GHC went further and stopped generalising local lets by default once type families arrived (“Let Should Not Be Generalised”, Vytiniotis, Peyton Jones and Schrijvers, 2010). The worst case is worse than it looks: ML typability is DEXPTIME-complete (Kfoury, Tiuryn and Urzyczyn; Mairson, both 1990), because nested lets can double type sizes. Real programs almost never hit that, and W stays close to linear in practice.

Milner’s 1991 Turing Award cited LCF, ML and his concurrency work together. The type system is the piece most programmers use every day without knowing whose it is.

Read alongside

Part of the Weekly CS Paper Digest series. Written from the published paper and its well-documented history; the diagram is original to this post.