Infer the most general type of a program with no annotations at all: give every unknown a fresh type variable, and every time a function is applied, unify (dart 134) its type with (argument → result). What survives is the principal type — the single most-general type, proven to exist. λx.x gets a→a; λf.λx.f x gets (a→b)→a→b.
THE TECHNIQUE fresh variables + unification
Assign each bound variable a fresh type variable; a literal or built-in has a known type; an application f x mints a fresh result var t and unifies the type of f with (type of x) → t. The accumulated substitution, applied to the term’s type, is the principal type. Below: two terms inferred from scratch. live demo
HISTORY & CREDIT Hindley and Milner never met on this
“Hindley and Milner co-invented it” — together independently, on different languages: Hindley typed combinatory logic (1969), Milner built ML’s algorithm and added let-polymorphism (1978). cited
1965 · Robinson — unification (dart 134), the engine the whole thing runs on. 1969 · J. Roger Hindley — the principal-type theorem: every typable combinatory term has a most-general type. (James Morris independently, 1968, is almost always omitted.) 1978 · Robin Milner — Algorithm W for ML + let-polymorphism (let-bound values generalise). This is the algorithm — and it is 1978, not 1982. 1982 / 1990 · Damas & Milner prove W sound and complete (the part “Hindley-Milner” silently drops); Kfoury-Tiuryn-Urzyczyn & Mairson prove ML typability DEXPTIME-complete — deeply-nested lets, not ordinary code (which infers in near-linear time).
Algorithm W is the specification you prove correct, not the code that ships — real compilers use union-find (Milner’s Algorithm J) with Rémy’s level-based generalisation. Milner 1978 / Damas-Milner 1982
RECOMMEND FOR I-13 fresh vars + the unification engine (134)
The core inference runs: fresh type variables + one unification per application, on the same engine as dart 134:
$ i13 run hm.i13 # type variables as ids; arrows via unification
lambda x. x : a -> a (param var == body var -> same type)
lambda x.lambda y.x: a -> b -> a (outer param reused in body; b never constrained)
lambda f.lambda x.f x : application unifies t_f := (t_x -> t_r) -> ok=1, t_f is an arrow
Recommend: the inference core is LIT — type variables are f64 ids; a bound variable used twice forces the same id (so λx.x is a→a, verified); an application unifies a fresh var with an arrow, which (unbound) simply binds — the exact rule that types f x (verified ok=1, the fresh var becomes the arrow). It is dart 134 with types as the terms. Note: the frontier is full nested type terms + let-generalisation — a type is a tree (node arena, PS-015) and generalisation quantifies free variables. The demo animates the whole Algorithm-W inference of (a→b)→a→b; the compiler grounds the fresh-var + unify core that makes it work.