ch:hindley-milner: ch:hindley-milner

For (a), first alpha-rename the quantified variables so that all prefixes are disjoint. The substitution $$[\gamma /\alpha ,\gamma /\beta ]$$ sends the body $\alpha \to \beta$ to $\gamma \to \gamma$. By lemma 3.9, $$\mathrm{\forall }\alpha \mathrm{\forall }\beta .\alpha \to \beta ⊒\mathrm{\forall }\gamma .\gamma \to \gamma .$$

For (b), the relation fails. An instance of $\mathrm{\forall }\alpha \mathrm{\forall }\beta .\alpha \to \beta$ may have unequal domain and codomain, for example $\mathsf{Nat}\to \mathsf{Bool}$. Every instance of $\mathrm{\forall }\gamma .\gamma \to \gamma$ has identical domain and codomain, so no instantiation produces that arrow.

For (c), the free $\delta$ is fixed and $[\delta /\alpha ](\alpha \to \delta )=\delta \to \delta$. Hence $$\mathrm{\forall }\alpha .\alpha \to \delta ⊒\delta \to \delta .$$

For (d), alpha-rename the scheme on the right to $\mathrm{\forall }ϵ.ϵ\to ϵ$, with $ϵ$ fresh. If the generality relation held, the characterization lemma would give a monotype $\rho$ with $$\rho \to \delta =ϵ\to ϵ.$$ Constructor injectivity would force both $\rho =ϵ$ and $\delta =ϵ$. The latter is impossible: $\delta$ is free and fixed on the left, whereas $ϵ$ is the freshly bound variable on the right. Thus the relation in (d) fails.

The arithmetic context has no free type variables. Therefore In the second line, $\alpha$ and $\beta$ are free in the context and only $\gamma$ is generalized.

For (c), $$\mathrm{ftv}(\mathrm{\forall }\alpha .\alpha \to \beta )=\{\beta \},\mathrm{ftv}({\mathrm{\Gamma }}_0,f:\mathrm{\forall }\alpha .\alpha \to \beta )=\{\beta \}.$$ The $\alpha$ in the proposed result type is therefore not fixed by the context, and $${\mathrm{Gen}}_{{\mathrm{\Gamma }}_0,f:\mathrm{\forall }\alpha .\alpha \to \beta }(\alpha \to \beta )=\mathrm{\forall }\alpha .\alpha \to \beta .$$

For the requested instance of lemma 3.15, start from (b) and $S=[\mathsf{Nat}/\alpha ]$. Rename the generalized variable $\gamma$ to a fresh ${\gamma }^{\prime }$ before applying $S$: $$T=[{\gamma }^{\prime }/\gamma ];S.$$ Then $T$ agrees with $S$ on the free variables $\alpha ,\beta$ of the context, $$\mathrm{\Gamma }[T]=\mathrm{\Gamma }[S]={\mathrm{\Gamma }}_0,f:\mathsf{Nat}\to \beta ,$$ and $${\mathrm{Gen}}_{\mathrm{\Gamma }[S]}(\tau [T])=\mathrm{\forall }{\gamma }^{\prime }.\mathsf{Nat}\to (\beta \to {\gamma }^{\prime })\to {\gamma }^{\prime }.$$ On the other hand, $${\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau )[S]=\mathrm{\forall }\gamma .\mathsf{Nat}\to (\beta \to \gamma )\to \gamma .$$ The two schemes are alpha-equivalent, so the required generality relation holds, in fact in both directions.

For (a), use two monomorphic assumptions and then generalize. Written one rule application per line, the complete derivation is $$\begin{array}{c}{\mathrm{\Gamma }}_0,x:\alpha ,y:\beta ⊢x:\alpha (Var),\\ {\mathrm{\Gamma }}_0,x:\alpha ⊢\lambda y.x:\beta \to \alpha (Lam),\\ {\mathrm{\Gamma }}_0⊢\lambda x.\lambda y.x:\alpha \to \beta \to \alpha (Lam),\\ {\mathrm{\Gamma }}_0⊢\lambda x.\lambda y.x:\mathrm{\forall }\alpha \mathrm{\forall }\beta .\alpha \to \beta \to \alpha (Gen\alpha ,\beta ).\end{array}$$ Both side conditions hold because ${\mathrm{\Gamma }}_0$ has no free type variables.

For (b), let ${\sigma }_{\mathsf{id}}=\mathrm{\forall }\alpha .\alpha \to \alpha$. The bound expression has that scheme by Var, Lam, and Gen. In the body, two independent Inst steps give Rule App combines them: $${\mathrm{\Gamma }}_0,\mathsf{id}:{\sigma }_{\mathsf{id}}⊢\mathsf{id}\mathsf{id}:\beta \to \beta .$$ Together with the typing of the bound identity, Let yields $${\mathrm{\Gamma }}_0⊢\mathsf{let}\mathsf{id}=\lambda x.x\mathsf{in}\mathsf{id}\mathsf{id}:\beta \to \beta .$$ Finally $\beta \notin \mathrm{ftv}({\mathrm{\Gamma }}_0)$, so one Gen step proves part (c): $${\mathrm{\Gamma }}_0⊢\mathsf{let}\mathsf{id}=\lambda x.x\mathsf{in}\mathsf{id}\mathsf{id}:\mathrm{\forall }\beta .\beta \to \beta .$$

Give the lambda-bound variables types ${\alpha }_f,{\alpha }_g,{\alpha }_x$. Give $gx$ the fresh result type $\beta$ and $f(gx)$ the fresh result type $\gamma$. The two application nodes force exactly $${\alpha }_g\doteq {\alpha }_x\to \beta ,{\alpha }_f\doteq \beta \to \gamma .$$ Eliminating ${\alpha }_g$ and ${\alpha }_f$ gives the MGU $$U=[{\alpha }_x\to \beta /{\alpha }_g,\beta \to \gamma /{\alpha }_f].$$ The provisional type of the three lambdas is ${\alpha }_f\to {\alpha }_g\to {\alpha }_x\to \gamma$; applying $U$ gives $$(\beta \to \gamma )\to ({\alpha }_x\to \beta )\to {\alpha }_x\to \gamma .$$ All three remaining variables are absent from ${\mathrm{\Gamma }}_0$. Renaming ${\alpha }_x$ to $\alpha$ and generalizing gives $$\mathrm{\forall }\alpha \mathrm{\forall }\beta \mathrm{\forall }\gamma .(\beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma .$$

Let $E_0$ be the printed two-equation list. Decomposition and elimination produce the following complete sequence: The algorithm returns, in diagrammatic order, $$R_1;R_2;R_3;R_4.$$ It sends $\alpha ,\gamma ,\delta$ to $\mathsf{Nat}$ and $\beta$ to $\mathsf{Bool}$. If the last initial equation is $\delta \doteq \delta \to \mathsf{Nat}$, the same two decompositions apply. The factors $R_1$ and $R_2$ do not mention $\delta$, and $R_3$ changes only $\gamma$, so that last equation remains $\delta \doteq \delta \to \mathsf{Nat}$. Since $\delta$ occurs properly on its right, U-Eliminate is forbidden and the occurs-check failure clause applies.

Give $f$ the fresh type $\alpha$ and $x$ the fresh type $\beta$. The innermost application introduces fresh $\gamma$ and solves $$\alpha \doteq \beta \to \gamma ,S_1=[\beta \to \gamma /\alpha ].$$ For the middle application, fresh $\delta$ stands for the result. After applying $S_1$, its ordered equation is $$\beta \to \gamma \doteq \gamma \to \delta .$$ Left-to-right decomposition produces $(\beta \doteq \gamma ,\gamma \doteq \delta )$. The first elimination is $[\gamma /\beta ]$; it leaves $\gamma \doteq \delta$, whose elimination is $[\delta /\gamma ]$. Thus the deterministic composite is $$S_2=[\gamma /\beta ];[\delta /\gamma ]=[\delta /\beta ,\delta /\gamma ].$$ Applying $S_1;S_2$ to the provisional lambda type $\alpha \to \beta \to \delta$ already yields the twice-shaped type. The third, outermost application introduces fresh $ϵ$ and solves $$\alpha [S_1;S_2]\doteq \delta \to ϵ,\delta \to \delta \doteq \delta \to ϵ.$$ Decomposition deletes the reflexive domain equation and returns $S_3=[ϵ/\delta ]$. Applying the full composite to the provisional lambda type $\alpha \to \beta \to ϵ$ yields $$(ϵ\to ϵ)\to ϵ\to ϵ.$$ Since $ϵ$ is absent from ${\mathrm{\Gamma }}_0$, generalization returns $\mathrm{\forall }ϵ.(ϵ\to ϵ)\to ϵ\to ϵ$. The third use of $f$ forces only the already-known equality of its input and output type, so the principal scheme is the same as for twice.

Write the scheme inferred for $\mathsf{compose}$ as $$C=\mathrm{\forall }\alpha \mathrm{\forall }\beta \mathrm{\forall }\gamma .(\beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma .$$ The let-bound definition is generalized to $C$. In the body $cc$, take two disjoint fresh instances: If $\rho$ is the fresh result type of the application, W solves $C_1\doteq C_2\to \rho$. Arrow decomposition first gives $${\beta }_1\to {\gamma }_1\doteq C_2,\rho \doteq ({\alpha }_1\to {\beta }_1)\to {\alpha }_1\to {\gamma }_1.$$ Decomposing the first equation gives the MGU components $${\beta }_1\mapsto {\beta }_2\to {\gamma }_2,{\gamma }_1\mapsto ({\alpha }_2\to {\beta }_2)\to {\alpha }_2\to {\gamma }_2.$$ Thus the body has monotype $$({\alpha }_1\to {\beta }_2\to {\gamma }_2)\to {\alpha }_1\to ({\alpha }_2\to {\beta }_2)\to {\alpha }_2\to {\gamma }_2.$$ The four displayed variables are generalized over ${\mathrm{\Gamma }}_0$.

The corresponding explicitly instantiated core term is The first static instance is precisely the function type required to accept the second instance as its first argument. Erasing annotations and type arguments returns the source term.

Work under $d:\alpha ,xs:\beta$. The list clause chooses fresh $\gamma$. The scrutinee call returns $(\mathrm{id},\beta )$, and the first equation is $$\beta \doteq \mathsf{List}(\gamma ).$$ Its MGU is $U=[\mathsf{List}(\gamma )/\beta ]$. The nil branch is the variable $d$, so it returns $(\mathrm{id},\alpha )$. The cons branch is checked under $$d:\alpha ,xs:\mathsf{List}(\gamma ),h:\gamma ,t:\mathsf{List}(\gamma ).$$ Its body is $h$, so it returns $(\mathrm{id},\gamma )$. The final branch equation is $\alpha \doteq \gamma$, with $V=[\gamma /\alpha ]$. Hence the list clause returns $$(U;V,\gamma ),\beta [U;V]=\mathsf{List}(\gamma ),\alpha [U;V]=\gamma .$$ The two enclosing lambda clauses therefore return $$\gamma \to \mathsf{List}(\gamma )\to \gamma .$$ Over the empty context, generalization gives $$\mathrm{\forall }\gamma .\gamma \to \mathsf{List}(\gamma )\to \gamma ,$$ which is the scheme in example 3.38, up to renaming.

The allocation expression receives $\mathsf{Ref}(\alpha \to \alpha )$. Since it is not a generalizable form, Let-Mono binds $r:\mathsf{Ref}(\alpha \to \alpha )$ with the same free $\alpha$. Typing $r:=(\lambda x.\mathsf{succ}x)$ produces $$\mathsf{Ref}(\alpha \to \alpha )\doteq \mathsf{Ref}(\mathsf{Nat}\to \mathsf{Nat}),$$ so unification fixes $\alpha =\mathsf{Nat}$. Dereferencing $r$ therefore returns a function of type $\mathsf{Nat}\to \mathsf{Nat}$, while the final application to $\mathsf{true}$ demands the equation $\mathsf{Nat}\doteq \mathsf{Bool}$. Its distinct nullary constructors trigger the clash rule. By contrast, $\lambda x.x$ is a generalizable form, so Let-Gen still assigns it $\mathrm{\forall }\alpha .\alpha \to \alpha$.

In the first example, $$\lambda f.\mathsf{let}n=f\mathsf{zero}\mathsf{in}f\mathsf{true},$$ rule Lam puts one monotype for $f$ in the context. The first application requires its domain to be $\mathsf{Nat}$, while the second requires the same domain to be $\mathsf{Bool}$. The rigid mismatch prevents a derivation. In an explicitly typed extension, the binder would be $f:\mathrm{\forall }\alpha .\alpha \to \alpha$, and the two occurrences would be written $f⟨\mathsf{Nat}⟩\mathsf{zero}$ and $f⟨\mathsf{Bool}⟩\mathsf{true}$. A value supplied for $f$ could be the explicit abstraction $\mathrm{\Lambda }\alpha .\lambda (x:\alpha ).x$.

The second example asks for an arrow whose domain is itself $\mathrm{\forall }\alpha .\alpha \to \alpha$. The monotype grammar of definition 3.6 has no $\mathrm{\forall }$ constructor, so such an arrow is not an HM monotype and cannot annotate a lambda-bound variable. In an extended syntax the binder carries that polymorphic annotation, and each use again contains an explicit type application such as $f⟨\mathsf{Nat}⟩\mathsf{zero}$.

The third example fails at instantiation. HM’s Inst substitutes monotypes for quantified variables, but $\mathrm{\forall }\alpha .\alpha \to \alpha$ is a scheme rather than a monotype. Hence the identity cannot be instantiated at its own polymorphic type. The displayed extended term places that scheme in an explicit type-application bracket and uses $\mathrm{\Lambda }$ at the two polymorphic values. In all three cases those annotations and applications are part of the extended source program; Algorithm W does not infer them.

The variable $\phi$ is inherited from the declaration of $f$ and is free in the input context. To infer the definition of $k$, W gives $x$ a fresh type $\alpha$. The body $f$ has type $\phi$, so $$\lambda x.f:\alpha \to \phi .$$ Generalization is relative to ${\mathrm{\Gamma }}_0,f:\phi$: $$\mathrm{ftv}(\alpha \to \phi )\setminus \mathrm{ftv}({\mathrm{\Gamma }}_0,f:\phi )=\{\alpha ,\phi \}\setminus \{\phi \}=\{\alpha \}.$$ Thus the let-bound declaration is $$k:\mathrm{\forall }\alpha .\alpha \to \phi .$$

At the occurrence $k\mathsf{zero}$, instantiate the prefix by a fresh $\beta$, obtaining $k:\beta \to \phi$. If $\gamma$ is the fresh application-result variable, unification solves $$\beta \to \phi \doteq \mathsf{Nat}\to \gamma$$ with the deterministic eliminations $[\mathsf{Nat}/\beta ]$ and $[\gamma /\phi ]$. The complete term therefore has result type $\gamma$. Up to identity action on the other fresh variables, W’s principal pair is $$([\mathsf{Nat}/\beta ,\gamma /\phi ],\gamma ).$$ Thus the returned substitution renames the inherited context parameter $\phi$ to the fresh result parameter $\gamma$. This is still principal: the factor $[\phi /\gamma ]$ recovers every typing over the original context, exactly as theorem 3.36, corollary 4.49 state. The fresh variables are $\alpha$ for the definition, $\beta$ for the independent use of its scheme, and $\gamma$ for the application result.

Process the equations first in their printed order. Eliminating $\alpha$, then $\beta$, then $\gamma$ produces the factors $$R_1=[\beta \to \gamma /\alpha ],R_2=[\mathsf{Nat}/\beta ],R_3=[\delta /\gamma ].$$ The returned composite $U_1=R_1;R_2;R_3$ acts on the problem variables by $$\alpha [U_1]=\mathsf{Nat}\to \delta ,\beta [U_1]=\mathsf{Nat},\gamma [U_1]=\delta ,\delta [U_1]=\delta .$$

Now process $$(\gamma \doteq \delta ,\beta \doteq \mathsf{Nat},\alpha \doteq \beta \to \gamma ).$$ The factors occur in the different order $$R_1^{\prime }=[\delta /\gamma ],R_2^{\prime }=[\mathsf{Nat}/\beta ],R_3^{\prime }=[\mathsf{Nat}\to \delta /\alpha ],$$ and $U_2=R_1^{\prime };R_2^{\prime };R_3^{\prime }$. Direct calculation gives the same four images as for $U_1$. Thus $$U_1{=}_{\{\alpha ,\beta ,\gamma ,\delta \}}{U}_2;\mathrm{id},U_2{=}_{\{\alpha ,\beta ,\gamma ,\delta \}}{U}_1;\mathrm{id}.$$ Although the lists of elimination factors differ, the two returned substitutions mutually factor on every problem variable. More generally, the MGU theorem gives such factors even when different legal traversals choose different variable representatives, so the solution family does not depend on the work-list order.

Give the identity value the monotype $\alpha \to \alpha$. Allocation then has type $$\mathsf{ref}(\lambda x.x):\mathsf{Ref}(\alpha \to \alpha ).$$ The allocation is expansive, so the first binding must use Let-Mono; it introduces $$r:\mathsf{Ref}(\alpha \to \alpha )$$ with no generalized variable.

The expression bound to $s$ is the variable $r$, hence it is nonexpansive and the generalized let rule is syntactically available. Nevertheless $\alpha$ occurs free in the surrounding declaration of $r$, so $${\mathrm{Gen}}_{{\mathrm{\Gamma }}_0,r:\mathsf{Ref}(\alpha \to \alpha )}(\mathsf{Ref}(\alpha \to \alpha ))=\mathsf{Ref}(\alpha \to \alpha ).$$ The prefix is empty. Thus the whole term has the same monomorphic reference type.

Operationally the first binding allocates one location $\ell$ containing the identity. The second let reduces by substituting that existing location: No second cell is allocated. Hence $r$ and $s$ are aliases and must share the one monomorphic store type assigned to $\ell$.

The only monotype instance of $\mathsf{Nat}$ is $\mathsf{Nat}$ itself. Instantiating the vacuous prefix in $\mathrm{\forall }\alpha .\mathsf{Nat}$ also always returns $\mathsf{Nat}$, because $\alpha$ does not occur in the body. Therefore each scheme is at least as general as the other, although they are not alpha-equivalent: alpha-renaming may change a bound name but cannot add or remove a quantifier.

Consequently principality is uniqueness in the preorder of generality, or uniqueness after quotienting by equality of instance sets, not uniqueness of literal printed syntax. A canonical printing convention removes this example by deleting every vacuous quantifier, equivalently by permitting in a prefix only variables that occur free in the scheme body. The definition of $\mathrm{Gen}$ already follows that convention.

The bound application is pure and reduces to the identity, but it is not a generalizable form. Under the conservative restriction it is therefore checked by Let-Mono. Give the resulting identity the single monotype $\alpha \to \alpha$ and introduce $i$ at that monotype.

The first use, $i\mathsf{zero}$, generates $$\alpha \to \alpha \doteq \mathsf{Nat}\to \beta ,$$ so unification sets $\alpha =\mathsf{Nat}$ and $\beta =\mathsf{Nat}$. The inner binding of $n$ does not change the type of $i$. The final use $i\mathsf{true}$ then requires $$\mathsf{Nat}\to \mathsf{Nat}\doteq \mathsf{Bool}\to \gamma ,$$ whose domain equation $\mathsf{Nat}\doteq \mathsf{Bool}$ is a rigid mismatch. That is the exact rejection.

A sound effect analysis could certify that evaluation of $(\lambda f.f)(\lambda x.x)$ neither allocates a reference nor reads, writes, or otherwise mutates shared state. It could then generalize its result to $\mathrm{\forall }\alpha .\alpha \to \alpha$, allowing the two uses to receive independent $\mathsf{Nat}$ and $\mathsf{Bool}$ instances. The same analysis must refuse that certificate for $P_{\mathsf{ref}}$: its bound expression performs allocation, and the later assignment mutates the allocated cell. Thus the effect-based relaxation accepts the pure application without reintroducing polymorphic references.