Foundations of Functional Programming/Pure type systems

Pure type systems are a wide class of explicitly typed λ-calculi which greatly generalize the systems of the λ-cube. They generalize them by relaxing restrictions on the number of sorts, and the rules governing the sorts.

The systems of the λ-cube had two sorts, $\text{Type}$ and ${\text{Type}}_1$, with $\text{Type}:{\text{Type}}_1$. They had $(s_1,s_2)$ rules which said how types of different sorts could be used to form function types.

In pure type systems, there can be any number of sorts, and any type relationships between them. The $(s_1,s_2)$ rules of the λ-cube systems are generalized to so-called $(s_1,s_2,s_3)$ rules, which relax the restriction that function types formed from types of sorts $s_1$ and $s_2$ must have the sort $s_2$ of the codomain type.

Syntax

The syntax of pure type systems is the same as that of the systems of the λ-cube, except that the set of sorts may be different. Expressions have the same syntax, which we repeat here:

$\begin{array}{ccc}\text{Expr}& ::=& \text{Var}\\ & |& \text{Const}\\ & |& \text{Expr}\text{Expr}\\ & |& \lambda \text{Var}:\text{Expr}.\text{Expr}\\ & |& (\text{Var}:\text{Expr})\to \text{Expr}\end{array}$

Recall that we denote denote variables by $a,b,c,...$, and when we need to refer to an arbitrary constant, we use bold lower case letters $𝐚,𝐛,...$. We use $A,B,C,...$ to denote arbitrary expressions.

Declarations and contexts are defined as with the λ-cube.

Specifications

A pure type system is defined by a "specification." The specification says what sorts the system has; what type relationships exist between the sorts; and what $(s_1,s_2,s_3)$ rules the system has. Precisely, a specification is a tuple $(S,A,R)$, where:

• $S$ is a set of constants, the sorts.
• $A$ is the set of "axioms." It is a set of statements of the form $s_1:s_2$, where $s_1$ and $s_2$ are sorts.
• $R$ is the set of "rules." It is a set of triples $(s_1,s_2,s_3)$, where $s_1,s_2,s_2$ are sorts.

Type theory

The notions of β-reduction and β-conversion are defined for pure type systems in the same way as for systems of the λ-cube.

Let $(S,A,R)$ be a specification for a pure type system. The typing rules for the system described by the specification are:

(axioms)	$⊢s_1:s_2$	if $(s_1:s_2)\in A$
(start)	$\frac{\mathrm{\Gamma }⊢A:s}{\mathrm{\Gamma },x:A⊢x:A}$	if $x\notin \mathrm{\Gamma }$
(weakening)	$\frac{\mathrm{\Gamma }⊢A:B\mathrm{\Gamma }⊢C:s}{\mathrm{\Gamma },x:C⊢A:B},\text{if}x\notin \mathrm{\Gamma }$
(application)	$\frac{\mathrm{\Gamma }⊢F:(x:A)\to B\mathrm{\Gamma }⊢C:A}{\mathrm{\Gamma }⊢FC:B[x/C]}$
(abstraction)	$\frac{\mathrm{\Gamma },x:A⊢B:C\mathrm{\Gamma }⊢(x:A)\to C:s}{\mathrm{\Gamma }⊢(\lambda x:A.B):(x:A)\to C}$
(conversion)	$\frac{\mathrm{\Gamma }⊢A:B\mathrm{\Gamma }⊢B^{\prime }:sB{\equiv }_{\beta }{B}^{\prime }}{\mathrm{\Gamma }⊢A:B^{\prime }}$
($(s_1,s_2,s_3)$ rules)	$\frac{\mathrm{\Gamma }⊢A:s_1\mathrm{\Gamma },x:A⊢B:s_2}{\mathrm{\Gamma }⊢(x:A)\to B:s_3}$	if $(s_1,s_2,s_3)\in R$

These rules are the same as the rules for the systems of the λ-cube, except that the axioms are suitably generalized and the $(s_1,s_2,s_3)$ rules replace the $(s_1,s_2)$ rules.

Examples of pure type systems

Every explicitly typed λ-calculus we have described so far can be formulated as a pure type system. For example, the second-order λ-calculus can be formulated as follows:

$S$	$\text{Type},{\text{Type}}_1$
$A$	$\text{Type}:{\text{Type}}_1$
$R$	$(\text{Type},\text{Type},\text{Type}),({\text{Type}}_1,\text{Type},\text{Type})$

It is straightforward to formulate the rest of the systems of the λ-cube as pure type systems.

λ* (naïve type theory)

Another important pure type system is the system λ*, which we also refer to as naïve type theory. This system is distinguished by the fact that it has just a single sort, $\text{Type}$, with the axiom $\text{Type}:\text{Type}$. Here is the specification:

$S$	$\text{Type}$
$A$	$\text{Type}:\text{Type}$
$R$	$(\text{Type},\text{Type},\text{Type})$

As we have already noted, the assumption that $\text{Type}:\text{Type}$ gives rise to Girard's paradox, which renders λ* inconsistent.

At first blush, one might think that this result is caused by the circularity of the assumption that $\text{Type}:\text{Type}$; many logical paradoxes, such as Russell's paradox and the liar paradox, are due to circularities of various kinds. However, Girard showed that the inconsistency also arises in the following pure type system, which has no obvious circularity (see Barendregt (1992)):

$S$	${\text{Type}}_0,{\text{Type}}_1,{\text{Type}}_2$
$A$	${\text{Type}}_0:{\text{Type}}_1,{\text{Type}}_1:{\text{Type}}_2$
$R$	$({\text{Type}}_0,{\text{Type}}_0,{\text{Type}}_0),({\text{Type}}_1,{\text{Type}}_0,{\text{Type}}_0),({\text{Type}}_1,{\text{Type}}_1,{\text{Type}}_1),({\text{Type}}_2,{\text{Type}}_1,{\text{Type}}_1),({\text{Type}}_2,{\text{Type}}_0,{\text{Type}}_0)$

Properties of pure type systems

The familiar properties we have seen in all the explicitly typed systems discussed so far do not always hold in the more general context of pure type systems. However, for each of them we can identify fairly broad classes of pure type systems for which they hold.

Of the properties we have discussed with previous systems, the only one that holds in all pure type systems is that β-reduction preserves type. That is, if $\mathrm{\Gamma }⊢A:T$ and and $A$ β-reduces to $A^{\prime }$, then $\mathrm{\Gamma }⊢A^{\prime }:T$.

Not all pure type systems have the [[../Strongly and weakly normalizing λ-calculi|strong normalization property]]. In an inconsistent pure type system, there are terms of every type. It can be proven that an expression of a type which corresponds to an arbitrary false statement must have no normal form, meaning that not all typeable terms are normalizing.

If a pure type system has the strong normalization property, then the problems of type checking and typability are decidable for that pure type system.

Many pure type systems also preserve the property that every expression has at most one type, up to β-convertibility. Recall that this property states that for any expression $A$ and any context $\mathrm{\Gamma }$, if two expressions $B$ and $B^{\prime }$ are such that $\mathrm{\Gamma }⊢A:B$ and $\mathrm{\Gamma }⊢A:B^{\prime }$, then $B{\equiv }_{\beta }{B}^{\prime }$.

Though many pure type systems have this property, not all do. In particular, it is trivial to break this property using axioms, as in the following pure type system:

$S$	$\text{Type},{\text{Type}}_1$
$A$	$\text{Type}:\text{Type},\text{Type}:{\text{Type}}_1$
$R$	$(\text{Type},\text{Type},\text{Type}),({\text{Type}}_1,\text{Type},\text{Type})$

In this pure type system, $\text{Type}$ has two non-β-convertible types -- $\text{Type}$ and ${\text{Type}}_1$ -- by fiat.

However, it can also be shown that this kind of stipulation is the only thing that can break the unique typability property in pure type systems. If a pure type system $(S,A,R)$ is such that no sort appears on the left hand side of more than one statement in $A$, then every expression has at most one type up to β-conversion in that system. A pure type system with this property, that no sort is assigned more than one sort by the axioms, is called "singly sorted."