Hindley–Milner Type Inference

In the simply typed calculus of chapter 2, every abstraction carries its domain. The identity function on natural numbers and the identity function on functions are therefore two different terms, and a program that needs the identity at seven types must contain seven copies of it. The defect is not the annotation itself but the granularity of the discipline: nothing in the body $x$ depends on the domain, yet the typing rules force a choice once and for all. A replacement discipline must remove that defect while keeping typechecking mechanical. Three demands constrain it.

1. One unannotated definition of the identity must serve every use, each use at the type that its position demands.

2. The programmer writes no types at all; the types are computed.

3. The computed answer must be principal: a single most general description of which every other valid description is a specialization, so that the algorithm never commits to an accidental choice.

Using the unannotated definition $\lambda x.x$ once at the two types displayed above is parametric polymorphism, or simply polymorphism in this chapter: one definition is reused at several types.

The let-language

Two differences from section 2.1 matter. Abstractions carry no domain: the discipline must recover it. And a new binding form $\mathsf{let}$ appears. For evaluation, $\mathsf{let}x=e_1\mathsf{in}{e}_2$ behaves as the application $(\lambda x.e_2)e_1$; for typing it will behave differently, and that difference is the entire subject of the chapter.

With let, one identity definition can be instantiated independently at $\mathsf{Nat}$ and at $\mathsf{Nat}\to \mathsf{Nat}$. Write $$P_{\mathsf{id}}:=\mathsf{let}\mathsf{id}=\lambda x.x\mathsf{in}(\mathsf{id}\mathsf{succ})(\mathsf{id}\mathsf{zero}).$$ One definition of the identity; two uses. The outer use applies $\mathsf{id}$ to $\mathsf{succ}$, so there it must have type $(\mathsf{Nat}\to \mathsf{Nat})\to (\mathsf{Nat}\to \mathsf{Nat})$; the inner use applies it to $\mathsf{zero}$, so there it must have type $\mathsf{Nat}\to \mathsf{Nat}$. A single simple type cannot do both jobs. The discipline we construct assigns $\mathsf{id}$ a type scheme: one type together with a finite list of variables that each use may replace independently. For identity, the type is $\alpha \to \alpha$ and the list contains $\alpha$. The outer use replaces both occurrences by $\mathsf{Nat}\to \mathsf{Nat}$; the inner use replaces both by $\mathsf{Nat}$.

Monotypes, type schemes, and the declarative system

Monotypes and substitutions

Monotypes contain no binders. Consequently substitution for type variables is plain structural recursion, with no renaming and no capture; this simplicity is load-bearing for everything that follows.

Proof of Lemma 4.6 — Extensionality of type substitution

Proof. Induct on the finite tree $\tau$. The variable case is the hypothesis. At $F({\tau }_1,\dots ,{\tau }_n)$, every variable of a component belongs to $\mathrm{ftv}(\tau )$, so the induction hypotheses give ${\tau }_i[S]={\tau }_i[T]$ for every $i$; congruence of $F$ gives the conclusion. ◻

Type schemes

For example, with $\sigma =\mathrm{\forall }\alpha .\alpha \to \alpha$: $$\sigma \succcurlyeq \mathsf{Nat}\to \mathsf{Nat},\sigma \succcurlyeq (\beta \to \beta )\to (\beta \to \beta ),\sigma ⋡\mathsf{Nat}\to \mathsf{Bool},$$ the last because $(\alpha \to \alpha )[\rho /\alpha ]$ always has equal domain and codomain. Also $\sigma ⊒\mathrm{\forall }\beta .(\beta \to \beta )\to (\beta \to \beta )$: each instance of the right-hand scheme has the form $(\rho \to \rho )\to (\rho \to \rho )$, which is $(\alpha \to \alpha )[\rho \to \rho /\alpha ]$. The converse fails, so $⊒$ is a preorder of generality. It becomes an order only after quotienting schemes that have the same monotype instances; this identifies alpha-renamed schemes and schemes differing only by vacuous quantifiers. The quotient matters when principal answers are compared: principality determines the set of instances, not a unique printed quantifier prefix.

The semantic definition of $⊒$ is the right notion to use, but a syntactic test is needed to compute with it.

Proof of Lemma 3.9 — Characterization of generality

Proof. ($\Leftarrow$) Suppose ${\tau }_2={\tau }_1[\overline{\rho }/\overline{\alpha }]$ and let ${\tau }_2[\overline{\mu }/\overline{\beta }]$ be an instance of ${\sigma }_2$. Then $${\tau }_2[\overline{\mu }/\overline{\beta }]={\tau }_1[\overline{\rho }/\overline{\alpha }][\overline{\mu }/\overline{\beta }]={\tau }_1[\overline{\rho }[\overline{\mu }/\overline{\beta }]/\overline{\alpha }],$$ where the second equality is checked on the variables of ${\tau }_1$: a quantified ${\alpha }_i$ is sent by both sides to ${\rho }_i[\overline{\mu }/\overline{\beta }]$, and a free $\gamma \in \mathrm{ftv}({\sigma }_1)$ is fixed by $[\overline{\rho }/\overline{\alpha }]$ and then by $[\overline{\mu }/\overline{\beta }]$, since $\overline{\beta }$ avoids $\mathrm{ftv}({\sigma }_1)$. The result is an instance of ${\sigma }_1$.

($\Rightarrow$) The body ${\tau }_2$ is itself an instance of ${\sigma }_2$ (instantiate each ${\beta }_j$ by ${\beta }_j$). So ${\sigma }_1\succcurlyeq {\tau }_2$, which is the displayed condition. ◻

Proof of Corollary 4.11 — Free variables decrease with generality

Proof. Use the witnessing instance substitution from lemma 3.9. It changes only variables quantified by ${\sigma }_1$; each free variable of ${\sigma }_1$ remains free in the resulting body and is not captured by the freshly renamed prefix of ${\sigma }_2$. ◻

The freshness hypothesis prevents a bound variable of ${\sigma }_2$ from capturing a free variable of ${\sigma }_1$ while the two bodies are compared. It costs nothing: a finite quantifier prefix can always be alpha-renamed away from the finite set $\mathrm{ftv}({\sigma }_1)$.

The second immediate consequence is stability under substitution.

Proof of Lemma 3.10 — Stability of generality

Proof. Choose an alpha-equivalent representative $\sigma =\mathrm{\forall }\overline{\alpha }.{\tau }_0$ with $\overline{\alpha }$ fresh for $\mathrm{vars}(S)$, so $\sigma [S]=\mathrm{\forall }\overline{\alpha }.{\tau }_0[S]$. Let $\tau ={\tau }_0[\overline{\rho }/\overline{\alpha }]$. We claim $${\tau }_0[\overline{\rho }/\overline{\alpha }][S]={\tau }_0[S][\overline{\rho }[S]/\overline{\alpha }].$$ Check on the variables of ${\tau }_0$: each ${\alpha }_i$ goes to ${\rho }_i[S]$ on both sides ($S$ fixes ${\alpha }_i$, which is outside $\mathrm{vars}(S)$); a variable $\gamma \notin \overline{\alpha }$ goes on the left to $\gamma [S]$, and on the right to $\gamma [S][\overline{\rho }[S]/\overline{\alpha }]=\gamma [S]$, since $\mathrm{ftv}(\gamma [S])$ avoids $\overline{\alpha }$ (either $\gamma \in \mathrm{dom}(S)$ and $\mathrm{ftv}(\gamma [S])\subseteq \mathrm{ftv}(S)$, or $\gamma [S]=\gamma \notin \overline{\alpha }$). By (3.2), $\tau [S]$ is an instance of $\sigma [S]$.

For the second claim, standardize both schemes apart. Choose alpha-equivalent representatives ${\sigma }_1=\mathrm{\forall }\overline{\alpha }.{\tau }_1$ and ${\sigma }_2=\mathrm{\forall }\overline{\beta }.{\tau }_2$ whose prefixes are disjoint and avoid $\mathrm{vars}(S)$, and with $\overline{\beta }$ also fresh for $\mathrm{ftv}({\sigma }_1)$. By lemma 3.9, $${\tau }_2={\tau }_1[\overline{\rho }/\overline{\alpha }],{\tau }_2[S]={\tau }_1[S][\overline{\rho }[S]/\overline{\alpha }],$$ where the second equality is (3.2) applied to the freshened prefix $\overline{\alpha }$. Since ${\sigma }_1[S]=\mathrm{\forall }\overline{\alpha }.{\tau }_1[S]$, ${\sigma }_2[S]=\mathrm{\forall }\overline{\beta }.{\tau }_2[S]$. Moreover, $$\mathrm{ftv}({\sigma }_1[S])\subseteq (\mathrm{ftv}({\sigma }_1)\setminus \mathrm{dom}(S))\cup \mathrm{ftv}(S),$$ and $\overline{\beta }$ avoids the set on the right. Therefore lemma 3.9 applies in the converse direction. ◻

Proof of Lemma 3.11 — Quantifier introduction

Proof. Let ${\tau }^{\ast }$ be an instance of $\mathrm{\forall }\alpha .{\sigma }_2$. Choose an alpha-equivalent representative ${\sigma }_2=\mathrm{\forall }\overline{\beta }.{\tau }_2$ with $\overline{\beta }$ fresh for $\mathrm{ftv}({\sigma }_1)$, for $\alpha$, and for the finitely many variables of ${\tau }^{\ast }$; then ${\tau }^{\ast }={\tau }_2[\mu /\alpha ,\overline{\mu }/\overline{\beta }]$ for some $\mu ,\overline{\mu }$ with $\overline{\beta }\cap \mathrm{ftv}(\mu )=\varnothing$. Put $S:=[\mu /\alpha ]$. Then $${\tau }^{\ast }={\tau }_2[S][\overline{\mu }/\overline{\beta }],$$ checked on the variables of ${\tau }_2$ as before, using $\overline{\beta }\cap \mathrm{ftv}(\mu )=\varnothing$. So ${\tau }^{\ast }$ is an instance of ${\sigma }_2[S]$; by lemma 3.10, ${\sigma }_1[S]⊒{\sigma }_2[S]$, and ${\sigma }_1[S]={\sigma }_1$ because $\alpha \notin \mathrm{ftv}({\sigma }_1)$. Hence ${\tau }^{\ast }$ is an instance of ${\sigma }_1$. ◻

Generalization

A scheme records which parts of a type a definition does not depend on. Generalization quantifies exactly the variables of the inferred monotype that the context does not fix.

The exclusion of $\mathrm{ftv}(\mathrm{\Gamma })$ is the entire content. The tempting simpler operation—quantify all variables of $\tau$—breaks the connection between a variable’s occurrences inside $\tau$ and its occurrences in the surrounding assumptions. For example, under $\mathrm{\Gamma }=f:\alpha \to \beta$, the naive result $${\mathrm{Gen}}_{\mathrm{\Gamma }}^{?}(\alpha \to \beta )=\mathrm{\forall }\alpha \beta .\alpha \to \beta$$ would let two uses of the same $f$ instantiate its domain and codomain differently. The context declares $f:\alpha \to \beta$ once, so both uses must instantiate that same monotype. Therefore define the quantified set as $\mathrm{ftv}(\tau )\setminus \mathrm{ftv}(\mathrm{\Gamma })$; neither $\alpha$ nor $\beta$ is quantified in the example.

If $\mathrm{ftv}(\mathrm{\Gamma })\subseteq \mathrm{ftv}({\mathrm{\Gamma }}^{\prime })$, then the variables quantified by ${\mathrm{Gen}}_{{\mathrm{\Gamma }}^{\prime }}(\tau )$ form a subset of those quantified by ${\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau )$, and therefore $${\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau )⊒{\mathrm{Gen}}_{{\mathrm{\Gamma }}^{\prime }}(\tau ).$$ For a substitution $S$, alpha-freshening the surviving quantified variables away from $S$ gives $${\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau )[S]⊒{\mathrm{Gen}}_{\mathrm{\Gamma }[S]}(\tau [S]).$$

A context with more free type variables pins down more of $\tau$ and therefore permits fewer quantifiers. This is why the generality arrow in the next lemma points from ${\mathrm{Gen}}_{\mathrm{\Gamma }}$ to ${\mathrm{Gen}}_{{\mathrm{\Gamma }}^{\prime }}$, not conversely.

Proof of Lemma 3.13 — Monotonicity

Proof. Write ${\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau )=\mathrm{\forall }\overline{\alpha }.\tau$ and ${\mathrm{Gen}}_{{\mathrm{\Gamma }}^{\prime }}(\tau )=\mathrm{\forall }\overline{\beta }.\tau$; then $\overline{\beta }\subseteq \overline{\alpha }$, and $\overline{\beta }$ avoids $\mathrm{ftv}({\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau ))\subseteq \mathrm{ftv}(\mathrm{\Gamma })$. The identity substitution on $\overline{\alpha }$ exhibits the condition of lemma 3.9. ◻

Proof of Lemma 3.14 — Generalization under substitution

Proof. Let $\overline{\alpha }=\mathrm{ftv}(\tau )\setminus \mathrm{ftv}(\mathrm{\Gamma })$ and choose fresh variables ${\overline{\alpha }}^{\prime }$ avoiding $\mathrm{vars}(S)\cup \mathrm{ftv}(\mathrm{\Gamma })\cup \mathrm{ftv}(\tau )$. With $\pi :=[{\overline{\alpha }}^{\prime }/\overline{\alpha }]$ and $T:=\pi ;S$, $${\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau )[S]=\mathrm{\forall }{\overline{\alpha }}^{\prime }.\tau [T],$$ by the definition of substitution on schemes. Now let $\tau [S][\overline{\mu }/\overline{\beta }]$ be an arbitrary instance of ${\mathrm{Gen}}_{\mathrm{\Gamma }[S]}(\tau [S])$, where $\overline{\beta }=\mathrm{ftv}(\tau [S])\setminus \mathrm{ftv}(\mathrm{\Gamma }[S])$. Define a further substitution $N$ on the primed prefix by ${\alpha }_i^{\prime }[N]:={\alpha }_i[S][\overline{\mu }/\overline{\beta }]$. We claim $$\tau [T][N]=\tau [S][\overline{\mu }/\overline{\beta }],$$ which exhibits the instance as an instance of ${\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau )[S]$ and finishes the proof. Check the claim on each $\gamma \in \mathrm{ftv}(\tau )$ using (3.1). If $\gamma ={\alpha }_i\in \overline{\alpha }$: the left side gives ${\alpha }_i[T][N]={\alpha }_i^{\prime }[S][N]={\alpha }_i^{\prime }[N]$ (as ${\alpha }_i^{\prime }$ is fresh for $S$), which is ${\alpha }_i[S][\overline{\mu }/\overline{\beta }]$, the right side at ${\alpha }_i$. If $\gamma \notin \overline{\alpha }$, then $\gamma \in \mathrm{ftv}(\mathrm{\Gamma })$, so $\mathrm{ftv}(\gamma [S])\subseteq \mathrm{ftv}(\mathrm{\Gamma }[S])$, which avoids $\overline{\beta }$; hence the right side fixes $\gamma [S]$, while the left side gives $\gamma [T][N]=\gamma [S][N]=\gamma [S]$, since $\mathrm{ftv}(\gamma [S])$ contains no primed variable. ◻

Standardizing the variables to be generalized apart before substitution produces a context-equivalent substitution $T$ for which generalization recovers the renamed prefix. This is the converse-looking companion to lemma 3.14: that lemma fixes $S$, so generalization can become less general, whereas the fresh renaming below changes $S$ away from the context while preserving its action on the context.

Proof of Lemma 3.15 — Fresh renaming before substitution

Proof. Take $\overline{\alpha }$, ${\overline{\alpha }}^{\prime }$, $\pi$, and $T=\pi ;S$ as in the proof of lemma 3.14. Claim 1 holds because $\pi$ fixes $\mathrm{ftv}(\mathrm{\Gamma })$. For claim 2, we saw ${\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau )[S]=\mathrm{\forall }{\overline{\alpha }}^{\prime }.\tau [T]$. Every ${\alpha }_i^{\prime }$ is free in $\tau [T]$ (it is ${\alpha }_i[T]$ with ${\alpha }_i\in \mathrm{ftv}(\tau )$, by (3.1)) and is absent from $\mathrm{ftv}(\mathrm{\Gamma }[S])\subseteq \mathrm{ftv}(\mathrm{\Gamma })\cup \mathrm{ftv}(S)$ by freshness. Hence the prefix of ${\mathrm{Gen}}_{\mathrm{\Gamma }[S]}(\tau [T])$ contains all of ${\overline{\alpha }}^{\prime }$, possibly more, and an instance of $\mathrm{\forall }{\overline{\alpha }}^{\prime }.\tau [T]$ becomes an instance of ${\mathrm{Gen}}_{\mathrm{\Gamma }[S]}(\tau [T])$ by instantiating the extra quantified variables by themselves. ◻

The declarative system

The asymmetry between Lam and Let is the design. A $\lambda$-bound variable stands for an argument that will arrive at run time from an unknown caller, so its type is a single (possibly variable-containing) monotype, recorded in the context and visible to the side condition of Gen. A $\mathsf{let}$-bound variable stands for a definition that is textually present, so the system may first close over everything the context does not fix (Gen), attach the resulting scheme, and let every use instantiate it independently (Inst).

Proof of Lemma 3.18 — Weakening

Proof. First alpha-rename every variable bound by a Gen step away from the finite set $\mathrm{ftv}(\mathrm{\Delta })$. Then induct on the derivation. Variable membership persists under extension, every term-forming rule reuses its induction hypotheses, and each Gen side condition remains true because its quantified variable occurs in neither $\mathrm{\Gamma }$ nor $\mathrm{\Delta }$. ◻

Proof of Lemma 3.19 — Term substitution

Proof. Induct on the second derivation after freshening all term binders away from $x$ and the free variables of $a$. At a Var leaf for $x$, use the first premise; at any other variable, reuse the declaration from $\mathrm{\Gamma }$. Rules Inst and Gen reapply directly. In the latter case its side condition says that the quantified type variable is absent from $\mathrm{ftv}(\mathrm{\Gamma },x:\sigma )$, hence also from $\mathrm{ftv}(\mathrm{\Gamma })$ after $x$ is discharged. Lambda and application follow from their induction hypotheses, using lemma 3.18 to carry the first premise under a newly bound variable. The let case is the same: weaken the typing of $a$ under the let binder, apply the induction hypothesis to both premises, and reapply Let. If that binder is also called $x$, freshen it first as permitted by convention 3.2. ◻

Now the boundary case. Why can a $\lambda$-bound variable not be used at two types? Suppose we try to type $\lambda f.e$ so that $f$ is applied to $\mathsf{zero}$ and to $\mathsf{true}$ inside $e$. Rule Lam forces a context $\mathrm{\Gamma },f:{\tau }_f$ with one monotype ${\tau }_f$; inside the body, any attempt to apply Gen to a variable of ${\tau }_f$ is blocked by the side condition. For example, from $\mathrm{\Gamma },f:\alpha \to \beta ⊢f:\alpha \to \beta$ one would need $$\alpha \notin \mathrm{ftv}(\mathrm{\Gamma },f:\alpha \to \beta )$$ to introduce $\mathrm{\forall }\alpha$, but the displayed condition is false because $\alpha$ occurs in the declaration of $f$. Hence Gen does not apply. So both uses of $f$ must share the single monotype ${\tau }_f$, and no monotype is simultaneously an arrow out of $\mathsf{Nat}$ and an arrow out of $\mathsf{Bool}$. Indeed, inversion on the two application derivations would give ${\tau }_f=\mathsf{Nat}\to A$ and ${\tau }_f=\mathsf{Bool}\to B$ for some monotypes $A,B$. Injectivity of the arrow constructor would then give $\mathsf{Nat}=\mathsf{Bool}$, contradicting disjointness of type constructors.

From programs to equations

The declarative system says which typings are derivable; it does not compute one. In example 3.17 the derivation contains chosen instances. Constraint generation instead assigns fresh unknowns and records the equations forced by typing rules. Its representative input is the twice-application combinator: $$\mathsf{twice}:=\lambda f.\lambda x.f(fx).$$

This constraint generator is not Algorithm W: it collects the complete list and solves it once. The batch output is therefore an equation list and a solution, not the pair of a threaded substitution and monotype returned by W.

Build the derivation from the outside in, under ${\mathrm{\Gamma }}_0$. Rule C-Lam binds $f$ at an unknown monotype ${\alpha }_f$ and then $x$ at an unknown ${\alpha }_x$; the working context is $\mathrm{\Gamma }:={\mathrm{\Gamma }}_0,f:{\alpha }_f,x:{\alpha }_x$. The body is $f(fx)$, an application, so C-App demands that the type of the function part be an arrow whose domain is the type of the argument part. Working on the inner application $fx$ first: $f$ has type ${\alpha }_f$ (C-Var); $x$ has type ${\alpha }_x$; C-App applies only if ${\alpha }_f$ is an arrow with domain ${\alpha }_x$. We do not know that; we record it, inventing a fresh unknown ${\beta }_1$ for the codomain: $${\alpha }_f\doteq {\alpha }_x\to {\beta }_1,\text{giving}\mathrm{\Gamma }{⊢}_{\mathrm{c}}fx:{\beta }_1\mid ({\alpha }_f\doteq {\alpha }_x\to {\beta }_1).$$ The outer application $f(fx)$ likewise demands that ${\alpha }_f$ be an arrow with domain ${\beta }_1$; invent ${\beta }_2$: Discharging the two C-Lam steps, the whole term has type ${\alpha }_f\to {\alpha }_x\to {\beta }_2$, provided the equation set $$E_{\mathsf{twice}}:=({\alpha }_f\doteq {\alpha }_x\to {\beta }_1,{\alpha }_f\doteq {\beta }_1\to {\beta }_2)$$ has a solution: a substitution making both equations literal identities. After applying a solution $S$, the two right-hand sides must coincide: $$({\alpha }_x\to {\beta }_1)[S]=({\beta }_1\to {\beta }_2)[S].$$ By injectivity of $\to$, $${\alpha }_x[S]={\beta }_1[S],{\beta }_1[S]={\beta }_2[S].$$ Taking $S=[{\alpha }_x/{\beta }_1,{\alpha }_x/{\beta }_2,({\alpha }_x\to {\alpha }_x)/{\alpha }_f]$ solves $E_{\mathsf{twice}}$ and turns the conditional typing into an actual derivation of $${\mathrm{\Gamma }}_0⊢\mathsf{twice}:({\alpha }_x\to {\alpha }_x)\to {\alpha }_x\to {\alpha }_x,$$ and one Gen, alpha-renaming the quantified ${\alpha }_x$ to $\alpha$ for display, yields the scheme $\mathrm{\forall }\alpha .(\alpha \to \alpha )\to \alpha \to \alpha$.

Was the solution forced? Not entirely. The substitution $$S^{\prime }=[\mathsf{Nat}/{\alpha }_x,\mathsf{Nat}/{\beta }_1,\mathsf{Nat}/{\beta }_2,(\mathsf{Nat}\to \mathsf{Nat})/{\alpha }_f]$$ also solves $E_{\mathsf{twice}}$ and yields the less useful $(\mathsf{Nat}\to \mathsf{Nat})\to \mathsf{Nat}\to \mathsf{Nat}$. Demand 3 of the introduction is exactly the demand that we always take the most general solution, of which every other is a substitution instance. The remaining problem is to construct such a solution whenever the equation set is solvable.

Now a failure. Consider the self-application $\lambda t.tt$. Binding $t$ at an unknown $\gamma$, the application $tt$ demands that $\gamma$ be an arrow with domain $\gamma$: $$\gamma \doteq \gamma \to \delta .$$ No substitution can solve this: applying any $S$ makes the right side an arrow one of whose immediate subtrees is the left side, and a finite tree cannot be a proper subtree of itself. Repeating that subtree occurrence would produce an infinite descending path in a finite tree. Note precisely what failed. If $t$ were $\mathsf{let}$-bound to $\mathsf{twice}$, each of the two occurrences would receive its own instance of the scheme of $\mathsf{twice}$, and no single $\gamma$ would be forced to equal an arrow over itself; the let-bound term therefore generates distinct variables for its two occurrences. The $\lambda$-bound version shares one monotype and dies on the equation above.

The unifier’s contract on an equation list $E$ is exact: success returns a substitution that satisfies every equation and through which every other such substitution factors on the variables occurring in $E$. Failure means that no satisfying substitution exists. The notation and the lexicographic triple of natural numbers that decreases at every recursive call are fixed below.

Unification

Unification solves finite equations between constructor trees. Constructor injectivity justifies decomposition, constructor disjointness justifies a head clash, and finiteness of the trees justifies the occurs check. No property specific to the arrow constructor is used.

Proof of Lemma 3.21 — Occurs check

Proof. The occurrence of $\alpha$ in $\tau$ is proper, so for every substitution $S$, the finite tree $\alpha [S]$ occurs as a proper subtree of $\tau [S]$. If $\alpha [S]=\tau [S]$, a finite tree would be a proper subtree of itself. Equivalently, following the proper-subtree occurrence repeatedly would give an infinite descending path through one finite tree. Both are impossible. ◻

Proof of Lemma 3.24 — Termination

Proof. Orientation is a finite preprocessing step and makes no recursive call. Order the arguments of recursive calls lexicographically by $$(|\mathrm{vars}(E)|,\text{total number of constructor nodes in }E,|E|).$$ Elimination removes $\alpha$ from every remaining equation; the occurs condition ensures that substituting $\tau$ cannot put it back, so the first component decreases. Decomposition removes the two equal outer constructor nodes and preserves the variables, so the second component decreases. Deleting a reflexive equation cannot increase either of the first two components. If the variable count drops, the first component decides the comparison; if it is unchanged but constructor nodes drop, the second does. Only when both are unchanged is the shorter equation list needed. Thus the triple decreases in the delete case as well. Delete, decompose, and eliminate exhaust the recursive clauses; the lexicographic order on triples of natural numbers is well founded. ◻

Proof of Lemma 3.25 — Elimination factorization

Proof. If $S$ solves the displayed equation, then $\alpha [S]=\tau [S]$. Hence, on $\alpha$, $\alpha [R;S]=\tau [S]=\alpha [S]$, while on every $\gamma \ne \alpha$, $\gamma [R;S]=\gamma [S]$. Thus $S=R;S$ on all problem variables. Applying this equality to both sides of each equation in $E$ shows $S\vDash E[R]$.

Conversely, $\alpha [R]=\tau =\tau [R]$, the last equality using $\alpha \notin \mathrm{ftv}(\tau )$. Thus every substitution after $R$ solves $\alpha \doteq \tau$. If $S=R;S$ on the problem variables and $S\vDash E[R]$, then $S$ also solves every equation of $E$: for each side $\rho$ occurring in $E$, agreement on the problem variables gives $\rho [S]=\rho [R;S]=\rho [R][S]$, and the equation in $E[R]$ identifies the final expressions. ◻

Proof of Theorem 3.26 — Unification is sound and principal

Proof. Induct according to the terminating recursion of lemma 3.24.

We prove both support assertions in item 3 simultaneously. U-Done returns the identity, through which every substitution factors. U-Delete preserves exactly the same solutions. Its recursive variable set is a subset of the old one; the recursive support assertions therefore fix any variable lost with the deleted equation and introduce no new one. For U-Decompose, injectivity of the common constructor says that a substitution solves the old head equation iff it solves every new component equation; the two problems have the same variables, so both assertions pass through the recursive call. Orientation also preserves the variable set. A head-constructor clash has no solution by disjointness. The occurs-check failure has no solution by lemma 3.21.

It remains to examine U-Eliminate. Its three obligations are $$\text{solution transport},\text{factor extension},\text{support preservation}.$$ Put $R=[\tau /\alpha ]$ and suppose the recursive call returns an MGU $U$ of $E[R]$. By lemma 3.25, $R;U$ solves the original problem. Let $S$ be any other solution. The same lemma gives $S\vDash E[R]$ and $S=R;S$ on the old problem variables. Since $U$ is most general for $E[R]$, there is $T_0$ with $S=U;T_0$ on its variables. Extend $T_0$ to a substitution $T$ by setting $\gamma [T]=\gamma [S]$ for each $\gamma \in \mathrm{ftv}(\tau )\setminus \mathrm{vars}(E[R])$. The recursive support assertions say that $U$ fixes those added variables and that none of them occurs in $\delta [U]$ for $\delta \in \mathrm{vars}(E[R])$. Thus changing $T_0$ there does not disturb the old factorization, and now $S=U;T$ on $\mathrm{vars}(E[R])\cup \mathrm{ftv}(\tau )$. Every old variable other than $\alpha$ lies in that union. Therefore, for every old variable $\gamma \ne \alpha$, $\gamma [R]=\gamma$, hence $\gamma [S]=\gamma [R][U;T]$. For $\alpha$, $$\alpha [R][U;T]\stackrel{definitionofR}{=}\tau [U;T]\stackrel{factorizationon\mathrm{ftv}(\tau )}{=}\tau [S]\stackrel{S\vDash \alpha \doteq \tau }{=}\alpha [S];$$ the middle equality follows from the extended factorization on $\mathrm{ftv}(\tau )$. Thus $S=R;U;T$ on the original problem variables, proving that $R;U$ is most general. This also proves that failure of the recursive call implies failure of the original problem. Finally, $R$ changes only $\alpha$ and introduces only variables already in the original problem. The recursive result fixes variables outside $\mathrm{vars}(E[R])$ and introduces no outside variable in the image of a recursive problem variable. Hence $R;U$ fixes every variable outside $\mathrm{vars}(E)$ and maps each old problem variable to a type using only old problem variables. This proves both remaining support assertions. ◻

Proof of Corollary 4.31 — Mutual factorization of most general unifiers

Proof. Because $V$ is a solution and $U$ is most general, there is $R$ with $V{=}_{\mathrm{vars}(E)}U;R$. Interchanging $U$ and $V$ gives the reverse factorization. Thus the two represent the same element of the solution preorder. No uniqueness-up-to-renaming conclusion follows: that stronger statement would require an extra rule choosing one printed substitution from each mutually factoring class. ◻

Algorithm W

Constraint generation and unification can now be fused. The fusion matters: after inferring the function part of an application, its substitution must be applied to the context before the argument is inferred. Otherwise the two walks can assign incompatible meanings to the same context variable.

The unthreaded attempt already fails on $\mathsf{twice}$. After the inner application has learned $U_1=[\beta \to \gamma /\alpha ]$, suppose the outer application still uses the stale $\alpha$. It solves $$\alpha \doteq \gamma \to \delta$$ independently of $\alpha \doteq \beta \to \gamma$; the returned result then leaves $\delta$ unconstrained and suggests the spurious type $(\beta \to \gamma )\to \beta \to \delta$. Applying $U_1$ before the second walk instead forces $\beta \to \gamma =\gamma \to \delta$, hence one common type. The let clause needs the same threading: generalizing over stale $\mathrm{\Gamma }$ could quantify a variable that the first substitution has already fixed in $\mathrm{\Gamma }[S_1]$.

Diagram

In the upper row of figure 4.1, the argument is checked in $\mathrm{\Gamma }[S_1]$, the function result is updated once more to ${\tau }_1[S_2]$, and $U$ solves ${\tau }_1[S_2]\doteq {\tau }_2\to \beta$. In the lower row, the same $S_1$ first updates the context used by generalization; the body then sees exactly $\mathrm{\Gamma }[S_1],x:\sigma$. The diagram records these two equalities and does not replace any clause of definition 3.28.

Proof of Lemma 4.35 — Completion of a finite name matching

Proof. Draw the finite directed graph on $A\cup B$, where $A=\{a_1,\dots ,a_n\}$ and $B=\{b_1,\dots ,b_n\}$, with one edge $a_i\to b_i$ for each $i$. Every vertex has at most one outgoing and at most one incoming edge because both lists have no repetitions. Each nontrivial connected component is therefore a directed cycle or a directed path. Keep every cycle. For each path, add one edge from its terminal vertex to its initial vertex. Fix every variable outside $A\cup B$. The resulting map has exactly one incoming and one outgoing edge at every vertex of $A\cup B$, agrees with every prescribed pair, and is the identity off that finite set. Since $F\cap (A\cup B)=\varnothing$, it fixes $F$. ◻

Proof of Lemma 3.29 — Fresh-choice irrelevance

Proof. First induct on the unification recursion. For every finite bijection $\pi$, renaming preserves the selected clause and $$\mathsf{unify}(E[\pi ])={\pi }^{-1};U;\pi \text{when}\mathsf{unify}(E)=U;$$ it also preserves both failure clauses. Renaming preserves constructor heads, reflexivity, and the occurs test. In U-Eliminate, the required calculation is $$[\rho [\pi ]/\alpha [\pi ]]={\pi }^{-1};[\rho /\alpha ];\pi .$$ The equations left after applying the current elimination substitution form the residual equation problem. The induction hypothesis applies to this renamed residual equation problem, and associativity assembles the returned composites.

The W induction is strengthened over arbitrary unconsumed suffixes of the two supplies and carries the ordered partial matching of variables consumed so far. At each allocation, append the pair of next variables. Injectivity of each supply keeps the matching one-to-one, and disjointness from $\mathrm{ftv}(\mathrm{\Gamma })$ keeps its domain and range away from the input variables. Whenever a total renaming is needed, complete the matching by lemma 4.35. A later completion agrees on every pair already prescribed, while later supply variables are absent from the current contexts, types, and equations; changing the closing edges therefore does not change an established equality. In the variable case, instantiation consumes corresponding finite prefixes, so structural substitution gives the claimed renamed type and the identity conjugacy equation. In the lambda case, extend the bijection by the binder pair and apply the induction hypothesis to the body under the two renamed contexts.

For application, the first induction hypothesis gives $S_1^{\prime }={\pi }^{-1};S_1;\pi$ and ${\tau }_1^{\prime }={\tau }_1[\pi ]$. Its unconsumed suffixes, rather than the original supplies, are passed to the argument calls; the second induction hypothesis therefore extends the same $\pi$ and gives the corresponding equations for $S_2$ and ${\tau }_2$. Pair the result variables next. The two application equations are related by $\pi$, so unification equivariance gives $U^{\prime }={\pi }^{-1};U;\pi$. Associativity then yields $$S_1^{\prime };S_2^{\prime };U^{\prime }={\pi }^{-1};(S_1;S_2;U);\pi .$$ It also shows that unification succeeds or fails in both runs.

For let, the definition of generalization gives $${\mathrm{Gen}}_{\mathrm{\Gamma }[S_1]}({\tau }_1)[\pi ]{=}_{\alpha }{\mathrm{Gen}}_{\mathrm{\Gamma }[S_1][\pi ]}({\tau }_1[\pi ]),$$ because $\pi$ carries the set difference of free variables bijectively to the set difference on the right. The body induction applies to these alpha-equivalent extended contexts and to the two unconsumed suffixes. This proves the three displayed conclusions on the input variables and the finite set of consumed names in every successful clause. Only finitely many names are consumed by a finite term. Apply lemma 4.35 to the two consumed prefixes. Its permutation agrees with every prescribed pair and fixes $\mathrm{ftv}(\mathrm{\Gamma })$; variables outside the prefixes occur in neither execution. The preceding equations therefore hold for this completed permutation. The same lockstep induction, stopped at the failing clause, proves corresponding failure. ◻

The application clause is best read as a derivation. The first call says $e_1$ has provisional type ${\tau }_1$ after $S_1$. The second call may learn more, so it sees $\mathrm{\Gamma }[S_1]$ and changes the function type to ${\tau }_1[S_2]$. A fresh $\beta$ stands for the result. Unification enforces $${\tau }_1[S_2]={\tau }_2\to \beta ,$$ and its substitution $U$ is applied to every accumulated answer.

The syntax-directed judgment

Proof of Lemma 3.32 — Type substitution

Proof. For the declarative judgment, induct on the derivation. Before a Gen case, alpha-rename its quantified variable away from $\mathrm{vars}(S)$. The side condition then remains true after applying $S$, and Gen rebuilds the conclusion. Inst uses lemma 3.10. Every other case applies $S$ to all monotypes in the displayed rule.

The syntax-directed assertion needs one extra piece of bookkeeping at a let. First standardize the finite derivation apart: whenever an S-Let premise has inferred type ${\tau }_1$, rename the variables in $$G=\mathrm{ftv}({\tau }_1)\setminus \mathrm{ftv}(\mathrm{\Gamma })$$ away from $\mathrm{vars}(S)$ and from all variables used outside that premise. These variables are bound by ${\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_1)$ in the body context, so this changes only the representative of that scheme and the matching first-premise derivation; it changes neither the surrounding context nor the conclusion.

Now induct on the standardized derivation. Variable, lambda, and application cases use instance stability and the induction hypotheses. In the let case the freshness of $G$ gives the alpha-equality $${\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_1)[S]{=}_{\alpha }{\mathrm{Gen}}_{\mathrm{\Gamma }[S]}({\tau }_1[S]).$$ Indeed, $S$ fixes every member of $G$, and every other free variable of ${\tau }_1$ occurs in $\mathrm{\Gamma }$, so all variables introduced by its image under $S$ occur in $\mathrm{\Gamma }[S]$ and are not generalized. The two induction hypotheses therefore produce exactly the premises of S-Let, with the body declaration identified by (3.3). ◻

Proof of Lemma 3.33 — More general contexts

Proof. Induct on the syntax-directed derivation. In S-Var, transitivity of $⊒$ replaces the old declaration. Lambda and application are immediate. More-general schemes have no additional free variables (corollary 4.11), so $\mathrm{ftv}(\mathrm{\Gamma })\subseteq \mathrm{ftv}({\mathrm{\Gamma }}^{\prime })$. Hence $${\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_1)⊒{\mathrm{Gen}}_{{\mathrm{\Gamma }}^{\prime }}({\tau }_1)$$ by lemma 3.13. In the let case, context monotonicity replaces the latter declaration by the former before applying the induction hypothesis to the body. Every case replaces only declarations and reapplies the same final rule, so the derivation height is unchanged. ◻

Proof of Theorem 3.34 — Declarative and syntax-directed typing agree

Proof. From right to left, replace S-Var by Var followed by Inst. In S-Let, obtain $\mathrm{\Gamma }⊢e_1:{\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_1)$ by applying Gen once for every generalized variable, then use Let. The other rules are already declarative rules.

For the converse, normalize a declarative derivation by induction on its last rule, proving the stronger statement about schemes. At a Var leaf, present the declared scheme as $\mathrm{\forall }\overline{\alpha }.{\tau }_0$ and replace its prefix by fresh variables $\overline{\beta }$ absent from $\mathrm{\Gamma }$. Rule S-Var gives the monotype ${\tau }_0[\overline{\beta }/\overline{\alpha }]$, whose generalization over $\mathrm{\Gamma }$ is alpha-equivalent to the declared scheme. Inst composes the old generality witness with its premise $\sigma ⊒{\sigma }^{\prime }$. In a Gen case, lemma 3.11 adds the quantified variable to the target scheme; its freshness follows from the rule side condition.

For Lam, the induction output for the premise has some result $\rho$ with ${\mathrm{Gen}}_{\mathrm{\Gamma },x:{\tau }_1}(\rho )⊒{\tau }_2$. Choose its witnessing instance substitution $Q$, so $\rho [Q]={\tau }_2$. The domain of $Q$ consists of variables generalized over the premise context, hence $Q$ fixes that context. The syntax-directed part of lemma 3.32 gives the required premise at ${\tau }_2$, and S-Lam applies. In an application, the two premise outputs may be specialized to the rule’s displayed monotypes ${\tau }_2\to \tau$ and ${\tau }_2$: standardize their generalized variables apart, take the two witnesses from lemma 3.9, apply lemma 3.32 separately, and then apply S-App. Each witness has domain among variables generalized over $\mathrm{\Gamma }$, hence fixes $\mathrm{\Gamma }$; standardizing the two domains apart therefore leaves both specialized premises under the same context $\mathrm{\Gamma }$.

For Let, let the induction output for its first premise be $$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_1:{\rho }_1,{\mathrm{Gen}}_{\mathrm{\Gamma }}({\rho }_1)⊒\sigma .$$ The second induction output is initially under $\mathrm{\Gamma },x:\sigma$. By lemma 3.33, replace that declaration by the more-general ${\mathrm{Gen}}_{\mathrm{\Gamma }}({\rho }_1)$ and apply S-Let. Its result type is the body output ${\rho }_2$. Finally, lemma 3.13 gives $${\mathrm{Gen}}_{\mathrm{\Gamma }}({\rho }_2)⊒{\mathrm{Gen}}_{\mathrm{\Gamma },x:\sigma }({\rho }_2),$$ so the body’s induction witness composes to the required witness for the let conclusion. When that conclusion is already a monotype, specialize the final syntax-directed derivation exactly as in the lambda case. ◻

Proof of Theorem 4.43 — Pure HM safety

Proof. For preservation, first use theorem 3.34 to replace the declarative monotype derivation by a syntax-directed one. Induct on the step derivation. At each compatible frame, inversion of the syntax-directed derivation exposes the child typing. Translate that child to declarative typing, apply the induction hypothesis, translate the result back, and rebuild the unique syntax-directed rule for the frame. At beta, inversion gives $\mathrm{\Gamma },x:{\tau }_1⊢b:{\tau }_2$ and $\mathrm{\Gamma }⊢v:{\tau }_1$; at let, it gives $\mathrm{\Gamma }⊢v:\sigma$ and $\mathrm{\Gamma },x:\sigma ⊢e:\tau$. In both root cases lemma 3.19 types the contractum. Finally translate the rebuilt syntax-directed derivation to the claimed declarative judgment.

For progress, translate to syntax-directed typing and induct on that derivation. An abstraction is a value. In an application, first step the function, then the argument; when both are values, the value grammar forces the function to be an abstraction, so beta applies. In a let, step its definition or, when that definition is a value, contract the let. The variable case is impossible under the empty context. ◻

The progress clause is restricted to the closed, constant-free base language. For every diagnostic under ${\mathrm{\Gamma }}_0$, extend the value grammar by the primitive function $\mathsf{succ}$, the Boolean constants, and the numeral judgment $$\frac{\phantom{X}}{\mathsf{zero}\mathsf{num}}\mathrm{N}-\mathrm{Z}\frac{n\mathsf{num}}{\mathsf{succ}n\mathsf{num}}\mathrm{N}-\mathrm{S}.$$ Numerals and Booleans are final values. Thus $\mathsf{succ}n$ is final exactly when $n\mathsf{num}$; no value or contraction rule applies to $\mathsf{succ}\mathsf{true}$, so that closed term is stuck. Thus the primitive signature itself distinguishes $\mathsf{Nat}$ from $\mathsf{Bool}$: the former admits $\mathsf{succ}$, while the latter does not.

Correctness and principal types

Proof of Theorem 3.35 — Soundness of W

Proof. Induct on $e$, following definition 3.28.

For a variable, $\mathsf{fresh}(\mathrm{\Gamma }(x))$ is an instance of its scheme, so Var followed by Inst applies. In the lambda case the induction hypothesis is $$\mathrm{\Gamma }[S],x:\alpha [S]⊢e:\tau ;$$ Lam gives the returned type $\alpha [S]\to \tau$.

For $e_1{e}_2$, the induction hypotheses give $$\mathrm{\Gamma }[S_1]⊢e_1:{\tau }_1,\mathrm{\Gamma }[S_1;S_2]⊢e_2:{\tau }_2.$$ Apply lemma 3.32 with $S_2$ to the first derivation and then with $U$ to both. Since $U$ solves W’s equation ${\tau }_1[S_2]\doteq {\tau }_2\to \beta$, $${\tau }_1[S_2;U]={\tau }_2[U]\to \beta [U].$$ Rule App therefore returns $\beta [U]$ under $\mathrm{\Gamma }[S_1;S_2;U]$.

For a let, the first induction hypothesis and repeated Gen give $$\mathrm{\Gamma }[S_1]⊢e_1:\sigma ,\sigma ={\mathrm{Gen}}_{\mathrm{\Gamma }[S_1]}({\tau }_1).$$ Apply type substitution $S_2$ to this declarative derivation, obtaining $$\mathrm{\Gamma }[S_1;S_2]⊢e_1:\sigma [S_2].$$ The second induction hypothesis is $$\mathrm{\Gamma }[S_1;S_2],x:\sigma [S_2]⊢e_2:{\tau }_2.$$ These are precisely the two premises of declarative Let. The returned context and type are $\mathrm{\Gamma }[S_1;S_2]$ and ${\tau }_2$. ◻

Proof of Lemma 4.45 — Extending an MGU factorization off its problem

Proof. For each $\gamma \in P\setminus \mathrm{vars}(E)$ set $\gamma [R]:=\gamma [Q]$ and retain $R$ elsewhere. The unifier fixes every variable outside its equation problem by theorem 3.26(3), so $\gamma [U;R]=\gamma [R]=\gamma [Q]$ there. On $\mathrm{vars}(E)$ the original factorization is unchanged. ◻

The protected set has a concrete role even in a one-node application. Take $\mathrm{\Gamma }={\mathrm{\Gamma }}_0,f:\alpha$, the term $f\mathsf{zero}$, and protect $P=\{\alpha \}$. Suppose the target specialization is $T=[\mathsf{Nat}\to \mathsf{Bool}/\alpha ]$. Both recursive calls return the identity; the application equation has MGU $U=[\mathsf{Nat}\to \beta /\alpha ]$, and the residual $R=[\mathsf{Bool}/\beta ]$ satisfies $$T{=}_{\{\alpha \}}U;R,\beta [R]=\mathsf{Bool}.$$ Protecting $\alpha$ is exactly what retains this equality after the recursive calls have returned.

For a substitution $Q$ and a finite set $P$, write $${\mathrm{fv}}_Q(P):=\bigcup _{\gamma \in P}\mathrm{ftv}(\gamma [Q]).$$ This is the set of variables in the $Q$-images of $P$; the parenthesized subscript is not substitution or term instantiation.

Proof of Lemma 4.46 — Protected principal-pair induction

Proof. Induct on the height of the syntax-directed derivation under $\mathrm{\Gamma }[T]$, generalized over $\mathrm{\Gamma },T,P$, while maintaining both the displayed factorization and agreement on $P$. By lemma 3.29, every generated variable lies outside $\mathrm{ftv}(\mathrm{\Gamma })\cup P$. Extend each MGU factor outside its equation variables by lemma 4.45. In the application case, protect ${\mathrm{fv}}_{S_1}(P)\cup \mathrm{ftv}({\tau }_1)$ during the second recursive call. Its factor then satisfies $${\tau }_1[S_2;R_2]={\tau }_1[R_1],$$ so the target substitution solves W’s final application equation.

Variable. The target ${\tau }^{\prime }$ is an instance of $\mathrm{\Gamma }[T](x)$, while W’s $\tau$ replaces the quantified prefix of $\mathrm{\Gamma }(x)$ by variables fresh for $T$ and $\mathrm{\Gamma }$. Extend $T$ by sending those fresh variables to the monotypes used in the target instance. The resulting $R$ agrees with $T$ on $\mathrm{ftv}(\mathrm{\Gamma })$. Because the generated variables avoid $P$ and W’s variable substitution is the identity, extend $R$ by $\gamma [R]=\gamma [T]$ for the remaining $\gamma \in P$; this does not change $\tau [R]$ and gives the protected agreement. Thus ${\tau }^{\prime }=\tau [R]$.

Abstraction. The target derivation has a premise $\mathrm{\Gamma }[T],x:{\rho }_1{⊢}_{\mathrm{s}}{e}_0:{\rho }_2$ and ${\tau }^{\prime }={\rho }_1\to {\rho }_2$. W chose fresh $\alpha$. Extend $T$ by $\alpha \mapsto {\rho }_1$ and apply the induction hypothesis to the recursive call on $\mathrm{\Gamma },x:\alpha$. It gives $R$ with ${\rho }_2={\tau }_0[R]$ and, because $\alpha$ occurs in the enlarged context, ${\rho }_1=\alpha [S;R]$. Hence $${\tau }^{\prime }={\rho }_1\to {\rho }_2=(\alpha [S]\to {\tau }_0)[R],$$ the returned lambda type.

Application. The target derivation has an intermediate type $\rho$: $\mathrm{\Gamma }[T]{⊢}_{\mathrm{s}}{e}_1:\rho \to {\tau }^{\prime }$ and $\mathrm{\Gamma }[T]{⊢}_{\mathrm{s}}{e}_2:\rho$. The first induction hypothesis factors $T$ through $S_1$ as $S_1;R_1$ and gives ${\tau }_1[R_1]=\rho \to {\tau }^{\prime }$. Regard the second target premise as a derivation under $\mathrm{\Gamma }[S_1;R_1]$ and apply the second induction hypothesis, adding ${\mathrm{fv}}_{S_1}(P)\cup \mathrm{ftv}({\tau }_1)$ to the protected set. It factors $R_1$ through $S_2$ as $S_2;R_2$ on both $\mathrm{ftv}(\mathrm{\Gamma }[S_1])$ and ${\mathrm{fv}}_{S_1}(P)\cup \mathrm{ftv}({\tau }_1)$, and gives ${\tau }_2[R_2]=\rho$. Extend $R_2$ to send the fresh result variable $\beta$ to ${\tau }^{\prime }$. Freshness gives $\beta \notin \mathrm{ftv}({\tau }_1[S_2])\cup \mathrm{ftv}({\tau }_2)$ and keeps $\beta$ out of every inherited protected image, so this extension changes none of the equalities already obtained. Then $R_2$ solves $${\tau }_1[S_2]\doteq {\tau }_2\to \beta .$$ Indeed, protected agreement gives ${\tau }_1[S_2;R_2]={\tau }_1[R_1]=\rho \to {\tau }^{\prime }$, while ${\tau }_2[R_2]=\rho$ and $\beta [R_2]={\tau }^{\prime }$. Hence unification cannot fail by theorem 3.26; let its MGU be $U$. Its universal property factors $R_2=U;R_3$ on the variables of this equation, and lemma 4.45 extends $R_3$ on the inherited protected variables and on $\mathrm{ftv}(\mathrm{\Gamma }[S_1;S_2])\cup {\mathrm{fv}}_{S_1;S_2}(P)$ outside the equation. At each equality above, agreement on the displayed free-variable set extends from variables to the containing types by lemma 4.6. The two factorization stages and the MGU stage have the following proof state: Substituting each residual factor into the preceding row gives the chain Thus substitution composition gives $T=S_1;S_2;U;R_3$ on $\mathrm{ftv}(\mathrm{\Gamma })\cup P$ and ${\tau }^{\prime }=\beta [U;R_3]$, exactly the returned pair.

Let. The target premises have the form $$\mathrm{\Gamma }[T]{⊢}_{\mathrm{s}}{e}_1:{\rho }_1,\mathrm{\Gamma }[T],x:{\sigma }^{\prime }{⊢}_{\mathrm{s}}{e}_2:{\tau }^{\prime },{\sigma }^{\prime }={\mathrm{Gen}}_{\mathrm{\Gamma }[T]}({\rho }_1).$$ The first induction hypothesis gives $T=S_1;R_1$ on $\mathrm{ftv}(\mathrm{\Gamma })\cup P$ and ${\rho }_1={\tau }_1[R_1]$. Put $\sigma ={\mathrm{Gen}}_{\mathrm{\Gamma }[S_1]}({\tau }_1)$, as W does. Lemma 3.14 gives $$\sigma [R_1]⊒{\mathrm{Gen}}_{\mathrm{\Gamma }[S_1;R_1]}({\tau }_1[R_1])={\sigma }^{\prime }.$$ Thus lemma 3.33 turns the second target premise into one under $$(\mathrm{\Gamma }[S_1],x:\sigma )[R_1].$$ The transported derivation has the same height by lemma 3.33, hence still has height strictly below the target let derivation. The height induction therefore applies to it. Apply the second induction hypothesis with protected set ${\mathrm{fv}}_{S_1}(P)$. It factors $R_1$ through $S_2$ as $S_2;R_2$ on the body context and on ${\mathrm{fv}}_{S_1}(P)$; it also gives ${\tau }^{\prime }={\tau }_2[R_2]$. Thus $$T=S_1;S_2;R_2\text{on}\mathrm{ftv}(\mathrm{\Gamma })\cup P,$$ which is the required factorization of W’s let pair. ◻

Proof of Theorem 3.36 — Principal-pair theorem

Proof. Apply lemma 4.46 with $P=\varnothing$; fresh-choice irrelevance transports its convenient run back to the fixed supply. For the final consequence, use theorem 3.34 to obtain a syntax-directed monotype derivation from the declarative one, then apply the first assertion. ◻

Proof of Corollary 3.37 — Principal schemes in a closed signature

Proof. The context equality is immediate because $S$ has no free context variable to change. Soundness followed by repeated Gen types $e$ at the displayed scheme. Given any other scheme, choose a fresh monotype instance as follows: present it as $\mathrm{\forall }\overline{\beta }.\rho$ with $\overline{\beta }$ fresh for ${\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau )$, and regard its body $\rho$ as the generic instance obtained by replacing the prefix with those fresh variables. Rule Inst types that body; theorem 3.34 converts it to a syntax-directed monotype derivation, and the principal-pair theorem expresses $\rho$ as $\tau [R]$. Every variable of $\tau$ is generalized over the closed context. By lemma 3.9, the generic instance of the competing scheme factors through ${\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau )$, so the latter is at least as general as the competing scheme. ◻

Proof of Corollary 4.49 — Principal generalization after an open-context run

Proof. Soundness and repeated Gen give the displayed typing. Apply theorem 3.36 to the competing typing with $T=S$. It yields $$S{=}_{\mathrm{ftv}(\mathrm{\Gamma })}S;R,{\tau }^{\prime }=\tau [R].$$ The first equality says exactly that $\mathrm{\Gamma }[S]=\mathrm{\Gamma }[S;R]=\mathrm{\Gamma }[S][R]$. Thus $R$ fixes every free parameter of the resulting context, and the equations ${\tau }^{\prime }=\tau [R]$ and $R{|}_{\mathrm{ftv}(\mathrm{\Gamma }[S])}=\mathsf{id}$ satisfy the instance condition of lemma 3.9. Hence ${\tau }^{\prime }$ is an instance of ${\mathrm{Gen}}_{\mathrm{\Gamma }[S]}(\tau )$. For a competing scheme, instantiate its quantified prefix by fresh monotypes, apply this argument to the resulting monotype, and generalize the fresh variables again. ◻

For an open $\mathrm{\Gamma }$, the substitution returned by W may act on $\mathrm{ftv}(\mathrm{\Gamma })$, so the resulting context in this corollary cannot generally be replaced by the original one. The closedness hypothesis of corollary 3.37 gives $\mathrm{\Gamma }[S]=\mathrm{\Gamma }$.

A complete inference trace

The batch calculation of section 3.3 collects all equations and solves them once. Algorithm W instead solves and threads substitutions while traversing the program. On a bound definition used polymorphically, take $$P_{\mathsf{twice}}:=\mathsf{let}t=\mathsf{twice}\mathsf{in}tt.$$ The bound calculation shows exactly the substitution threading hidden by a batch solve. Give $f$ the fresh type $\alpha$ and $x$ the fresh type $\beta$. In the inner application $fx$, both variable calls return the identity. A fresh $\gamma$ stands for the result, so W calls $$\mathsf{unify}((\alpha \doteq \beta \to \gamma ))=U_1,U_1=[\beta \to \gamma /\alpha ].$$ The inner application therefore returns $(U_1,\gamma )$. For the outer application $f(fx)$, the first recursive call again gives provisional function type $\alpha$, while the second returns $(U_1,\gamma )$. The application clause must apply that second substitution to the provisional function type before unifying: $$\alpha [U_1]=\beta \to \gamma \doteq \gamma \to \delta ,$$ where $\delta$ is the fresh result variable. Left-to-right decomposition and elimination give $$U_2=[\delta /\beta ,\delta /\gamma ].$$ Thus the body returns $(U_1;U_2,\delta )$. The two lambda clauses reapply the same composite to their provisional domains, so This is the same principal monotype as the batch answer, up to the name of its surviving parameter. Unlike that answer, the calculation displays the two separate unification calls made by W and the nonidentity substitution $U_1$ threaded from the argument call back into the function type.

Because $S_0$ acts as the identity on ${\mathrm{\Gamma }}_0$, the let clause generalizes $\delta$ and extends the context by $$t:{\sigma }_t,{\sigma }_t:=\mathrm{\forall }\delta .(\delta \to \delta )\to \delta \to \delta .$$ Now infer the application $tt$. Its two variable calls both return the identity substitution, but they consume different fresh instance variables, $ϵ$ and $\zeta$: Thus $S_f=S_a=\mathrm{id}$ for these two inner calls. Introduce the fresh result variable $\eta$. The application clause asks unification to solve $$(ϵ\to ϵ)\to (ϵ\to ϵ)\doteq ((\zeta \to \zeta )\to (\zeta \to \zeta ))\to \eta .$$ Decomposition first equates the domains and then the codomains: $$ϵ\to ϵ\doteq (\zeta \to \zeta )\to (\zeta \to \zeta ),ϵ\to ϵ\doteq \eta .$$ The first equation decomposes once more. Both of its components say $ϵ\doteq \zeta \to \zeta$; after the first elimination, the second is deleted as reflexive. Substitution in the remaining equation then gives $$(\zeta \to \zeta )\to (\zeta \to \zeta )\doteq \eta .$$ Rule U-Orient first moves $\eta$ to the left; U-Eliminate then removes it. Thus the MGU is $$U_3=[(\zeta \to \zeta )/ϵ,((\zeta \to \zeta )\to (\zeta \to \zeta ))/\eta ],$$ and the body call returns $(U_3,\eta [U_3])$. The complete let clause therefore returns the pair $$\mathsf{W}({\mathrm{\Gamma }}_0,P_{\mathsf{twice}})=(S_0;U_3,(\zeta \to \zeta )\to \zeta \to \zeta ).$$ In the outer let clause of definition 3.28, its first result is the substitution called $S_0$ in this trace, and its second result is the substitution called $U_3$ here. W itself returns this monotype; it does not generalize the final answer. Since ${\mathrm{\Gamma }}_0$ is closed and $\zeta$ is absent from it, corollary 3.37 gives the principal scheme of the program: $$\mathrm{\forall }\zeta .(\zeta \to \zeta )\to \zeta \to \zeta .$$ There is no circular typing here. The two occurrences of $t$ were opened at different instances before equation (3.4) was solved. The unifier then discovered the particular relation between those instances required by the application.

The evidence reconstructed by inference

An implementation should be able to show what it inferred. The following small core records every instantiation and lambda domain without introducing first-class polymorphism.

Let $\mathrm{\Theta }$ be a finite scope of type variables. Write $\mathrm{\Theta }⊢\tau \mathsf{mono}$ when $\mathrm{ftv}(\tau )\subseteq \mathrm{\Theta }$, and call a context $\mathrm{\Gamma }$ well formed over $\mathrm{\Theta }$ when $\mathrm{ftv}(\mathrm{\Gamma })\subseteq \mathrm{\Theta }$.

Proof of Lemma 4.52 — Evidence substitution

Proof. Induct on the checking derivation. Rule Ev-Var uses the substitution commutation calculation (3.2). Rules Ev-Lam and Ev-App reapply to the induction hypotheses. In Ev-Let, first alpha-rename $\overline{\alpha }$ away from the domain and range of $S$. Substitution then fixes the prefix, acts on the free variables inherited from $\mathrm{\Gamma }$ in both premises, and preserves the displayed set difference. Reapply Ev-Let. Erasure equality follows from the four structural clauses of definition 4.50. ◻

Proof of Lemma 4.53 — Evidence over a prescribed scope

Proof. Induct on its height, generalized over $\mathrm{\Gamma },\tau ,\mathrm{\Theta }$. The variable case uses the instance witness from S-Var in Ev-Var; the lambda case copies the domain from S-Lam into Ev-Lam. At an application, write its premise types as $\rho \to \tau$ and $\rho$. The variables of $\rho$ need not occur in the conclusion. Let $G$ send every variable of $\mathrm{ftv}(\rho )\setminus \mathrm{\Theta }$ to $\mathsf{Nat}$ and fix all others. Since $G$ fixes $\mathrm{\Gamma }$ and $\tau$, the syntax-directed construction in lemma 3.32 preserves their heights and changes them to $$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_1:\rho [G]\to \tau ,\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_2:\rho [G],$$ and $\mathrm{ftv}(\rho [G])\subseteq \mathrm{\Theta }$. Apply the two induction hypotheses and then Ev-App.

At a let, put $\overline{\alpha }=\mathrm{ftv}({\tau }_1)\setminus \mathrm{ftv}(\mathrm{\Gamma })$ and alpha-rename this prefix away from $\mathrm{\Theta }$. Every free type variable of the definition premise lies in $\mathrm{\Theta }\cup \overline{\alpha }$, while the quantified prefix is absent from the free variables of the body context. Apply the induction hypothesis to the definition over $\mathrm{\Theta }\cup \overline{\alpha }$, apply it to the body over $\mathrm{\Theta }$, and finish with Ev-Let. Each constructor used here erases to the source constructor in the corresponding premise. ◻

Proof of Theorem 4.54 — Checked reconstruction from W

Proof. By theorem 3.35, W’s result has a declarative derivation $\mathrm{\Gamma }[S]⊢e:\tau$. The declarative-to-syntax-directed half of theorem 3.34 gives $\mathrm{\Gamma }[S]{⊢}_{\mathrm{s}}e:\tau$. The definition of $\mathrm{\Theta }$ covers exactly the free variables of this judgment, so lemma 4.53 supplies the required evidence. Its erasure equation is part of that lemma’s conclusion. ◻

For $P_{\mathsf{twice}}$, W reconstructs, up to renaming of type variables, The first occurrence has type $$((\zeta \to \zeta )\to (\zeta \to \zeta ))\to (\zeta \to \zeta )\to (\zeta \to \zeta ),$$ and the second has its domain type $(\zeta \to \zeta )\to (\zeta \to \zeta )$. Hence the core application checks without another guess. The angle-bracketed arguments are static records of independent HM instantiations; they are not run-time type applications.

Algebraic data and pattern branches

Polymorphism remains attached to definitions, not to values extracted from an unknown list.

For a constructor calculation, take $\mathrm{\Gamma }=x:\alpha$. The declarative rules give

$(x:\alpha )\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x:\alpha$

$\mathrm{\Gamma }⊢\mathsf{nil}:\mathsf{List}(\alpha )$

$\mathrm{\Gamma }⊢\mathsf{cons}x\mathsf{nil}:\mathsf{List}(\alpha )$

W returns $(\mathrm{id},\alpha )$ for the head and $(\mathrm{id},\mathsf{List}(\beta ))$ for the tail, with fresh $\beta$. The cons equation $\mathsf{List}(\beta )\doteq \mathsf{List}(\alpha )$ decomposes to $\beta \doteq \alpha$, whose MGU is $[\alpha /\beta ]$; the constructor clause therefore returns $([\alpha /\beta ],\mathsf{List}(\alpha ))$.

For example, under $\mathrm{\Gamma }=d:\alpha ,xs:\mathsf{List}(\alpha )$, the body of $\mathsf{headOr}$ has the complete declarative derivation

$\mathrm{\Gamma }⊢xs:\mathsf{List}(\alpha )$$\mathrm{\Gamma }⊢d:\alpha$$\mathrm{\Gamma },h:\alpha ,t:\mathsf{List}(\alpha )⊢h:\alpha$

$\mathrm{\Gamma }⊢\mathsf{case}xs\mathsf{of}\{\mathsf{nil}\mapsto d;\mathsf{cons}ht\mapsto h\}:\alpha$

Definition 4.56, Definition 4.57 give one W clause for each of $\mathsf{nil}$, $\mathsf{cons}$, and $\mathsf{case}$. Every recursive call receives the substitutions returned by all earlier calls in its clause; the final unification in the case clause makes both branches produce one result type.

Proof of Theorem 4.58 — Sound and principal list inference

Proof. There are three new term forms. For nil soundness, apply S-ListNil at the fresh element type. For cons soundness, the two recursive induction hypotheses, transported successively by $S_2$ and $U$, have types $$e_1:{\tau }_1[S_2;U],e_2:\mathsf{List}({\tau }_1[S_2;U]);$$ apply S-ListCons. In the protected induction, a target nil typing has type $\mathsf{List}(\xi )$. Send W’s fresh $\alpha$ to $\xi$ and leave the inherited protected variables as prescribed; this factors the identity answer. For a target cons typing, apply the first recursive induction hypothesis to its head, then the second while protecting the updated head type. The residual factor makes ${\tau }_2=\mathsf{List}({\tau }_1[S_2])$ true after substitution, so MGU factorization supplies $U$; associativity gives the returned three-stage factorization and its list result type.

For case soundness, the three recursive induction hypotheses type the scrutinee and both branches under the contexts shown in the W clause. Apply each later substitution to each earlier derivation. Because $U$ solves ${\tau }_0\doteq \mathsf{List}(\alpha )$, the updated scrutinee has type $\mathsf{List}(\alpha [U;S_1;S_2;V])$. The two pattern declarations have that element type. Because $V$ solves ${\rho }_0[S_2]\doteq {\rho }_1$, both branches have type ${\rho }_1[V]$. Rule S-ListCase gives exactly the returned context and type.

For the protected induction, invert a target case derivation under $\mathrm{\Gamma }[T]$. For some target types $\xi ,\chi$, its premises are $$\mathrm{\Gamma }[T]{⊢}_{\mathrm{s}}e:\mathsf{List}(\xi ),\mathrm{\Gamma }[T]{⊢}_{\mathrm{s}}{e}_0:\chi ,$$ $$\mathrm{\Gamma }[T],h:\xi ,t:\mathsf{List}(\xi ){⊢}_{\mathrm{s}}{e}_1:\chi .$$ Choose the W element variable $\alpha$ fresh for the target derivation and let $\hat{T}$ agree with $T$ everywhere except that $\alpha [\hat{T}]=\xi$. Freshness gives $\mathrm{\Gamma }[\hat{T}]=\mathrm{\Gamma }[T]$ and $\hat{T}{=}_{\mathrm{ftv}(\mathrm{\Gamma })\cup P}T$. Apply the first induction hypothesis to the scrutinee with protected set $P\cup \{\alpha \}$. It returns $S_0,{\tau }_0$ and a factor $R_0$ such that $$\hat{T}{=}_{\mathrm{ftv}(\mathrm{\Gamma })\cup P\cup \{\alpha \}}{S}_0;R_0,{\tau }_0[R_0]=\mathsf{List}(\xi ).$$ The scrutinee call receives the supply after $\alpha$ was consumed, so $S_0$ fixes $\alpha$. Agreement at the added protected variable therefore gives $\alpha [R_0]=\alpha [S_0;R_0]=\alpha [\hat{T}]=\xi$. Together with the last equality, this says that $R_0$ solves ${\tau }_0\doteq \mathsf{List}(\alpha )$. Let $U$ be its MGU. MGU factorization, extended on $\mathrm{ftv}(\mathrm{\Gamma }[S_0])\cup {\mathrm{fv}}_{S_0}(P)$, gives $R_0=U;R_U$ there. Therefore the nil target premise may be read under $\mathrm{\Gamma }[S_0;U;R_U]$. Its induction hypothesis returns $S_1,{\rho }_0$ and $R_1$ with $$R_U{=}_{\mathrm{ftv}(\mathrm{\Gamma }[S_0;U])\cup {\mathrm{fv}}_{S_0;U}(P)}{S}_1;R_1,{\rho }_0[R_1]=\chi .$$

Protect additionally the variables of $\alpha [U;S_1]$ and ${\rho }_0$. The preceding factorizations identify the target pattern context with the W pattern context after $R_1$: $$\alpha [U;S_1;R_1]=\xi ,\mathsf{List}(\alpha [U;S_1;R_1])=\mathsf{List}(\xi ).$$ The cons-branch induction hypothesis consequently returns $S_2,{\rho }_1$ and $R_2$ such that Protected agreement also gives ${\rho }_0[S_2;R_2]={\rho }_0[R_1]=\chi$; hence $R_2$ solves the final equation ${\rho }_0[S_2]\doteq {\rho }_1$. If $V$ is its MGU, extend its factorization to obtain $R_2=V;R_3$ on every inherited protected variable. Put These are the protected arguments supplied to the three recursive induction hypotheses. The proof state is Associativity now assembles the five stages: Finally ${\rho }_1[V;R_3]=\chi$, which is the protected conclusion for the returned list-case pair.

It remains to connect these syntax-directed calculations to declarative principal schemes. Extend the simultaneous induction of theorem 3.34. The nil rules translate one-for-one at the same chosen element monotype. In the cons and case directions, specialize the induction outputs to the monotypes displayed in definition 4.55 and reapply the corresponding rule; in the reverse direction, replace each syntax-directed premise by its declarative induction hypothesis. Outer Inst and Gen are handled by the unchanged scheme-strengthened cases of that induction. Thus declarative and syntax-directed monotype typing remain equivalent after all three list forms are added. Combining this bridge with the nil, cons, and case calculations above proves every cited conclusion. ◻

Type inference and exhaustiveness are different questions. In the core syntax above, a list case contains both branches by grammar. A surface language may permit a partial match, but then a separate coverage check must reject a missing constructor before translating the surface case into its internal core term. Typing alone cannot do that job: the partial phrase $$\mathsf{case}xs\mathsf{of}\mathsf{cons}ht\mapsto h$$ has perfectly consistent type equations and still has no result on $\mathsf{nil}$.

The nil contraction selects $e_0$; the cons contraction substitutes the stored head and tail into $e_1$. Together they select a branch for each closed list constructor, which is the coverage needed by safety.

References and polymorphic let

Extend the type-constructor signature by the unary constructor $\mathsf{Ref}$. Substitution and unification again use their generic constructor clauses.

Pure evaluation cannot make one use of a let-bound value alter what another use will see. A mutable cell can. Add the type constructor $\mathsf{Ref}$, the type $\mathsf{Unit}$, and term forms $$\mathsf{ref}e,!e,e_1:=e_2,\mathsf{unit},$$ with the expected monomorphic rules

$\mathrm{\Gamma }⊢\mathsf{unit}:\mathsf{Unit}$

$\mathrm{\Gamma }⊢e:\tau$

$\mathrm{\Gamma }⊢\mathsf{ref}e:\mathsf{Ref}(\tau )$

$\mathrm{\Gamma }⊢e:\mathsf{Ref}(\tau )$

$\mathrm{\Gamma }⊢!e:\tau$

$\mathrm{\Gamma }⊢e_1:\mathsf{Ref}(\tau )$$\mathrm{\Gamma }⊢e_2:\tau$

$\mathrm{\Gamma }⊢e_1:=e_2:\mathsf{Unit}$

Naively retaining unrestricted let-generalization makes the following closed program typable: The first definition is assigned a provisional type $\mathsf{Ref}(\alpha \to \alpha )$. Naive generalization gives $$r:\mathrm{\forall }\alpha .\mathsf{Ref}(\alpha \to \alpha ).$$ The assignment instantiates this scheme at $\mathsf{Nat}$, while the final dereferencing instantiates it at $\mathsf{Bool}$. Thus the program receives type $\mathsf{Bool}$.

At run time, however, $\mathsf{ref}(\lambda x.x)$ allocates one location $\ell$. The assignment overwrites that same location with $\lambda x.\mathsf{succ}x$. The final line therefore reduces to $\mathsf{succ}\mathsf{true}$, which is stuck. The false step was not unification; it was treating one allocated cell as though each use created a fresh instance. This diagnostic uses the conventional run-time clauses for $\mathsf{succ}$ and $\mathsf{true}$. It is not an instance of the constant-free pure safety theorem above; that theorem applies only after a chosen primitive signature supplies typing and dynamics for its constants.

Proof of Lemma 4.64 — Context generality for value-restricted typing

Proof. Extend the induction of lemma 3.33. Unit has no premises, and reference, dereference, and assignment reapply their rules to the induction hypotheses. In S-Let-Mono, the bound declaration is the same monotype in the two body contexts. In S-Let-Gen, more-general outer declarations have no additional free type variables, so $\mathrm{ftv}(\mathrm{\Gamma })\subseteq \mathrm{ftv}({\mathrm{\Gamma }}^{\prime })$. Therefore $${\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_1)⊒{\mathrm{Gen}}_{{\mathrm{\Gamma }}^{\prime }}({\tau }_1)$$ by lemma 3.13; use this relation for the bound declaration when applying the body induction hypothesis. For ${\mathcal{L}}_{\mathsf{list}\mathsf{+}\mathsf{ref}}$, nil has no premises, while cons and case reapply their rules to the induction hypotheses. These are all rules added to either syntax-directed judgment. ◻

Proof of Lemma 4.65 — Value-restricted syntax equivalence

Proof. For declarative-to-syntax-directed typing, induct on the declarative derivation with the same strengthened scheme conclusion as theorem 3.34. A Var leaf chooses a fresh monotype instance for S-Var; Inst composes the instance witness; Gen enlarges the generalized prefix; and Lam and App specialize the induction outputs to their displayed monotypes before reapplying S-Lam or S-App.

There are three declarative let cases after inspecting the right-hand side. A Let-Gen derivation specializes its two induction outputs to the displayed monotypes and rebuilds S-Let-Gen. A Let-Mono derivation whose right-hand side is nongeneralizable rebuilds S-Let-Mono. If the right-hand side of Let-Mono is instead a generalizable form, its body induction output initially has context $\mathrm{\Gamma },x:{\tau }_1$. Since $${\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_1)⊒{\tau }_1,$$ lemma 4.64 transports that body derivation to $\mathrm{\Gamma },x:{\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_1)$, and S-Let-Gen rebuilds the conclusion. Thus the deterministic syntax-directed choice represents both declarative rules even when Let-Mono was used at a generalizable right-hand side. Unit, reference, dereference, and assignment each have one term-forming rule, so their induction cases specialize the premise outputs to the monotypes displayed above and reapply that rule. Conversely, induct on the syntax-directed derivation: replace S-Var by Var followed by Inst, insert repeated Gen before Let-Gen, and reuse the declarative lambda, application, monomorphic-let, and four store-form rules. In ${\mathcal{L}}_{\mathsf{list}\mathsf{+}\mathsf{ref}}$, the nil, cons, and case rules translate one-for-one in both directions. These cases exhaust both extended systems. ◻

Proof of Lemma 4.66 — Protected induction for the value-restricted signature

Proof. Induct on the syntax-directed derivation, generalized over $\mathrm{\Gamma },T,P$. The pure cases are exactly lemma 4.46. For ${\mathcal{L}}_{\mathsf{list}\mathsf{+}\mathsf{ref}}$, the three list cases are the constructor and five-stage case calculations in theorem 4.58. It remains to calculate the new let and store forms.

S-Let-Mono. Inversion gives target premises $$\mathrm{\Gamma }[T]{⊢}_{\mathrm{s}}{e}_1:{\rho }_1,\mathrm{\Gamma }[T],x:{\rho }_1{⊢}_{\mathrm{s}}{e}_2:{\tau }^{\prime }.$$ The first induction hypothesis returns $(S_1,{\tau }_1)$ and $R_1$ with $$T{=}_{\mathrm{ftv}(\mathrm{\Gamma })\cup P}{S}_1;R_1,{\tau }_1[R_1]={\rho }_1.$$ Thus the body premise is a derivation under $(\mathrm{\Gamma }[S_1],x:{\tau }_1)[R_1]$. Apply the second induction hypothesis while protecting ${\mathrm{fv}}_{S_1}(P)\cup \mathrm{ftv}({\tau }_1)$. It returns $(S_2,{\tau }_2)$ and $R_2$ such that $$R_1{=}_{\mathrm{ftv}(\mathrm{\Gamma }[S_1])\cup {\mathrm{fv}}_{S_1}(P)\cup \mathrm{ftv}({\tau }_1)}{S}_2;R_2,{\tau }_2[R_2]={\tau }^{\prime }.$$ Extensionality and associativity now give $T{=}_{\mathrm{ftv}(\mathrm{\Gamma })\cup P}{S}_1;S_2;R_2$, which is the returned factorization. The S-Let-Gen case is the pure let case because W selects it exactly when the right-hand side belongs to the generalizable-form grammar.

S-Assign. Inversion supplies a target type $\rho$ with $$\mathrm{\Gamma }[T]{⊢}_{\mathrm{s}}{e}_1:\mathsf{Ref}(\rho ),\mathrm{\Gamma }[T]{⊢}_{\mathrm{s}}{e}_2:\rho .$$ The first induction hypothesis gives $$T{=}_{\mathrm{ftv}(\mathrm{\Gamma })\cup P}{S}_1;R_1,{\tau }_1[R_1]=\mathsf{Ref}(\rho ).$$ Read the second target premise under $\mathrm{\Gamma }[S_1][R_1]$, protect ${\mathrm{fv}}_{S_1}(P)\cup \mathrm{ftv}({\tau }_1)$, and apply the second induction hypothesis: $$R_1=S_2;R_2\text{on that protected set},{\tau }_2[R_2]=\rho .$$ Consequently $${\tau }_1[S_2;R_2]={\tau }_1[R_1]=\mathsf{Ref}(\rho )=\mathsf{Ref}({\tau }_2[R_2]),$$ so $R_2$ solves W’s equation ${\tau }_1[S_2]\doteq \mathsf{Ref}({\tau }_2)$. If $U$ is its MGU, factor $R_2=U;R_3$ on the equation variables and extend $R_3$ on the inherited protected set by lemma 4.45. Put $P_1={\mathrm{fv}}_{S_1}(P)\cup \mathrm{ftv}({\tau }_1)$. The proof state is Composing the three residual factors gives $$T{=}_{\mathrm{ftv}(\mathrm{\Gamma })\cup P}{S}_1;S_2;U;R_3,\mathsf{Unit}=\mathsf{Unit}[R_3].$$

S-Deref. Inversion gives $\mathrm{\Gamma }[T]{⊢}_{\mathrm{s}}{e}_0:\mathsf{Ref}(\rho )$. The one recursive induction hypothesis gives $T=S;R_0$ on the inherited protected set and $\tau [R_0]=\mathsf{Ref}(\rho )$. Send W’s fresh $\alpha$ to $\rho$; then $R_0$ solves $\tau \doteq \mathsf{Ref}(\alpha )$. MGU factorization gives $R_0=U;R$, extended on the inherited protected variables, and $\alpha [U;R]=\rho$. This is precisely the assignment calculation with its second recursive branch and the outer $\mathsf{Ref}$ on ${\tau }_2$ removed.

S-Unit and S-Ref. Unit returns $(\mathrm{id},\mathsf{Unit})$; take $R=T$ and preserve agreement on $P$. For reference construction, the recursive induction hypothesis gives $\tau [R]=\rho$, and structural substitution gives $\mathsf{Ref}(\tau )[R]=\mathsf{Ref}(\rho )$. These cases exhaust the added forms and establish the strengthened claim. ◻

Proof of Theorem 4.67 — Principality with the conservative value restriction

Proof. For soundness, extend the induction of theorem 3.35. Unit uses S-Unit; reference construction reapplies S-Ref to its recursive typing. In dereference, type substitution by $U$ changes the recursive result from $\tau$ to $\mathsf{Ref}(\alpha [U])$, so S-Deref returns $\alpha [U]$. For assignment, the two induction hypotheses, transported successively by $S_2$ and $U$, have types $$e_1:{\tau }_1[S_2;U]=\mathsf{Ref}({\tau }_2[U]),e_2:{\tau }_2[U];$$ S-Assign returns $\mathsf{Unit}$. The generalized and monomorphic let clauses rebuild S-Let-Gen and S-Let-Mono, respectively. For ${\mathcal{L}}_{\mathsf{list}\mathsf{+}\mathsf{ref}}$, the three list cases are theorem 4.58; they are absent from ${\mathcal{L}}_{\mathsf{ref}}$.

For completeness and principality, first use lemma 4.65 to obtain a syntax-directed target. That equivalence normalizes a declarative Let-Mono with a generalizable right-hand side to S-Let-Gen, so the target and W select the same branch. Apply lemma 4.66 with $P=\varnothing$, then use the same final context-generality argument as in theorem 3.36. The returned factorization is therefore principal among all value-restricted typings. ◻

This conservative restriction is smaller than the nonexpansive classes used by mature ML implementations. A nonexpansive expression is one whose evaluation is certified not to allocate fresh mutable state or perform another effect before returning; generalizable forms constitute a simple conservative subclass. The smaller rule exposes the proof idea without an effect analysis. The offending expression $\mathsf{ref}(\lambda x.x)$ is not a generalizable form, so $r$ receives the single monotype $\mathsf{Ref}(\alpha \to \alpha )$. The assignment forces $\alpha =\mathsf{Nat}$; the final use then asks for $\alpha =\mathsf{Bool}$. Declaratively there is no monotype satisfying both uses; algorithmically W exposes the clash $\mathsf{Nat}\doteq \mathsf{Bool}$ and rejects it by constructor disjointness.

Proof of Lemma 4.69 — Run-time context generality

Proof. Induct on the run-time declarative derivation. Variable and instantiation use transitivity of $⊒$; every nongeneralizing rule reapplies to its induction hypotheses. More-general declarations have no additional free type variables, so $\mathrm{ftv}(\mathrm{\Gamma })\subseteq \mathrm{ftv}({\mathrm{\Gamma }}^{\prime })$. Hence a Gen$\mathrm{\Sigma }$ side condition valid for ${\mathrm{\Gamma }}^{\prime }$ is valid for $\mathrm{\Gamma }$. At Let-Gen$\mathrm{\Sigma }$, lemma 3.13 gives $${\mathrm{Gen}}_{\mathrm{\Gamma },\mathrm{\Sigma }}({\tau }_1)⊒{\mathrm{Gen}}_{{\mathrm{\Gamma }}^{\prime },\mathrm{\Sigma }}({\tau }_1),$$ where the fixed store variables are included in both forbidden sets. Use this relation for the bound declaration in the body induction hypothesis. The monomorphic let and location cases add no side condition. ◻

Proof of Lemma 4.70 — Run-time syntax equivalence

Proof. Use the simultaneous induction of theorem 3.34, with $\mathrm{ftv}(\mathrm{\Gamma })$ replaced by $\mathrm{ftv}(\mathrm{\Gamma })\cup \mathrm{ftv}(\mathrm{\Sigma })$ in every generalization case. A declarative Inst composes its instance witness with the one returned by the induction hypothesis; Gen$\mathrm{\Sigma }$ enlarges only the outer prefix. Each nongeneralizing term form translates one-for-one. For Let-Gen$\mathrm{\Sigma }$, the strengthened scheme conclusion identifies the body declaration with ${\mathrm{Gen}}_{\mathrm{\Gamma },\mathrm{\Sigma }}({\tau }_1)$. A Let-Mono derivation with a nonvalue definition uses the unchanged monotype declaration. If its definition is a closed value, then ${\mathrm{Gen}}_{\mathrm{\Gamma },\mathrm{\Sigma }}({\tau }_1)⊒{\tau }_1$, so lemma 4.69 transports the body premise before S-Let-Gen$\mathrm{\Sigma }$ is rebuilt. The location rule translates to S-Loc, and the list and reference rules are the cases already established in lemma 4.65. Conversely, replace the syntax-directed variable rule by Var followed by Inst, translate S-Let-Gen$\mathrm{\Sigma }$ directly to Let-Gen$\mathrm{\Sigma }$, and reuse each displayed declarative term-forming rule. These cases exhaust both run-time judgments. ◻

Proof of Lemma 4.71 — Run-time canonical forms

Proof. Apply lemma 4.70. The resulting syntax-directed derivation for an arrow can end only in the abstraction rule, one for a reference only in the location rule, and one for a list only in $\mathsf{nil}$ or $\mathsf{cons}$; constructor disjointness excludes the remaining value forms. ◻

Proof of Lemma 4.72 — Weakening by fresh store entries

Proof. Induct on the run-time typing derivation. The location and nongeneralizing cases are immediate because every old location retains its monotype. Before a Gen$\mathrm{\Sigma }$ case, alpha-rename its quantified variable throughout the premise and conclusion away from $\mathrm{ftv}({\mathrm{\Sigma }}^{\prime })$; the renamed side condition then holds for ${\mathrm{\Sigma }}^{\prime }$. Before a Let-Gen$\mathrm{\Sigma }$ case, alpha-rename the whole prefix of ${\mathrm{Gen}}_{\mathrm{\Gamma },\mathrm{\Sigma }}({\tau }_1)$, together with the corresponding free variables in the value-typing premise, away from $\mathrm{ftv}({\mathrm{\Sigma }}^{\prime })$. Those variables were absent from $\mathrm{\Gamma }$ and $\mathrm{\Sigma }$, so type-variable renaming preserves both premises. With the fresh presentation, ${\mathrm{Gen}}_{\mathrm{\Gamma },{\mathrm{\Sigma }}^{\prime }}({\tau }_1)$ is alpha-identical to the old scheme, and the two induction hypotheses reconstruct the rule. These are the only cases in which enlarging the store typing changes a side condition. ◻

Proof of Lemma 4.73 — Store-indexed value substitution

Proof. Freshen every term binder away from $x$ and the free variables of $v$, then induct on the second derivation. A variable leaf for $x$ is the first premise; every other variable keeps its declaration. The location, unit, and nil rules contain no term premise. Lambda, application, reference, dereference, assignment, cons, and list case reapply their rule to the induction hypotheses; in the case rule, freshening the two pattern binders prevents capture.

Rules Inst and Gen$\mathrm{\Sigma }$ reapply directly. The latter’s side condition is unchanged because substitution changes terms but neither $\mathrm{\Gamma }$ nor $\mathrm{\Sigma }$. In Let-Mono, apply the induction hypothesis to the definition and body and rebuild the rule. In Let-Gen$\mathrm{\Sigma }$, its definition is a run-time value. Substitution of the run-time value $v$ for a variable in another run-time value again yields a run-time value: abstractions use capture avoidance, unit and nil are unchanged, cons recurses on its two value arguments, and a location remains a location. The last case is permitted by the explicit run-time clause above and is not classified as a source constant or data constructor.

It remains to transport the body declaration. Freshen the inner binder to $y$. The two induction hypotheses give $$\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}{v}_1[v/x]:{\tau }_1,\mathrm{\Gamma },y:{\mathrm{Gen}}_{\mathrm{\Gamma },x:\sigma ,\mathrm{\Sigma }}({\tau }_1){⊢}_{\mathrm{\Sigma }}{e}_2[v/x]:{\tau }_2.$$ Removing $x:\sigma$ can only enlarge the generalized prefix, so $${\mathrm{Gen}}_{\mathrm{\Gamma },\mathrm{\Sigma }}({\tau }_1)⊒{\mathrm{Gen}}_{\mathrm{\Gamma },x:\sigma ,\mathrm{\Sigma }}({\tau }_1).$$ Apply lemma 4.69 to the second displayed derivation and then rebuild Let-Gen$\mathrm{\Sigma }$ with the first. These cases cover the complete run-time judgment, including both let rules and every list/reference form. ◻

Proof of Theorem 3.40 — Safety with the value restriction

Proof. Progress. Apply lemma 4.70 to the closed monotype typing, then induct on the resulting syntax-directed derivation. Lambda is a value. Application first uses the induction hypothesis on its next call-by-value child; an arrow-typed value is an abstraction by lemma 4.71, so the remaining application is a beta redex. A let with a nonvalue definition steps that definition, and either let rule contracts once its definition is a value. List constructors and their case eliminator use the two constructor contractions of section 3.8; unit is a value. For the store forms, by lemma 4.71, a closed value of reference type has the form $\ell$. From $\mu :\mathrm{\Sigma }$ and $\mathrm{\Sigma }(\ell )=\tau$ we obtain $\cdot {⊢}_{\mathrm{\Sigma }}\mu (\ell ):\tau$, so dereference steps to a term of the required type. Assignment uses the same lookup and replaces the cell by a value already typed at $\tau$. Allocation extends both $\mu$ and $\mathrm{\Sigma }$ by one matching entry.

Preservation. Use lemma 4.70 to put the source monotype typing in syntax-directed form, then induct on the store-step derivation. This supplies the premises of the unique rule for each outer term form. At a root step, allocation uses lemma 4.72 for every old cell and extends $\mathrm{\Sigma }$ by the inferred monotype of the allocated value; the location rule types the fresh result. Dereferencing uses the defining clause of $\mu :\mathrm{\Sigma }$, and assignment preserves that clause because the new value has exactly $\mathrm{\Sigma }(\ell )$. At a monomorphic let redex, lemma 4.73 applies. At a generalized let redex, its premise gives $v:{\tau }_1$, and the rule side condition permits repeated Gen$\mathrm{\Sigma }$, now excluding $\mathrm{ftv}(\mathrm{\Gamma })\cup \mathrm{ftv}(\mathrm{\Sigma })$. Hence $$\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}v:{\mathrm{Gen}}_{\mathrm{\Gamma },\mathrm{\Sigma }}({\tau }_1),$$ so the same substitution lemma discharges the let binder. Equivalently, the type-substitution lemma may instantiate this scheme while fixing both the context and the store typing. No allocation or assignment occurs inside the value. Because the generalized variables exclude $\mathrm{ftv}(\mathrm{\Sigma })$, a location’s stored monotype cannot be duplicated at incompatible instances. At beta and either let contraction, lemma 4.73 applies to the displayed run-time premises; its induction never changes $\mathrm{\Sigma }$, so the fixed store-typing premise is preserved.

For the nil case contraction, inversion of S-ListCase gives the nil branch directly at the result type. For the cons contraction, inversion gives $$\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}v:\rho ,\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}w:\mathsf{List}(\rho ),\mathrm{\Gamma },h:\rho ,t:\mathsf{List}(\rho ){⊢}_{\mathrm{\Sigma }}{e}_1:\tau .$$ Freshen $h,t$, weaken the two value typings under the other pattern declaration, and apply lemma 4.73 first to $h$ and then to $t$. The result is $\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}{e}_1[v/h,w/t]:\tau$, exactly the contractum typing.

For a compatible step, induct on $\mathcal{E}$. The child induction hypothesis may enlarge $\mathrm{\Sigma }$ to ${\mathrm{\Sigma }}^{\prime }$. In a unary frame $\mathsf{ref}[]$ or $![]$, reapply its rule directly. In every frame with a fixed sibling, first transport that sibling from $\mathrm{\Sigma }$ to ${\mathrm{\Sigma }}^{\prime }$ by lemma 4.72. For example, in $[]:=e_2$, the child retains type $\mathsf{Ref}(\rho )$ under ${\mathrm{\Sigma }}^{\prime }$; weakening gives $\cdot {⊢}_{{\mathrm{\Sigma }}^{\prime }}{e}_2:\rho$, so S-Assign reconstructs $\mathsf{Unit}$. In $v_1:=[]$, weaken the fixed premise $v_1:\mathsf{Ref}(\rho )$ instead. Application and cons use the same two calculations for their left and right frames.

For $\mathsf{let}x=[]\mathsf{in}{e}_2$, first weaken the body premise under $x:{\tau }_1$. If the reduct in the hole is not a value, rebuild S-Let-Mono. If it is a value, use ${\mathrm{Gen}}_{\mathrm{\Gamma },{\mathrm{\Sigma }}^{\prime }}({\tau }_1)⊒{\tau }_1$ and lemma 4.69 to transport the weakened body premise before rebuilding S-Let-Gen${\mathrm{\Sigma }}^{\prime }$. For the case frame, weaken both fixed branch premises; the two pattern declarations retain their monotypes. Store weakening also transports the nonstepping argument in $\mathcal{E}e$, the already evaluated function in $v\mathcal{E}$, and the corresponding cons arguments. These frames exhaust the context grammar in definition 4.68, so allocation inside any frame preserves the whole expression typing under the enlarged store typing. ◻

Where rank-one inference stops

HM quantifiers occur only at the outer edge of a let-bound scheme. This restriction is visible in three increasingly strong examples.

First, a lambda parameter cannot be assumed polymorphic. The term $$\lambda f.\mathsf{let}n=f\mathsf{zero}\mathsf{in}f\mathsf{true}$$ would need two instances of $f$, one with domain $\mathsf{Nat}$ and one with domain $\mathsf{Bool}$. Rule Lam gives $f$ one monotype, and W therefore produces incompatible equations for that single arrow domain. If a language allowed the rank-two annotation $$f:\mathrm{\forall }\alpha .\alpha \to \alpha ,$$ the body would be typable; HM deliberately cannot express that parameter type. Here rank two means that a quantified type occurs to the left of one arrow: the universal in the displayed parameter type is nested one level inside the type of the enclosing function. HM schemes have universals only at the outside and are therefore rank one.

Second, polymorphic values are not first-class data. HM can bind the identity to a scheme and use it, but it cannot put the scheme itself to the left of an arrow. Thus a function of intended type $$(\mathrm{\forall }\alpha .\alpha \to \alpha )\to \mathsf{Nat}$$ is outside the grammar of definition 3.6, even when its body merely applies the argument at $\mathsf{Nat}$.

Third, HM instantiation is predicative: quantified variables are replaced by monotypes, and a monotype contains no $\mathrm{\forall }$. An explicitly typed calculus may instead instantiate the polymorphic identity at its own polymorphic type, $$(\mathrm{\Lambda }\alpha .\lambda (x:\alpha ).x)⟨\mathrm{\forall }\alpha .\alpha \to \alpha ⟩(\mathrm{\Lambda }\alpha .\lambda (x:\alpha ).x).$$ Read $\mathrm{\Lambda }\alpha .d$ here as a static type abstraction binding the type variable $\alpha$ in $d$, and $d⟨\tau ⟩$ as explicit type application, which substitutes $\tau$ for that bound variable and erases before ordinary evaluation. This $\mathrm{\Lambda }$ binds a type variable, not the individual-variable proof notation used in first-order logic. This is an impredicative use. It requires a calculus with explicit type abstractions and applications. Abstracting an operation whose inputs are themselves types additionally requires kinds, classifiers that separate well-formed type-level functions from term-level functions. Neither explicit impredicative instantiation nor type-level abstraction belongs to HM. The gain would be expressiveness. The cost is that the inference problem solved by W would no longer describe the whole language: annotations or a stronger, more limited inference discipline become necessary.

Principal inference and its boundary

For input $(\mathrm{\Gamma },e)$, Algorithm W traverses $e$, generates fresh type unknowns, solves the resulting equations by most-general unification, and generalizes exactly the variables outside $\mathrm{ftv}(\mathrm{\Gamma })$. Theorem 3.35 types the returned pair, while theorem 3.36, corollary 3.37 show that every other typing factors through its substitution, and the returned generalization is at least as general as every scheme assignable to $e$ under the resulting context. In the pure calculus, distinct uses of a let-bound variable instantiate its scheme independently. With references, allocation makes those uses share one cell, so theorem 4.67 generalizes only the stated generalizable forms, a strict conservative subclass of nonexpansive expressions. Rank-one schemes still exclude polymorphic arguments and impredicative instantiation.

Bibliographic notes.

The presentation and notation are adapted to the proofs above, but the principal result is the theorem of Damas and Milner: they write with the more general scheme on the left [DM82]. The relation $⊒$ keeps that orientation while reserving for arithmetic. Their algorithm is stated in Section 6, soundness is Proposition 4, and completeness is the theorem of Section 7 [DM82]. Damas gives the fuller proof as Theorems 2 and 3 of Chapter II, Sections 4–5, of his thesis [Dam85]. The imperative counterexample and conservative value restriction belong to the subsequent development of imperative polymorphism; Wright proves type soundness for the corresponding discipline [Wri95].