• What is Hindley–Milner?
• Types, schemes, and environments
• Unification (Robinson)
• Algorithm W
• Let-polymorphism and generalization
• Occurs check and infinite types
• Extensions: type classes, GADTs (at a glance)
• Implementation tips
• Exercises

• Polymorphic type inference for λ-calculus with let; principal types without annotations.
• Used in ML-family languages (OCaml, Haskell core), and influences many modern TIs.
• Key ideas: unification + generalization at let-bindings.

• Types: T ::= α | T → T | (T × T) | ...
• Type schemes: σ ::= ∀α1..αn. T (quantified vars)
• Environment Γ maps variables to schemes.

Γ(x) = ∀α. α → α

• Find most general substitution S such that S(T1) = S(T2).
• Rules: unify variables, functions, and ensure occurs check to avoid infinite types.
• Composition of substitutions applies right-to-left.

unify(α, T) = {α ↦ T} if α ∉ freevars(T)

• Recursively infers type of expression and returns substitution + type.
• Let-binding: infer type of rhs, generalize w.r.t. Γ, extend Γ for body.
• Applications: infer f and arg, unify f's type with arg → result.

W(Γ, e1 e2): S1,t1 = W(Γ,e1); S2,t2 = W(S1Γ,e2); α fresh; S3 = unify(S2t1, t2 → α); return S3∘S2∘S1, S3α

• Generalize only those type variables not free in Γ (value restriction in strict langs).
• Instantiation replaces quantified vars with fresh metas on use.
• Maintains principal types and avoids unsoundness.

generalize(Γ, T) = ∀(freevars(T) − freevars(Γ)). T

• Occurs check prevents α = T[α], which would imply infinite types.
• Some practical engines skip occurs check for performance—dangerous without guards.
• Cycle detection or delayed checks can mitigate overhead.

• Type classes add constraints to inference (context reduction, dictionary passing).
• GADTs enrich pattern matching with local refinement; require annotations.
• Effect systems, subtyping, and rank-n polymorphism complicate inference.

• Represent types with union-find style structure for efficient unification.
• Alpha-renaming and fresh variable supply are critical.
• Great error messages: show expected vs actual types, highlight source spans.

Subst = Map; apply(Subst, Type), compose(Subst, Subst)

1. Implement unification with occurs check and test on nested function types.
2. Implement Algorithm W for a small λ-calculus with let-polymorphism.
3. Add type scheme generalization/instantiation and verify principal types.