Hindley–Milner polymorphism and the value restriction

HM monotypes are finite constructor trees whose leaves may be type variables. Schemes have only an outer quantifier prefix, $\sigma ::=\tau \mid \mathrm{\forall }\alpha .\sigma$, and contexts assign schemes to distinct term variables. Write $\sigma ⊒{\sigma }^{\prime }$ when every monotype instance of ${\sigma }^{\prime }$ is an instance of $\sigma$. The complete declarative core is

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

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

$\mathrm{\Gamma }⊢e:\sigma$$\sigma ⊒{\sigma }^{\prime }$

$\mathrm{\Gamma }⊢e:{\sigma }^{\prime }$

$\mathrm{\Gamma }⊢e:\sigma$$\alpha \notin \mathrm{ftv}(\mathrm{\Gamma })$

$\mathrm{\Gamma }⊢e:\mathrm{\forall }\alpha .\sigma$

$\mathrm{\Gamma },x:{\tau }_1⊢e:{\tau }_2$

$\mathrm{\Gamma }⊢\lambda x.e:{\tau }_1\to {\tau }_2$

$\mathrm{\Gamma }⊢e_1:{\tau }_2\to \tau$$\mathrm{\Gamma }⊢e_2:{\tau }_2$

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

$\mathrm{\Gamma }⊢e_1:\sigma$$\mathrm{\Gamma },x:\sigma ⊢e_2:\tau$

$\mathrm{\Gamma }⊢\mathsf{let}x=e_1\mathsf{in}{e}_2:\tau$

Here the types displayed in Lam and App are monotypes; only a let-bound variable may receive a scheme.

For the closed primitive diagnostic, numerals are generated by

$\mathsf{zero}\mathsf{num}$

$n\mathsf{num}$

$\mathsf{succ}n\mathsf{num}$

Constraint generation, unification, and Algorithm W

For the let-free teaching calculation, the ordered constraint judgment is $\mathrm{\Gamma }{⊢}_{\mathrm{c}}e:\tau \mid E$, where $E\cdot E^{\prime }$ is list concatenation:

$\mathrm{\Gamma }(x)=\tau$

$\mathrm{\Gamma }{⊢}_{\mathrm{c}}x:\tau \mid ()$

$\mathrm{\Gamma },x:\alpha {⊢}_{\mathrm{c}}e:\tau \mid E$$\alpha \text{fresh}$

$\mathrm{\Gamma }{⊢}_{\mathrm{c}}\lambda x.e:\alpha \to \tau \mid E$

$\mathrm{\Gamma }{⊢}_{\mathrm{c}}{e}_1:{\tau }_1\mid E_1$$\mathrm{\Gamma }{⊢}_{\mathrm{c}}{e}_2:{\tau }_2\mid E_2$$\beta \text{fresh}$

$\mathrm{\Gamma }{⊢}_{\mathrm{c}}{e}_1{e}_2:\beta \mid E_1\cdot E_2\cdot ({\tau }_1\doteq {\tau }_2\to \beta )$

This judgment collects once; it is not Algorithm W.

The deterministic unifier consumes a finite equation list from the left. Substitutions act postfix, and $\tau [S;T]=(\tau [S])[T]$. Its complete clauses are Orientation is a nonrecursive preprocessing rewrite. The elimination clause requires $\alpha \ne \tau$ and $\alpha \notin \mathrm{ftv}(\tau )$. It fails when the occurs check fails. Unequal rigid constructors or unequal arities fail. Decomposition prepends component equations in the displayed order.

Syntax-directed typing is

$\mathrm{\Gamma }(x)=\sigma$$\sigma \succcurlyeq \tau$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}x:\tau$

$\mathrm{\Gamma },x:{\tau }_1{⊢}_{\mathrm{s}}e:{\tau }_2$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}\lambda x.e:{\tau }_1\to {\tau }_2$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_1:{\tau }_1\to {\tau }_2$$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_2:{\tau }_1$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_1{e}_2:{\tau }_2$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_1:{\tau }_1$$\mathrm{\Gamma },x:{\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_1){⊢}_{\mathrm{s}}{e}_2:{\tau }_2$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}\mathsf{let}x=e_1\mathsf{in}{e}_2:{\tau }_2$

Algorithm W carries one monotonically consumed fresh-variable supply. With every fresh variable new for the entire run, its complete pure clauses are

The evidence checker records variable instantiation, lambda domains, application, and let generalization by the four rules Ev-Var, Ev-Lam, Ev-App, and Ev-Let of definition 4.51; its judgment is $\mathrm{\Theta };\mathrm{\Gamma }{⊢}_{\mathsf{ev}}d:\tau$, and erasure is defined in definition 4.50.

For lists add $\mathsf{List}$, nil, cons, and the rules

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

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

$\mathrm{\Gamma }⊢\mathsf{cons}{e}_1{e}_2:\mathsf{List}(\tau )$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}\mathsf{nil}:\mathsf{List}(\tau )$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_1:\tau$$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_2:\mathsf{List}(\tau )$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}\mathsf{cons}{e}_1{e}_2:\mathsf{List}(\tau )$

$\mathrm{\Gamma }⊢e:\mathsf{List}(\tau )$$\mathrm{\Gamma }⊢e_0:\rho$$\mathrm{\Gamma },h:\tau ,t:\mathsf{List}(\tau )⊢e_1:\rho$

$\mathrm{\Gamma }⊢\mathsf{case}e\mathsf{of}\{\mathsf{nil}\mapsto e_0;\mathsf{cons}ht\mapsto e_1\}:\rho$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}e:\mathsf{List}(\tau )$$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_0:\rho$$\mathrm{\Gamma },h:\tau ,t:\mathsf{List}(\tau ){⊢}_{\mathrm{s}}{e}_1:\rho$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}\mathsf{case}e\mathsf{of}\{\mathsf{nil}\mapsto e_0;\mathsf{cons}ht\mapsto e_1\}:\rho$

W returns $(\mathrm{id},\mathsf{List}(\alpha ))$ for nil with fresh $\alpha$. For cons it computes and returns $(S_1;S_2;U,\mathsf{List}({\tau }_1[S_2;U]))$. The case clause computes, in order, and returns $(S_0;U;S_1;S_2;V,{\rho }_1[V])$.

For references, add $\mathsf{Unit}$, $\mathsf{Ref}(\tau )$, locations, and the standard 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}$

The conservative value restriction replaces unrestricted generalization at let by

$\mathrm{\Gamma }⊢v:{\tau }_1$$\mathrm{\Gamma },x:{\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_1)⊢e_2:{\tau }_2$

$\mathrm{\Gamma }⊢\mathsf{let}x=v\mathsf{in}{e}_2:{\tau }_2$

$\mathrm{\Gamma }⊢e_1:{\tau }_1$$\mathrm{\Gamma },x:{\tau }_1⊢e_2:{\tau }_2$

$\mathrm{\Gamma }⊢\mathsf{let}x=e_1\mathsf{in}{e}_2:{\tau }_2$

where $v$ ranges over the generalizable forms (variables, constants, abstractions, and fully applied data constructors whose arguments are generalizable forms) and ${\mathrm{Gen}}_{\mathrm{\Gamma }}(\tau )=\mathrm{\forall }(\mathrm{ftv}(\tau )\setminus \mathrm{ftv}(\mathrm{\Gamma })).\tau$, with the finite prefix listed in the fixed global type-variable order.

The syntax-directed value-restricted rules are

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}v:{\tau }_1$$\mathrm{\Gamma },x:{\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_1){⊢}_{\mathrm{s}}{e}_2:{\tau }_2$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}\mathsf{let}x=v\mathsf{in}{e}_2:{\tau }_2$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_1:{\tau }_1$$\mathrm{\Gamma },x:{\tau }_1{⊢}_{\mathrm{s}}{e}_2:{\tau }_2$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}\mathsf{let}x=e_1\mathsf{in}{e}_2:{\tau }_2$

The first rule requires a generalizable form and the second a nongeneralizable expression. The store forms are

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

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

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

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

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

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_1:\mathsf{Ref}(\tau )$$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_2:\tau$

$\mathrm{\Gamma }{⊢}_{\mathrm{s}}{e}_1:=e_2:\mathsf{Unit}$

At run time a store typing $\mathrm{\Sigma }$ maps locations to monotypes, and

$\ell \in \mathrm{dom}(\mathrm{\Sigma })$

$\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}\ell :\mathsf{Ref}(\mathrm{\Sigma }(\ell ))$

$\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}e:\sigma$$\alpha \notin \mathrm{ftv}(\mathrm{\Gamma })\cup \mathrm{ftv}(\mathrm{\Sigma })$

$\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}e:\mathrm{\forall }\alpha .\sigma$

$\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}v:{\tau }_1$$\mathrm{\Gamma },x:{\mathrm{Gen}}_{\mathrm{\Gamma },\mathrm{\Sigma }}({\tau }_1){⊢}_{\mathrm{\Sigma }}{e}_2:{\tau }_2$

$\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}\mathsf{let}x=v\mathsf{in}{e}_2:{\tau }_2$

where $${\mathrm{Gen}}_{\mathrm{\Gamma },\mathrm{\Sigma }}(\tau )=\mathrm{\forall }(\mathrm{ftv}(\tau )\setminus (\mathrm{ftv}(\mathrm{\Gamma })\cup \mathrm{ftv}(\mathrm{\Sigma }))).\tau .$$ All nongeneralizing rules lift by adding the same $\mathrm{\Sigma }$ subscript. For a store $\mu$, the three value-restricted roots are