Lesson 7.3 — Generalization in practice: levels, the value restriction, and complexity¶

Techniques: level-based generalization — decide \(\mathrm{ftv}(\Gamma)\) membership by a per-variable integer instead of a scan of the environment (Rémy 1992 [Rem92]; OCaml's Ctype.generalize; GHC's TcLevel) ; the value restriction — generalize only syntactic values, so that polymorphism and mutable references stay sound (Wright 1995 [Wri95]; Tofte's imperative type variables [Tof90] before it; relaxed by Garrigue [Gar04]); the complexity of Hindley–Milner inference — DEXPTIME-complete in theory (Mairson 1990 [Mai90]; Kfoury, Tiuryn & Urzyczyn 1990 [KTU90]), near-linear in practice (McAllester 2003 [McA03]) · Pebble implements: none (Pebble has no polymorphism); the lab's Algorithm J uses levels and every algorithm applies the value restriction (labs/ch07-hm L2, L4) · Drills: generalization · Prerequisites: Lesson 7.2 · Time: 4 hours

Lesson 7.2's algorithms are correct but leave three practical questions open. How do you compute \(\mathrm{gen}(\Gamma, \tau)\) without looking at the whole environment at every let? What happens when a polymorphic value is stored in a mutable cell? And how bad can inference get? The answers — levels, the value restriction, and a complexity result that is both frightening and irrelevant to everyday programs — are what separates a textbook HM implementation from OCaml's.

1. Problem and motivation¶

Level-based generalization¶

The problem. Gen (Algorithm 7.2.6) must exclude \(\mathrm{ftv}(\Theta\Gamma)\), which in a straightforward implementation means traversing every type in the context at every let: \(\Theta(n \cdot \lvert\Gamma\rvert)\) for \(n\) lets, quadratic on the lab's letChain. Rémy [Rem92] observed that a type variable is free in the context exactly when it was created, or has been unified with something created, outside the let being generalized. Recording for each variable the let-nesting depth — its level — at which it became reachable from the context, and keeping that number up to date during unification, turns the membership test into an integer comparison. OCaml has done this since the early 1990s; Kiselyov's account of the OCaml type checker [Kis13] explains it as "generalization is region-based memory management", and GHC's TcLevel is the same idea used for untouchable variables (Lesson 7.4).

The value restriction¶

The problem. With references, let-polymorphism is unsound. let r = ref (fun x -> x) would give r : ∀α. (α → α) ref; storing an int → int function through one instance and calling it on a bool through another is accepted and crashes. Tofte [Tof90] fixed this with a second kind of type variable ("imperative" variables that are not generalized over expansive expressions); Standard ML '90 adopted it and found it too complex. Wright [Wri95] proposed the blunt, simple rule adopted by SML '97, OCaml, F# and this chapter's lab: generalize the type of a let only if its right-hand side is a syntactic value (a variable, a literal, a function, or a tuple of values). A value cannot allocate a reference when it is evaluated, so no reference can be shared between two instances. Garrigue [Gar04] later relaxed it for variables that occur only covariantly — OCaml's current rule.

Complexity of HM inference¶

The problem. In practice ML type inference is fast; in theory it is not. Mairson [Mai90] and, independently, Kfoury, Tiuryn and Urzyczyn [KTU90] proved that deciding whether a program is typable in HM is complete for deterministic exponential time: nested lets can double the size of a principal type at every level, and a program can use this to simulate an exponential-time Turing machine. McAllester [McA03] explained why this never shows up: if the nesting depth of lets and the size of the types are bounded, inference is nearly linear. A compiler writer needs both facts: the first to know what inputs can hurt (generated code, deeply nested functors), the second to know that the ordinary program will not.

2. Definitions and algorithms¶

Level-based generalization¶

Definition 7.3.1 (Levels)

A level is a natural number or the special value \(\mathsf{generic}\) (greater than every number). The current level \(\ell\) starts at 1 and is incremented when inference enters the right-hand side of a let and decremented when it leaves. Every unbound type variable \(\alpha\) carries a level \(\mathrm{lvl}(\alpha)\); a fresh variable gets \(\mathrm{lvl}(\alpha) = \ell\). A variable with level \(\mathsf{generic}\) is a quantified variable of a scheme; a type with generic variables is a scheme.

Algorithm 7.3.2 (Algorithm J with levels)

Input: a context \(\Gamma\) (types with generic variables are schemes) and an expression \(e\).
Output: a type; the global union-find \(\Theta\) is extended in place.
Precondition: UnifyInPlace is Algorithm 7.1.10 with the level adjustment below.
Postcondition: the same results as Algorithm 7.2.8 (Theorem 7.3.8).
Invariant (Lemma 7.3.7): for every unbound, non-generic variable \(\alpha\) reachable from \(\Theta\Gamma(x)\), \(\mathrm{lvl}(\alpha) \le\) the level at which \(x\) was bound; at a let, after leaving its right-hand side, a variable of the right-hand side's type is free in \(\Theta\Gamma\) iff its level is \(\le \ell\).

function Fresh():           return new variable α with lvl(α) = ℓ
function BindVar(α, t):     # inside UnifyInPlace, before linking α to t
    if Occurs(α, t): fail "occurs"
    for every unbound variable β reachable in t:
        lvl(β) ← min(lvl(β), lvl(α))          # β becomes as old as α
    link α to t
function LinkVars(α, β):    # two unbound variables
    keep the one with the smaller level as representative; link the other to it

function Generalize(τ):     # called with ℓ already decremented
    for every unbound variable α reachable in τ:
        if lvl(α) ≠ generic and lvl(α) > ℓ: lvl(α) ← generic
function Instantiate(τ):    # copies generic variables, shares the rest
    m ← empty map
    return τ with each generic variable α replaced by (m[α] if present else m[α] ← Fresh())

case e of let x = e1 in e2:
    ℓ ← ℓ + 1;  τ1 ← J(Γ, e1);  ℓ ← ℓ − 1
    if IsValue(e1): Generalize(τ1)            # Lesson 7.3, value restriction
    else:           Lower(τ1)                 # every lvl > ℓ becomes ℓ
    return J(Γ[x ↦ τ1], e2)

The value restriction¶

Definition 7.3.3 (Syntactic values; the value-restricted Let rule)

The syntactic values of MiniML are \(v ::= x \mid n \mid \mathsf{true} \mid \mathsf{false} \mid () \mid \mathsf{fun}\ x \to e \mid (v_1, v_2)\) (the lab's isSyntacticValue). The Let rule of Definition 7.2.4 becomes two rules:

\[ \dfrac{\Gamma \vdash v : \tau_1 \qquad \Gamma, x{:}\mathrm{gen}(\Gamma, \tau_1) \vdash e_2 : \tau_2}{\Gamma \vdash \mathsf{let}\ x = v\ \mathsf{in}\ e_2 : \tau_2}\ (\textsf{Let-Val}) \qquad \dfrac{\Gamma \vdash e_1 : \tau_1 \qquad \Gamma, x{:}\tau_1 \vdash e_2 : \tau_2 \qquad e_1 \text{ not a value}}{\Gamma \vdash \mathsf{let}\ x = e_1\ \mathsf{in}\ e_2 : \tau_2}\ (\textsf{Let-Exp}) \]

Let-Exp binds a monotype: its variables are not generalized; OCaml prints them '_weak1, the course's drills '_a.

Algorithm 7.3.4 (Value restriction in W, J and M)

Input: the bound expression \(e_1\) of a let, its inferred type \(\tau_1\), and the context.
Output: the scheme to bind.
Precondition: \(\tau_1\) has the current substitution applied (W, M) or is dereferenced (J).
Postcondition: the scheme is \(\mathrm{gen}(\Gamma, \tau_1)\) if \(e_1\) is a value, the monotype \(\tau_1\) otherwise; in J, the variables of a non-value are lowered to the current level so that an outer let cannot generalize them either.
Invariant: a generalized variable never occurs in the type of a reference allocated by evaluating the program.

function IsValue(e):
    case e of
        x, n, true, false, (), fun x -> e':  return true
        (e1, e2):                            return IsValue(e1) and IsValue(e2)
        otherwise:                           return false
function DecideScheme(Γ, e1, τ1):
    if IsValue(e1): return Gen(Γ, τ1)
    Lower(τ1)                                  # J only: lvl(α) ← min(lvl(α), ℓ)
    return τ1                                  # a monotype

Complexity of HM inference¶

Definition 7.3.5 (HM typability; let-expansion)

HM typability is the decision problem: given a closed MiniML program \(e\) (without references), is there a \(\tau\) with \(\Gamma_0 \vdash e : \tau\)? The let-expansion \(\mathrm{exp}(e)\) replaces, innermost first, every \(\mathsf{let}\ x = e_1\ \mathsf{in}\ e_2\) by \((\mathsf{fun}\ \_ \to [x \mapsto e_1]e_2)\ e_1\) (the extra application keeps \(e_1\) type-checked even if \(x\) is unused). A \(\mathsf{let\ rec}\ f = v\ \mathsf{in}\ e_2\) is first rewritten to \(\mathsf{let}\ f = \mathit{fix}\ (\mathsf{fun}\ f \to v)\ \mathsf{in}\ e_2\) with the monomorphic constant \(\mathit{fix} : (\tau \to \tau) \to \tau\) (the LetRec rule types \(f\) monomorphically inside \(v\), exactly as \(\mathit{fix}\) does), and then expanded like any let.

Algorithm 7.3.6 (Deciding HM typability by let-expansion)

Input: a closed MiniML program \(e\) of size \(n\) without references.
Output: "typable" (with a principal type) or "not typable".
Precondition: pure MiniML (no value restriction needed).
Postcondition: the answer is correct (Theorem 7.3.10); the running time is \(2^{O(n)}\) (§5).
Invariant: \(e\) is typable iff the current, partially expanded program is typable (let-expansion lemma, used in the proof of Theorem 7.3.10).

function Typable(e):
    e' ← exp(e)                            # no let left: at most 2^O(n) nodes
    generate one equation per application/if/operator of e' over fresh variables
    θ ← UnifyUF(equations)                 # Algorithm 7.1.10, polynomial in |e'|
    return "not typable" if UnifyUF fails else θ(type of e')

3. Worked examples¶

Level-based generalization¶

\(e_{\mathrm{lv}} = \mathsf{fun}\ g \to \mathsf{let}\ k = \mathsf{fun}\ y \to g\ y\ \mathsf{in}\ \mathsf{let}\ h = \mathsf{fun}\ z \to (z, z)\ \mathsf{in}\ ((k, h\ 1), h\ \mathsf{true})\) (20 subterms). Algorithm 7.3.2, with \(\alpha\) for \(g\), \(\beta\) for \(y\), \(\gamma\) for the result of g y, \(\delta\) for \(z\):

step	event	current \(\ell\)	variables and levels afterwards
1	`fun g`: \(\alpha\) fresh	1	\(\alpha{:}1\)
2	enter `let k`'s right-hand side	2
3	`fun y`: \(\beta\) fresh; `g y`: \(\gamma\) fresh	2	\(\alpha{:}1\), \(\beta{:}2\), \(\gamma{:}2\)
4	unify \(\alpha \doteq \beta \to \gamma\): bind \(\alpha\), lower \(\beta, \gamma\) to \(\mathrm{lvl}(\alpha)\)	2	\(\alpha \Rightarrow \beta \to \gamma\), \(\beta{:}1\), \(\gamma{:}1\)
5	leave; `Generalize`(\(\beta \to \gamma\)): no level \(> 1\)	1	\(k : \beta \to \gamma\) (monomorphic)
6	enter `let h`: `fun z`: \(\delta\) fresh	2	\(\delta{:}2\)
7	leave; `Generalize`(\(\delta \to \delta \times \delta\)): \(\mathrm{lvl}(\delta) = 2 > 1\)	1	\(\delta{:}\mathsf{generic}\): \(h : \forall\delta.\ \delta \to \delta \times \delta\)
8	`h 1`, `h true`: two instances, linked to \(\mathsf{int}\) and \(\mathsf{bool}\)	1	unchanged schemes

Result: \((\beta \to \gamma) \to ((\beta \to \gamma) \times (\mathsf{int} \times \mathsf{int})) \times (\mathsf{bool} \times \mathsf{bool})\), i.e. ('a -> 'b) -> (('a -> 'b) * (int * int)) * (bool * bool). Step 4 is the whole idea: \(\beta\) and \(\gamma\) were created inside the let, but unification made them reachable from \(g\)'s type, which is in the context; lowering their levels records that, and step 5 correctly refuses to generalize them — exactly what \(\mathrm{ftv}(\Theta\Gamma)\) would have said, without looking at \(\Gamma\).

Try it

./course drill generalization --seed 4 --difficulty medium --solution prints, for each let of a random program, the levels at generalization time next to W's \(\mathrm{ftv}(\Gamma)\) test.

The value restriction¶

\(e_{\mathrm{vr}} = \mathsf{let}\ r = \mathit{ref}\ \mathit{nil}\ \mathsf{in}\ \mathsf{let}\ f = \mathsf{fun}\ x \to x\ \mathsf{in}\ \mathsf{let}\ g = f\ f\ \mathsf{in}\ (r, g)\):

`let`	right-hand side	value?	type at generalization	scheme bound
\(r\)	\(\mathit{ref}\ \mathit{nil}\) (an application)	no	\(t\ \mathsf{list}\ \mathsf{ref}\)	\(t\ \mathsf{list}\ \mathsf{ref}\), \(t\) lowered to level 1: `'_a list ref`
\(f\)	\(\mathsf{fun}\ x \to x\)	yes	\(u \to u\), \(\mathrm{lvl}(u) = 2\)	\(\forall u.\ u \to u\)
\(g\)	\(f\ f\) (an application)	no	\(w \to w\)	\(w \to w\): `'_a -> '_a`

The program's type is 'a list ref * ('b -> 'b) only because the whole program is closed; \(g\) cannot be used at two types (the lab test L2_ValueRestriction checks that (g 1, g true) is rejected). The unsound program the restriction exists for is the lab corpus's 36-value-restriction.mml:

let r = ref (fun x -> x) in
let u = set r (fun y -> y + 1) in
get r true

With the restriction, \(r : (t \to t)\ \mathsf{ref}\) is monomorphic, set r (fun y -> y + 1) fixes \(t = \mathsf{int}\), and get r true fails (# error-wj: 8:1). Without it (hm.infer(src, value_restriction=False) in the oracle), all three algorithms answer bool — and evaluation would add 1 to true.

Complexity of HM inference¶

The pair tower \(\mathit{tower}_n = \mathsf{let}\ x_0 = \mathsf{fun}\ z \to z\ \mathsf{in}\ \mathsf{let}\ x_1 = (x_0, x_0)\ \mathsf{in} \dots\ x_n\) (the lab's pairTower):

\(n\)	program size (nodes)	principal type	arrows in the type
0	4	`'a -> 'a`	1
1	8	`('a -> 'a) * ('b -> 'b)`	2
2	12	`(('a -> 'a) * ('b -> 'b)) * (('c -> 'c) * ('d -> 'd))`	4
\(n\)	\(4n + 4\)	a complete binary tree of pairs	\(2^n\)

Each let instantiates the previous scheme twice, with independent variables; the principal type must record both, so its size doubles. Algorithm 7.3.6 expands the lets and makes the program itself exponentially large; union-find over the shared types does the same work in time proportional to the output. The lab test L1_PairTower_ExponentialType checks the \(2^6 = 64\) arrows of \(\mathit{tower}_6\).

4. Invariants and correctness¶

Level-based generalization¶

Lemma 7.3.7 (The level invariant)

Throughout Algorithm 7.3.2, for every binding \(x\) of \(\Gamma\) made at level \(\ell_x\) and every unbound, non-generic variable \(\alpha\) reachable from \(\Theta\Gamma(x)\): \(\mathrm{lvl}(\alpha) \le \ell_x\). Moreover, every unbound variable reachable from the type of a subexpression being inferred at level \(\ell\) has level \(\le \ell\).

Proof

Initialization: \(\Gamma_0\)'s schemes contain only generic variables. Fresh variables get the current level \(\ell\); a binding made at level \(\ell_x = \ell\) therefore satisfies the invariant. Unification changes reachability only in BindVar(α, t): afterwards, every variable reachable through \(\alpha\) is either reachable through \(t\) or was already reachable; BindVar sets every such \(\beta\) to \(\min(\mathrm{lvl}(\beta), \mathrm{lvl}(\alpha))\), so any binding that reached \(\alpha\) (whose level bound held for \(\alpha\)) now has the same bound for \(\beta\). LinkVars keeps the smaller level, which is at most both. Leaving a let decrements \(\ell\); variables of level \(\ell + 1\) remain only in \(\tau_1\) (the second clause at the inner level), and Generalize or Lower removes every level \(> \ell\) from them. Instantiation creates fresh variables at level \(\ell\) and shares non-generic ones, which satisfy the bound already.

Theorem 7.3.8 (Levels compute gen)

At a let in Algorithm 7.3.2, after inferring \(\tau_1\) and decrementing \(\ell\): an unbound, non-generic variable \(\alpha\) reachable from \(\tau_1\) is in \(\mathrm{ftv}(\Theta\Gamma)\) if and only if \(\mathrm{lvl}(\alpha) \le \ell\). Hence Generalize computes \(\mathrm{gen}(\Theta\Gamma, \Theta\tau_1)\), and Algorithm 7.3.2 computes the same schemes and types as Algorithms 7.2.7 and 7.2.8.

Proof sketch (full development: [Rem92]; OCaml's account: [Kis13])

(\(\Rightarrow\)) If \(\alpha \in \mathrm{ftv}(\Theta\Gamma(x))\), Lemma 7.3.7 gives \(\mathrm{lvl}(\alpha) \le \ell_x \le \ell\), since every binding of \(\Gamma\) was made at a level \(\le \ell\). (\(\Leftarrow\)) Suppose \(\mathrm{lvl}(\alpha) \le \ell\). \(\alpha\) was either created at a level \(\le \ell\) — before entering the let, hence reachable only from types of the context or of sibling expressions already finished; a sibling's type is not reachable from \(e_1\)'s constraints except through \(\Gamma\), so a variable of \(\tau_1\) created outside the let is in \(\Theta\Gamma\) — or it was created at level \(\ell + 1\) or deeper and later lowered by BindVar to the level of a variable \(\gamma\) with \(\mathrm{lvl}(\gamma) \le \ell\) that became bound to a type containing \(\alpha\); by induction on the number of lowerings, \(\gamma\) is reachable from \(\Theta\Gamma\), hence so is \(\alpha\). The equality with W then follows from Theorem 7.2.12. The course checks it empirically: test_w_j_m_agree_on_random_programs compares the schemes of W (by \(\mathrm{ftv}\)) and of levels on 1500 random programs.

The value restriction¶

Proposition 7.3.9 (Unrestricted generalization is unsound with references)

Without the value restriction, the program of §3 (let r = ref (fun x -> x) in let u = set r (fun y -> y + 1) in get r true) has type \(\mathsf{bool}\), and its evaluation gets stuck adding 1 to true.

Proof

Typing: \(\mathit{ref}\ (\mathsf{fun}\ x \to x) : (\alpha \to \alpha)\ \mathsf{ref}\), generalized to \(\forall\alpha.\ (\alpha \to \alpha)\ \mathsf{ref}\). The second let instantiates \(\alpha = \mathsf{int}\): \(\mathit{set}\ r : (\mathsf{int} \to \mathsf{int}) \to \mathsf{unit}\), applied to fun y -> y + 1. The body instantiates \(\alpha = \mathsf{bool}\): \(\mathit{get}\ r : \mathsf{bool} \to \mathsf{bool}\), applied to true: \(\mathsf{bool}\). Evaluation: ref allocates one cell containing the identity; set overwrites it with fun y -> y + 1; get r returns that function, which is applied to true and must evaluate true + 1, which no rule of the operational semantics reduces — the "stuck state" that Lesson 6.1's progress theorem rules out for sound systems.

Theorem 7.3.10 (Soundness with the value restriction; decidability by let-expansion)

(a) MiniML with references, typed with Let-Val and Let-Exp, is sound: a well-typed closed program does not get stuck. (b) For pure MiniML, \(e\) is typable iff \(\mathrm{exp}(e)\) is typable in the simply typed fragment (no schemes needed), so Algorithm 7.3.6 decides typability.

Proof sketch (full proofs: (a) [Wri95, §3–4]; (b) [PR05, §10.1] (let-expansion) with [TAPL §22.3–22.5] (the monomorphic problem))

(a) By progress and preservation (Lesson 6.1) for a store-passing semantics, with a store typing. The only new case is Let-Val: evaluating a value allocates nothing, so the store typing is unchanged when its type is generalized, and substituting the value into the body preserves typing by the substitution lemma for each instance separately; Let-Exp binds a monotype, so the cells allocated by \(e_1\) are typed at one type only. (b) (\(\Rightarrow\)) Given a derivation for \(\mathsf{let}\ x = e_1\ \mathsf{in}\ e_2\), each use of \(x\) in \(e_2\) is typed at an instance of \(\mathrm{gen}(\Gamma, \tau_1)\); substituting a copy of \(e_1\)'s derivation, instantiated accordingly, types each copy of \(e_1\) in the expansion. (\(\Leftarrow\)) If the expansion is typable, each copy of \(e_1\) has a type that is an instance of \(e_1\)'s principal type (Theorem 7.2.11), which is therefore available through \(\mathrm{gen}\) at every use; the extra application \((\mathsf{fun}\ \_ \to \dots)\ e_1\) ensures that \(e_1\) is typable even if \(x\) is unused. By induction on the number of lets.

Complexity of HM inference¶

Theorem 7.3.11 (HM typability is DEXPTIME-complete)

HM typability is decidable in time \(2^{O(n)}\), and every problem decidable in deterministic time \(2^{n^k}\) reduces to it in polynomial time.

Proof sketch (full proofs: [Mai90]; independently [KTU90])

Upper bound: Algorithm 7.3.6. Expanding a let whose variable occurs \(k\) times multiplies the size of its right-hand side by at most \(k + 1 \le 2^k\), and the occurrence counts of the nested lets sum to at most \(n\), so the expansions compose to a factor of at most \(\prod_i (k_i + 1) \le 2^{\sum_i k_i} \le 2^n\) along any nesting: \(\lvert \mathrm{exp}(e) \rvert \le n \cdot 2^{n} = 2^{O(n)}\); the monomorphic unification problem it generates has size linear in \(\lvert\mathrm{exp}(e)\rvert\) and is solved by Algorithm 7.1.10 in almost linear time. Lower bound: Mairson encodes the computation of a deterministic Turing machine running for \(2^{n^k}\) steps as a program whose lets build, by repeated doubling, a type-level representation of the step function applied exponentially many times; the program is typable iff the machine accepts, and the program has polynomial size. The encoding needs nested lets whose types grow exponentially — the pair tower of §3 is its simplest ingredient.

Proposition 7.3.12 (The pair tower's type has \(2^n\) arrows)

The principal type of \(\mathit{tower}_n\) has exactly \(2^n\) occurrences of \(\to\) and \(2^{n+1}\) occurrences of type variables, all distinct in pairs.

Proof

By induction on \(n\). \(n = 0\): \(x_0 : \forall\alpha.\ \alpha \to \alpha\), one arrow, two variable occurrences. Step: \(x_{n+1} = (x_n, x_n)\) instantiates \(x_n\)'s scheme twice with disjoint fresh variables, so its type is the product of two variable-disjoint copies of \(x_n\)'s type: twice the arrows and twice the variable occurrences, each copy's variables still appearing exactly twice. Generalization quantifies all of them.

5. Complexity¶

Technique	Time (worst)	Time (typical)	Space	Variables
Generalization by \(\mathrm{ftv}(\Theta\Gamma)\)	\(O(\lvert\Gamma\rvert + \lvert\tau\rvert)\) per `let` · \(\Theta(n^2)\) on `letChain`	dominated by the context scan	none extra	\(n\) `let`s
Level-based generalization	\(O(\lvert\tau_1\rvert)\) per `let`; lowering \(O(\lvert t \rvert)\) per binding, folded into the occurs check	near-linear overall	one integer per variable	\(\tau_1\) the bound type
Value restriction	\(O(\lvert e_1 \rvert)\) syntactic test per `let`	negligible	none	\(e_1\) the bound expression
HM typability	\(2^{O(n)}\); DEXPTIME-complete (Theorem 7.3.11)	near-linear for bounded let-depth and type size [McA03]	\(2^{O(n)}\) types as trees, less as graphs	\(n\) program size

Justification. Levels: Generalize visits only \(\tau_1\); the level adjustment in BindVar visits exactly the nodes that the occurs check visits anyway, so it adds a constant factor. ftv: computing \(\mathrm{ftv}(\Theta\Gamma)\) visits every type in \(\Gamma\); on letChain(n) the \(i\)-th let has \(i\) bindings in scope. Typability: Theorem 7.3.11. Practice: McAllester shows that with let-nesting depth and type size bounded by constants, a constraint-based algorithm runs in \(O(n\,\alpha(n))\) [McA03].

Pathological families, derived. (1) Exponential: \(\mathit{tower}_n\) — program size \(4n + 4\) (each level adds a let, a pair and two variable occurrences), type size \(\Theta(2^n)\) by Proposition 7.3.12. (2) Doubly exponential printed size: \(f_0 = \mathsf{fun}\ x \to (x, x)\), \(f_{i} = \mathsf{fun}\ y \to f_{i-1}\,(f_{i-1}\,y)\): if \(f_{i-1}\)'s result has \(L_{i-1}\) leaves, \(f_i\) applies it twice, so \(L_i = L_{i-1}^2\) with \(L_0 = 2\), i.e. \(L_n = 2^{2^n}\); as a graph, the type has only \(O(2^n)\) distinct nodes. (3) Quadratic for W: letChain(n), measured below.

Real-world scale. OCaml 4.14.1 prints \(f_4\)'s type as 565 261 characters (§7); the lab's ch07-hm-bench shows W's quadratic factor — 58 ms at \(n = 1000\) against 0.54 ms for J with levels — and all three algorithms at 470–740 ms for \(\mathit{tower}_{14}\), whose type has 338 285 characters.

Level-based generalization¶

Rank-based / region-based generalization [Kis13]: view each let as a region in which variables are allocated; generalization frees the region. Trade-off: the same algorithm, explained as memory management; enables "lazy" level adjustment (OCaml delays updating levels inside types until they are needed).
GHC's TcLevel and touchability [VPJSS11]: levels decide not only generalization but which unification variables an implication constraint may assign (Lesson 7.4). Trade-off: one mechanism for two jobs; the level discipline must also hold for GADT match scopes.
Scanning the context (Algorithm 7.2.6 as written): no bookkeeping. Trade-off: quadratic, and every unification must keep types in \(\Gamma\) up to date (W) or be dereferenced (J).

The value restriction¶

Relaxed value restriction [Gar04] (OCaml since 3.07): generalize variables of an expansive expression that occur only covariantly in its type, e.g. [] @ [] gets 'a list. Trade-off: more programs polymorphic, a variance analysis of type constructors needed.
Imperative type variables [Tof90] (SML '90): track which variables may be stored in references and generalize the others. Trade-off: more precise, but the extra variable kind leaks into signatures and was found too hard to use.
Effect systems and monads (Haskell): references live in IO/ST, so a pure let can always be generalized. Trade-off: no restriction needed, but effects must be typed.

Complexity of HM inference¶

Constraint-based inference with let-constraints (Lesson 7.4, [PR05]): solve the constraints of a let's right-hand side once, simplify them, and copy the simplified scheme at each use. Trade-off: the practical near-linear behavior of [McA03] without let-expansion.
Hash-consing and graph-based type representation (OCaml, Lesson 7.1): keep types shared. Trade-off: fast on the towers of §3, but printing and error messages still pay the tree size.

7. In real compilers¶

Level-based generalization¶

OCaml: typing/ctype.ml keeps current_level (incremented by begin_def, decremented by end_def) and implements generalize by comparing each node's level with it; unification lowers levels through update_level [OCAML-Ctype]. GHC: every meta type variable has a TcLevel, and isTouchableMetaTyVar compares levels in compiler/GHC/Tc/Utils/TcType.hs [GHC-TcType]; simplifyInfer generalizes the variables above the binding's level [GHC-Solver].

OCaml 4.14's generalize is Algorithm 7.3.2's

Reproduce (OCaml 4.14.1 source; curl):

curl -sSL https://raw.githubusercontent.com/ocaml/ocaml/4.14.1/typing/ctype.ml \
  | sed -n '/^let rec generalize ty =/,/^$/p'
mkdir -p ml && echo 'let f = fun g -> let k = fun y -> g y in let h = fun z -> (z, z) in ((k, h 1), h true)' > ml/levels.ml
ocamlc -i ml/levels.ml

Output (complete):

let rec generalize ty =
  let level = get_level ty in
  if (level > !current_level) && (level <> generic_level) then begin
    set_level ty generic_level;
    (* recur into abbrev for the speed *)
    begin match get_desc ty with
      Tconstr (_, _, abbrev) ->
        iter_abbrev generalize !abbrev
    | _ -> ()
    end;
    iter_type_expr generalize ty
  end

val f : ('a -> 'b) -> (('a -> 'b) * (int * int)) * (bool * bool)

What to notice: the test level > !current_level && level <> generic_level is Generalize of Algorithm 7.3.2, down to the special generic level. The second command is §3's \(e_{\mathrm{lv}}\): OCaml gives k one monomorphic type (it appears once, as 'a -> 'b, tied to g's parameter) and uses h at int and bool — the levels trace of §3, and the same type the course oracle computes.

The value restriction¶

OCaml decides expansiveness with is_nonexpansive in typing/typecore.ml and applies the relaxed restriction [OCAML-Typecore]; weak variables print as '_weakN. SML/NJ follows the SML '97 Definition and instantiates non-generalizable top-level variables to dummy types with a warning. F# reports error FS0030 for value-restricted top-level bindings.

The value restriction in OCaml 4.14 and SML/NJ 110.79

Reproduce (OCaml 4.14.1, SML/NJ 110.79):

mkdir -p ml sml && cat > ml/vr.ml <<'EOF'
let r = ref []
let f = (fun x -> x) (fun y -> y)
let g = fun z -> (fun x -> x) (fun y -> y) z
EOF
ocamlc -i ml/vr.ml
cat > sml/vr.sml <<'EOF'
val r = ref []
val f = (fn x => x) (fn y => y)
val g = fn z => (fn x => x) (fn y => y) z
EOF
sml sml/vr.sml < /dev/null

Output (the SML/NJ banner and trailing prompt removed):

val r : '_weak1 list ref
val f : '_weak2 -> '_weak2
val g : 'a -> 'a
[opening sml/vr.sml]
sml/vr.sml:1.6-1.16 Warning: type vars not generalized because of
   value restriction are instantiated to dummy types (X1,X2,...)
sml/vr.sml:2.5-2.32 Warning: type vars not generalized because of
   value restriction are instantiated to dummy types (X1,X2,...)
val r = ref [] : ?.X1 list ref
val f = fn : ?.X1 -> ?.X1
val g = fn : 'a -> 'a

What to notice: ref [] and the application (fun x -> x) (fun y -> y) are not syntactic values, so both compilers refuse to generalize; η-expanding f into g (a fun) restores polymorphism — Let-Val vs Let-Exp of Definition 7.3.3. OCaml keeps the weak variable to be fixed by a later use; SML/NJ, at top level, fixes it to a dummy type at once.

Complexity of HM inference¶

Every HM implementation is exposed to the exponential families; production compilers share type nodes (OCaml, GHC, rustc) so that inference itself stays fast and only printing pays the tree size. GHC's -freduction-depth and OCaml's lack of any limit show the two attitudes: bound the work, or trust that real programs are small.

Doubly exponential types in OCaml 4.14

Reproduce (OCaml 4.14.1):

mkdir -p ml && for n in 1 2 3 4; do
  { echo "let f0 = fun x -> (x, x)"; for i in $(seq 1 $n); do echo "let f$i = fun y -> f$((i-1)) (f$((i-1)) y)"; done; } > ml/dbl$n.ml
  printf 'n=%s  %9s characters in the type of f%s\n' $n "$(ocamlc -i ml/dbl$n.ml | sed -n "/^val f$n /,\$p" | wc -c)" $n
done
ocamlc -i ml/dbl1.ml

Output (complete):

n=1         37 characters in the type of f1
n=2        127 characters in the type of f2
n=3       1965 characters in the type of f3
n=4     565261 characters in the type of f4
val f0 : 'a -> 'a * 'a
val f1 : 'a -> ('a * 'a) * ('a * 'a)

What to notice: a four-line program has a 565-kilobyte type: \(f_n\)'s result has \(2^{2^n}\) leaves (§5, family 2). OCaml computes it instantly because its types are shared graphs; the cost appears only when the type is printed. The same program structure, generalized, is the heart of Mairson's lower bound (Theorem 7.3.11).

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Level-based generalization	Exactly \(\mathrm{gen}(\Theta\Gamma, \tau)\) (Theorem 7.3.8)	\(O(\lvert\tau_1\rvert)\) per `let` · lab: J 0.87 ms vs W 286 ms at \(n = 2000\)	Same types; `'_weak` variables are levels that were lowered	Low once union-find exists: an integer per variable, a `min` in `BindVar`	OCaml, GHC (`TcLevel`), the lab's J
The value restriction	Sound with references (Theorem 7.3.10a); rejects some pure programs (η-expansion fixes them)	\(O(\lvert e_1\rvert)\) per `let` · negligible	Weak variables; SML/NJ warns, F# errors (FS0030)	Very low: one syntactic test	SML '97, OCaml (relaxed [Gar04]), F#, the lab
Complexity of HM inference	DEXPTIME-complete (Theorem 7.3.11)	\(2^{O(n)}\) worst · near-linear for bounded let-depth and type size [McA03]	Exponential types are unreadable before they are slow	— (a property, not an implementation)	Explains generated-code and functor blow-ups; motivates shared types

Choose levels in any HM implementation you expect to scale. Choose the value restriction (or the relaxed one) whenever the language has mutable state and let-polymorphism; choose effect typing if you design the language from scratch. Remember the complexity result when you generate code that nests lets or functor applications deeply: bound the nesting, or share and never print the types.

9. Assessment¶

Technique	Quiz ids	Drill	Flashcard tag	Exercises
Level-based generalization	`levels-generalize`, `levels-lowering`	`generalization`	`levels`	lab L2
The value restriction	`vr-schemes`, `vr-unsound`	`generalization` (`--difficulty hard`)	`value-restriction`	lab L1–L3 (SPEC §3.4)
Complexity of HM inference	`tower-arrows`, `dexptime`	— (a complexity result; the lab's `ch07-hm-bench` measures it, and `tower-arrows` is computed)	`hm-complexity`	lab L4

References¶

See the chapter references.

Lesson 7.3 — Generalization in practice: levels, the value restriction, and complexity¶

1. Problem and motivation¶

Level-based generalization¶

The value restriction¶

Complexity of HM inference¶

2. Definitions and algorithms¶

Level-based generalization¶

The value restriction¶

Complexity of HM inference¶

3. Worked examples¶

Level-based generalization¶

The value restriction¶

Complexity of HM inference¶

4. Invariants and correctness¶

Level-based generalization¶

The value restriction¶

Complexity of HM inference¶

5. Complexity¶

6. Variants and refinements¶

Level-based generalization¶

The value restriction¶

Complexity of HM inference¶

7. In real compilers¶

Level-based generalization¶

The value restriction¶

Complexity of HM inference¶

8. Comparison¶

9. Assessment¶

References¶