LARA

Simply Typed Lambda Calculus

A restriction of Untyped Lambda Calculus to type terms that has simpler semantics.

  • foundation of modern functional programming languages (when extended with recursion)
  • particularly suitable as a foundation of logic: due to termination properties

Simple Types

Consider a family of base types $B$.

The set of simple types are defined by grammar

\begin{equation*} \tau ::= B \mid (\tau \Rightarrow \tau) \end{equation*}

The type $\tau_1 \doublerightarrow \tau_2$ is meant to denote functions from $\tau_1$ to $\tau_2$ (whether it denotes total or partial or computable functions, depends on particular semantics).

In simply typed lambda calculus, each variable is assigned one type from $\tau$.

Syntax of System with Concrete Types

Given a family of base types, a term $T$ of simply typed lambda calculus is like a term of Untyped Lambda Calculus, but carries a type. We define it as follows:

  • variable of type $\tau$ is a term of type $\tau$
  • if $t$ has type $\tau$ and $x$ is a variable of type $\sigma$, then $\lambda x.t$ is a term of type $(\sigma \doublerightarrow \tau)$
  • if $t_1$ is a term of type $\sigma \doublerightarrow \tau$ and $t_2$ is a term of type $\sigma$, then $t_1 t_2$ is a term of type $\tau$

Notation using type rules:

\begin{equation*}\begin{array}{l} \displaystyle \frac{}{x :: \tau}, \mbox{ i{}f } x \in V_\tau \\ \ \\ \displaystyle \frac{t :: \tau}{(\lambda x.t) :: (\sigma \Rightarrow \tau)} \mbox{ i{}f } {x \in V_\sigma} \\ \ \\ \displaystyle \frac{t_1 :: (\sigma \Rightarrow \tau),\ t_2 :: \sigma}{(t_1 t_2) :: \tau} \end{array}\end{equation*}

Note that there is no way to assign a type to $x$ such that the term $\lambda x. x x$ is well typed. Therefore, $\lambda x.xx$ is not a term of simply typed lambda calculus.

Hindley-Milner Type Inference

Hindley-Milner type inference uses unification to infer possible types of lambda terms, even if we do not specify types for variables. The problem reduces to unification in language that has as many constants as there are base types, and one binary constructor (function constructor).

In some cases, such as $\lambda x.x$, there is an infinite family of possible concrete types. In such cases, Hindley-Milner inference computes the most-general unifier of constraints, which gives polymorphic type. For simplicity we assume that we have obtained some concrete types for variables and therefore for lambda terms.

Strong Normalization

Unlike beta reduction on typed terms, beta reduction on typed terms always terminates and the result does not depend on the order of applying beta reductions in the term. (Proof requires some work, and there are several variants; there are some short and elegant proofs that interpret based on set theory, see Barendregt's chapter.)

The consequence is that for each term in simply typed lambda calculus we can compute a normal form where all beta reductions were applied.