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{... ...raction} \\ & \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₁[t₂/x] of substituting a term t₂ for all the free occurrences of a variable x in a term t₁. 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{{\mat... ...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}}{... ...}; \\ \\ \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{<}{t}ex2html_comment_mark> {\Gamma_1\;\vda... ...ts\ \Gamma_n\;\vdash\;t_n : \tau_n} {\Gamma\;\vdash\;t : \tau}$$

which is read as follows: ``t has type $\tau$ under $\Gamma$ if t₁ 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: 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<sub>1</sub>+t<sub>2</sub>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{... ...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... ...ongrightarrow\;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: Typing rules for an Extended Typed Polymorphic $\lambda$-Calculus