Typed lambda calculi — λ-calculus

In the λ-calculus paradigm, types are a guarantee that a program finishes in finite time. The price is the loss of Turing completeness; the payoff is predictability, documentation and, as we have already seen, an entire logic.

The simplest such system is the simply typed λ-calculus ( $\lambda^{\to}$ ). Every term in it is assigned a type, and the types themselves are built from atomic $\alpha$ by a single construction — the arrow:

\displaystyle \tau \;\mathrel{\text{::=}}\; \alpha \;\mid\; \tau

\displaystyle \to \tau

(1.37)

Three inference rules — one per term construct:

\frac{x{:}\tau \in \Gamma}{\Gamma \vdash x : \tau} \qquad \frac{\Gamma,\; x{:}\sigma \vdash M : \tau}{\Gamma \vdash \lambda x.\,M : \sigma \to \tau} \qquad \frac{\Gamma \vdash M : \sigma \to \tau \quad \Gamma \vdash N : \sigma}{\Gamma \vdash M\,N : \tau}

(1.38)

Left to right: a variable takes its type from the context $\Gamma$ ; abstraction — if under the assumption $x{:}\sigma$ the body $M$ has type $\tau$ , then $\lambda x.\,M$ is a function of type $\sigma$ $\to\tau$ ; application — a function of type $\sigma$ $\to\tau$ may only be applied to an argument of type $\sigma$ , and the result gets type $\tau$ .

There are two important properties: the first is strong normalization: every typable term has a normal form, and every reduction order reaches it — as a consequence, $\Omega$ and $\mathrm{Y}$ are untypable and the language is not Turing-complete; the second is subject reduction: the type is preserved under reduction — “computation does not spoil the type”.

What about polymorphism? Polymorphism in types, that is. $\lambda^{\to}$ has none: the identity function $\lambda x{:}\alpha.\,x$ is tied to one particular type $\alpha$ , and it has to be written anew for every type. Girard and Reynolds removed this restriction by allowing terms to abstract not only over values but also over types themselves — the result is System F, where the following holds:

\displaystyle \mathrm{id}

\displaystyle = \Lambda\alpha.\,\lambda x{:}\alpha.\,x \;:\; \forall\alpha.\,\alpha

\displaystyle \to\alpha

Here $\Lambda\alpha$ is abstraction over a type: $\mathrm{id}$ first takes a type $\alpha$ , then a value $x$ of that type, and returns it unchanged. The type $\forall\alpha.\,\alpha$ $\to\alpha$ reads “for any type $\alpha$ , a function from $\alpha$ to $\alpha$ ”: one and the same $\mathrm{id}$ applies to a number, a boolean, a function — polymorphism became part of the calculus itself.

Type inference in full System F is undecidable, so Haskell uses a decidable fragment — the Hindley–Milner system (algorithm W), where all types are inferred without annotations; it is the subject of the next section.