Parametric Polymorphism

A monomorphic type is a single, concrete type: `int`, `int -> bool`, `[string]`. A function with a monomorphic type works for exactly one instantiation of its type variables. Parametric polymorphism allows a term to have a type that is quantified over one or more type variables, written using the universal quantifier `∀`. The type

says that `id` behaves correctly for any type `α` substituted uniformly for every occurrence — the same code, `λx. x`, works whether `α` is `int`, `string`, or a list of records. This is "parametric" in the strict theoretical sense (owed to Strachey and formalized by Reynolds): the behavior of the function cannot depend on which type it was instantiated at, because the function has no way to inspect `α` at all. This is the crucial contrast with ad-hoc polymorphism (overloading, typeclasses), where different code genuinely runs for different types. Types come in two syntactic classes in the Hindley-Milner system. A type (monotype) τ is built from type variables and constructors: `τ ::= α | int | bool | τ1 -> τ2 | τ list | ...` — no quantifiers appear inside a monotype. A type scheme (polytype) σ is a monotype prefixed by zero or more universal quantifiers: `σ ::= τ | ∀α. σ`. Crucially, quantifiers only ever appear at the outermost level of a scheme — you cannot write `(∀α. α → α) → int` in this system. This restriction to prenex, rank-1 polymorphism is exactly what keeps type inference decidable and syntax-directed; allowing quantifiers to appear nested inside argument positions (rank-2 or higher polymorphism) requires programmer-supplied annotations and loses full inference, which is why Hindley-Milner deliberately stops at rank 1. Two operations connect monotypes and schemes. Instantiation takes a scheme `∀α1...αn. τ` and produces a monotype by substituting fresh, freshly-generated type variables `β1...βn` for `α1...αn` throughout `τ` — "fresh" meaning variables that appear nowhere else in the current inference, so they can later be unified independently at each use site. Generalization is the reverse: given a monotype `τ` derived under a typing environment `Γ`, it closes over the free type variables of `τ` that do not also appear free in `Γ`, producing `∀α1...αn. τ` where `{α1,...,αn} = ftv(τ) \ ftv(Γ)`. Generalization is only sound with respect to variables not constrained by the surrounding context — quantifying over a variable still needed elsewhere would let the checker "forget" a constraint and accept ill-typed programs.

Hindley-Milner's answer to "when do we generalize, and when do we instantiate?" is a simple syntactic rule tied to two constructs: variable lookup and `let`. Every time an identifier is looked up in the environment, its scheme is instantiated with fresh type variables — this is what allows the same `id` to be applied to an `int` in one place and a `bool` in another within a single expression. Every time a `let`-bound expression finishes type-checking, its inferred monotype is generalized with respect to the current environment before the bound name is added to scope for the body — this is what allows `let id = λx. x in (id 1, id true)` to type-check, whereas doing the analogous thing with a lambda parameter (`λid. (id 1, id true)`) does not type-check, because a lambda parameter is monomorphic: it gets one type, fixed once at the call site, for its entire scope. This asymmetry between `let` and `λ` is precisely let-polymorphism. It is a deliberate, principled restriction: full "let-like" polymorphism for every binder (including function parameters) would require quantifiers to appear in argument position of function types — rank-2 polymorphism — and type inference for that system is undecidable in general. Hindley-Milner buys decidability and an efficient (near-linear in practice) inference algorithm by confining generalization to `let`.

Algorithm W, the classical presentation of Hindley-Milner inference, encodes exactly this discipline. ``` // Algorithm W: infer(Γ, e) = (S, τ) // Γ : type environment mapping variables to type SCHEMES // e : expression // Returns a substitution S and a monotype τ such that S(Γ) ⊢ e : τ function infer(Γ, e): match e: case Var(x): if x not in dom(Γ): error "unbound variable" σ = Γ(x) // a scheme ∀α1..αn. τ0 τ = instantiate(σ) // fresh copy, see below return (id_substitution, τ) case Lit(c): return (id_substitution, typeOf(c)) // e.g. int, bool case Abs(x, e1): // λx. e1 — NO generalization here β = freshTypeVar() Γ' = Γ, x : β // β is a MONOTYPE scheme (no ∀) (S1, τ1) = infer(Γ', e1) return (S1, S1(β) -> τ1) case App(e1, e2): (S1, τ1) = infer(Γ, e1) (S2, τ2) = infer(S1(Γ), e2) β = freshTypeVar() S3 = unify(S2(τ1), τ2 -> β) return (S3 ∘ S2 ∘ S1, S3(β)) case Let(x, e1, e2): // let x = e1 in e2 — generalization HERE (S1, τ1) = infer(Γ, e1) σ1 = generalize(S1(Γ), τ1) // close over free vars not in Γ Γ' = S1(Γ), x : σ1 (S2, τ2) = infer(Γ', e2) return (S2 ∘ S1, τ2)

function generalize(Γ, τ): vars = freeTypeVars(τ) \ freeTypeVars(Γ) return ∀ vars . τ // if vars is empty, this is just τ (a monotype scheme) function instantiate(σ): // σ = ∀α1..αn. τ0 fresh = [freshTypeVar() for each αi] return substitute({α1 ↦ fresh1, ..., αn ↦ freshn}, τ0) ``` The unification step (`unify`) is the same Robinson unification used throughout Hindley-Milner and is described fully in Type Inference and Hindley-Milner; it is not repeated here except to note that it produces the most general unifier (MGU) — this is what guarantees the inferred type is the most general one possible, i.e., every other valid typing is an instance of it.

The diagram makes the two disjoint code paths explicit: the body of `λx. x` gets `x` a bare monotype `β` (Abs case — no generalization), while the whole function `id`, once its inference is complete, is generalized once at the `let` boundary into a scheme `∀β. β → β`. Each of the two call sites then independently instantiates that scheme with its own fresh variable, so `int` and `bool` can coexist without conflict — this is the entire mechanism of let-polymorphism in one picture.

Time and space complexity. Instantiation and generalization themselves are cheap: instantiation is a linear-time substitution over the size of the scheme's monotype body, and generalization is a linear scan to compute `ftv(τ) \ ftv(Γ)` (using an efficient representation of `Γ`'s free variables, e.g. a level-based occurs check, this is close to constant amortized work per binding). The dominant cost in the whole algorithm remains unification, which is where the real complexity story lives. With naive substitution-based unification (as literally written above, applying `S1` to `Γ` eagerly), Algorithm W is exponential in the worst case on pathological inputs, because each `App` node can double the size of the type produced by composing substitutions eagerly (classical examples chain many nested lets that build up sharing which then gets copied). In practice — and in essentially every real compiler — this is avoided by implementing types as a union-find structure over mutable type variable cells rather than building explicit substitutions; unification becomes union-find's inverse-Ackermann-amortized operations, and the overall algorithm runs in near-linear time, `O(n α(n))`, for realistic programs, where `n` is program size. This is the standard justification: Hindley-Milner is efficient in the implementation that everyone actually uses, even though the textbook substitution-based presentation is worst-case exponential.

Correctness — soundness. Soundness means: if `Γ ⊢ e : σ` is derivable, then `e` cannot "go wrong" (get stuck) when evaluated, for any instantiation of the type variables in `σ`. The proof is the standard progress + preservation argument (syntactic type soundness), extended with one extra lemma specific to polymorphism:

• Instantiation lemma: if `Γ ⊢ e : ∀α. τ` then for any monotype `τ'`, `Γ ⊢ e : τ[α ↦ τ']`. This says a polymorphic typing really does license every concrete substitution, which is the semantic content of `∀` — exactly Reynolds' parametricity property, that the term's behavior is uniform across all instantiations because it is the same syntactic term being type-checked, not a different one per type.
• Generalization lemma (soundness of closing over unconstrained variables): if `α ∉ ftv(Γ)` and `Γ ⊢ e : τ`, then `Γ ⊢ e : ∀α. τ` is a valid strengthening, because no assumption elsewhere in `Γ` depends on what `α` is, so quantifying it introduces no unsoundness — any future instantiation is consistent with everything already assumed about `e`'s free variables.

The generalization lemma is exactly why the algorithm subtracts `ftv(Γ)`: quantifying over a type variable that Γ still depends on would be unsound, because a later use of some other variable sharing that type could force it to a specific type inconsistent with a different instantiation chosen at `x`'s use site. This is the textbook bug: forgetting to subtract `ftv(Γ)` (over-generalizing) breaks soundness; the correct algorithm never generalizes variables that appear in the environment.

Correctness — principal types. Algorithm W has the principal types property: whenever `e` is typable, W infers a type scheme `σ` such that every valid typing of `e` is a substitution instance of `σ`. This follows from unification producing a most general unifier at every step — if unification always returns the least-committal solution, and generalization quantifies over every variable that is free to vary, then no more specific inference could have thrown away typability. This is what makes Hindley-Milner inference genuinely a decision procedure rather than a heuristic: there is one canonical answer, and the algorithm always finds it or correctly reports "untypable."

The tradeoff — restriction to let-polymorphism. The soundness and decidability above depend on the rank-1 restriction: quantifiers appear only at the top of a scheme, never nested inside a function argument type. If you allowed a lambda parameter itself to have a polymorphic type — e.g., `λ(f : ∀α. α → α). (f 1, f true)` — this is higher-rank polymorphism, and inferring it (without an annotation on `f`) is undecidable in general. Systems that want this power (e.g. GHC Haskell with `RankNTypes`) require the programmer to write the polymorphic type annotation explicitly; inference is not attempted for it. This is the honest cost of let-polymorphism's decidability: full inference in exchange for a real, useful, but restricted form of genericity.

Trace inference on: ``` let compose = λf. λg. λx. f (g x) in let double = compose (λn. n + n) (λn. n + n) in (double 3, compose (λb. not b) (λb. b)) ``` This example is deliberately non-symmetric: `compose` gets used once at `int -> int -> int` (via `double`) and once at `bool -> bool` directly, forcing two genuinely different instantiations of the same generalized scheme.

The crucial moment is step 2 → steps 3 and 6: `compose` is generalized exactly once, into `∀β3 β4 β5. ...`, and then that single scheme is instantiated twice, with completely disjoint fresh variables `γ` and `δ` each time. Because they are disjoint, unifying `γ4=int` in step 3 has no effect whatsoever on `δ4=bool` in step 6 — this disjointness is exactly what "fresh type variables at each instantiation" buys you, and it is why the same `compose` can be soundly used at incompatible concrete types within one program.

Every generic container and higher-order function in OCaml, Standard ML, F#, and Haskell relies on let-polymorphism exactly as described here — `List.map`, `Option.bind`, `Array.sort` are all polymorphic definitions generalized once at their `let`/`val` binding and instantiated fresh at each call site. Rust's generic functions and traits, while checked by a different (bidirectional, not full Algorithm W) system, inherit the same conceptual core: one definition, many monomorphic instantiations, with monomorphization at compile time producing specialized machine code per instantiation — the compile-time cost of parametricity paid explicitly rather than via runtime dispatch. TypeScript's generic functions (`function identity(x: T): T`) and Java's/C#'s generics likewise borrow the `∀`-quantified-scheme model, though with subtler variance and erasure tradeoffs specific to object-oriented type systems. Compiler infrastructure for functional languages (GHC, the OCaml/Flambda pipeline, F#'s FSharp.Compiler.Service) all implement some variant of Algorithm W or its constraint-based cousin, Algorithm M, precisely to support this feature efficiently at scale — and the value-restriction fix for mutable references is load-bearing in every real-world ML/Haskell standard library that exposes references or arrays.

Ask the tutor: Why exactly does allowing generalization inside a lambda body make type inference undecidable, and what would a rank-2 type annotation look like for a function that needs it?