Hindley–Milner type system

Definition

Fix a set of type variables $\alpha, \beta, \dots$ and a set of type constructors containing the arrow $\to$. The monotypes are $\tau ::= \alpha \mid C\, \tau_1 \cdots \tau_n$, where $C$ is a type constructor of arity $n$; in particular $\tau_1 \to \tau_2$ is a monotype. The type schemes are $\sigma ::= \tau \mid \forall \alpha.\, \sigma$. The terms are $e ::= x \mid e\, e \mid \lambda x.\, e \mid \mathsf{let}\ x = e\ \mathsf{in}\ e$. A context $\Gamma$ assigns type schemes to finitely many variables. A monotype $\tau$ is an instance of $\forall \alpha_1 \dots \alpha_n.\, \tau_0$ if $\tau = \tau_0[\tau_1/\alpha_1, \dots, \tau_n/\alpha_n]$ for some monotypes $\tau_i$. The typing relation $\Gamma \vdash e : \tau$ of the Hindley–Milner type system is the least relation closed under these rules.

1. Variable: if $x : \sigma$ is in $\Gamma$ and $\tau$ is an instance of $\sigma$, then $\Gamma \vdash x : \tau$.
2. Application: if $\Gamma \vdash e_1 : \tau_1 \to \tau_2$ and $\Gamma \vdash e_2 : \tau_1$, then $\Gamma \vdash e_1\, e_2 : \tau_2$.
3. Abstraction: if $\Gamma, x : \tau_1 \vdash e : \tau_2$ with $\tau_1$ a monotype, then $\Gamma \vdash \lambda x.\, e : \tau_1 \to \tau_2$.
4. Let: if $\Gamma \vdash e_1 : \tau_1$ and $\Gamma, x : \mathrm{gen}_\Gamma(\tau_1) \vdash e_2 : \tau_2$, then $\Gamma \vdash \mathsf{let}\ x = e_1\ \mathsf{in}\ e_2 : \tau_2$.

Here $\mathrm{gen}_\Gamma(\tau_1) = \forall \alpha_1 \dots \alpha_n.\, \tau_1$, where $\alpha_1, \dots, \alpha_n$ are the type variables free in $\tau_1$ but not free in $\Gamma$.