The Typed Polymorphic $\lambda$-Calculus

We assume a set $\ensuremath{\mathbf{C}}$ of pregiven constants ususally denoted by $a, b \ldots$, and a countably infinite set of variable symbols $\ensuremath{\mathbf{V}}$ usually denoted by $x, y, \ldots$. The syntax of a term $t$ of the $\lambda$-Calculus is given by the following grammar:

$$\begin{array}{rrlll} t & ::= & a & (a\in\ensuremath{\mathbf{C... ...traction} \ & \vert & t\;t & & \mbox{application} \end{array}$$ (8)

We shall call $\ensuremath{\mathbf{T}}$ the set of terms $t$ defined by this grammar. These terms are also called raw terms.

An abstraction $\lambda x.t$ defines a lexical scope for its bound variable $x$, whose extent is its body $t$. Thus, the notion of free occurrence of a variable in a term is defined as usual, and so is the operation $t_1[t_2/x]$ of substituting a term $t_2$ for all the free occurrences of a variable $x$ in a term $t_1$. Thus, a bound variable may be renamed to a new one in its scope without changing the abstraction.

The computation rule defined on $\lambda$-terms is the so-called $\beta$-reduction:

$$\begin{array}{rl} (\lambda x.t_1)\;t_2 & \;\longrightarrow\;t_1[t_2/x]. \end{array}$$ (9)

We assume a set $\ensuremath{{\mathcal B}}$ of basic type symbols denoted by $A, B, \ldots$, and a countably infinite set of type variables $\ensuremath{{\mathcal V}}$ denoted by $\alpha, \beta, \ldots$. The syntax of a type $\tau$ of the Typed Polymorphic $\lambda$-Calculus is given by the following grammar:

$$\begin{array}{rrlll} \tau & ::= & A & (A\in\ensuremath{{\math... ...ert & \tau\rightarrow \tau & & \mbox{function type} \end{array}$$ (10)

We shall call $\ensuremath{{\mathcal T}}$ the set of types $\tau$ defined by this grammar. A monomorphic type is a type that contains no variable types. Any type containing at least one variable type is called a polymorphic type.

The terms of the Typed Polymorphic $\lambda$-Calculus are only those raw terms in $\ensuremath{\mathbf{T}}$ that admit a well-defined type in $\ensuremath{{\mathcal T}}$. Each constant in $\ensuremath{\mathbf{C}}$ is assumed to have a unique type in $\ensuremath{{\mathcal T}}$, and we write $\ensuremath{\mathbf{type}}(a)=\tau$ to mean that constant $a$ has type $\tau$.

One may assign types to symbols using a type context $\Gamma$, which is a partial function from $V$ to $\ensuremath{{\mathcal T}}$. Given a type context $\Gamma$, a variable $x\in\ensuremath{\mathbf{V}}$ and a type $\tau\in\ensuremath{{\mathcal T}}$, we define:

$$\Gamma[x:\tau](y) \ensuremath{\;\stackrel{\mbox{\tiny def}}{=}\;}... ... \mbox{if $x = y$}; \ \ \Gamma(y) & \mbox{if $x\neq y$}. \end{array}\right.$$ (11)

In other words, $\Gamma[x:\tau]$ coincides with $\Gamma$ everywhere on $\ensuremath{\mathbf{V}}$ except at $x$, where it takes the value $\tau$. The empty context is the function noted $\emptyset$ defined nowhere on $\ensuremath{\mathbf{V}}$.

To find out whether a term $t$ in $\ensuremath{\mathbf{T}}$ is well-typed, one must exhibit a type assignment that constitutes a suitable typing context for the variable symbols occurring in $t$, and from which one may ascribe a (unique) type for the whole term. Given a type context $\Gamma$, a term $t$, and a type $\tau$, a type judgement is an expression of the form $\Gamma\;\vdash\;t : \tau$, which stands to mean that $t$ has been deemed to have type $\tau$ when the symbols occurring in it have the types assigned to them by the context $\Gamma$. Without a type context $\Gamma$, the expression $t:\tau$ is used to mean that $\Gamma\;\vdash\;t : \tau$ for some $\Gamma$.

Deriving types for terms is done using typing rules of the form:

$$\displaystyle\frac{\Gamma_1\;\vdash\;t_1 : \tau_n , \cdots \Gamma_n\;\vdash\;t_n : \tau_n }{\Gamma\;\vdash\;t : \tau }$$

which is read as follows: ``$t$ has type $\tau$ under $\Gamma$ if $t_1$ has type $\tau_1$ under $\Gamma_1$, ..., and $t_n$ has type $\tau_n$ under $\Gamma_n$.'' Note that it is possible that $n=0$, in which case the rule is written:

$$\displaystyle\frac{}{\Gamma\;\vdash\;t : \tau }$$

and it is called an axiom.

The typing rules for the Typed Polymorphic $\lambda$-Calculus are given in Figure 4.

Figure 4: Typing rules for the Typed Polymorphic $\lambda$-Calculus

These rules can be readily translated into a Logic Programming language based on Horn-clauses such as Prolog, and used as an effective means to infer the types of expressions based on the Typed Polymorphic $\lambda$-Calculus.

The basic syntax of the Typed Polymorphic $\lambda$-Calculus may be extended with other operators and convenient data structures as long as typing rules for the new constructs are provided. Typically, one provides at least the set $\ensuremath{\mathbb{N}}$ of integer constants and $\ensuremath{\mathbb{B}}=\{\ensuremath{\mathfrak{true}},\ensuremath{\mathfrak{false}}\}$ of boolean constants, along with basic arithmetic and boolean operators, pairing (or tupling), a conditional operator, and a fix-point operator. The usual arithmetic and boolean operators are denoted by constant symbols (e.g., $+, *, -, /, \vee, \wedge,$ etc.). Let $\ensuremath{\mathbf{O}}$ be this set.

The computation rules for these operators are based on their usual semantics as one might expect, modulo transforming the usual binary infix notation to a ``curryed'' application. For example, $t_1+t_2$ is implicitly taken to be the application $(+\;t_1)\;t_2$. Note that this means that all such operators are implicitly ``curryed.''⁷

For example, we may augment the grammar for the terms given in (8) as follows:

$$\begin{array}{rrlll} t & ::= & a & (a\in\ensuremath{\mathbf{C... ...\ensuremath{\mathfrak{fix}}\;t & & \mbox{recursion} \end{array}$$ (12)

The computation rules for the other new constructs are:

$$\begin{array}{rl} \langle t_1, \cdots, t_k\rangle .i & \;\lon... ...longrightarrow\;t\;(\ensuremath{\mathfrak{fix}}\;t) \end{array}$$ (13)

To account for the new constructs, the syntax of types is extended accordingly to:

$$\begin{array}{rrlll} \tau & ::= & \ensuremath{\mathtt{int}}\;... ...ert & \tau\rightarrow \tau & & \mbox{function type} \end{array}$$ (14)

We are given that $\ensuremath{\mathbf{type}}(n)=\ensuremath{\mathtt{int}}$ for all $n\in\ensuremath{\mathbb{N}}$ and that $\ensuremath{\mathbf{type}}(\ensuremath{\mathfrak{true}})=\ensuremath{\mathtt{bool}}$ and $\ensuremath{\mathbf{type}}(\ensuremath{\mathfrak{false}})=\ensuremath{\mathtt{bool}}$. The (fully curried) types of the built-in operators are given similarly; i.e., $\ensuremath{\mathbf{type}}(+)=\ensuremath{\mathtt{int}}\rightarrow (\ensuremath{\mathtt{int}}\rightarrow \ensuremath{\mathtt{int}})$, $\ensuremath{\mathbf{type}}(\vee)=\ensuremath{\mathtt{bool}}\rightarrow (\ensuremath{\mathtt{bool}}\rightarrow \ensuremath{\mathtt{bool}})$, etc., ...The typing rules for this extended calculus are given in Figure 5.

Figure 5: Typing rules for an Extended Typed Polymorphic $\lambda$-Calculus