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, and , with . They had 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 rules of the λ-cube systems are generalized to so-called rules, which relax the restriction that function types formed from types of sorts and must have the sort of the codomain type.



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:


Recall that we denote denote variables by  , and when we need to refer to an arbitrary constant, we use bold lower case letters  . We use   to denote arbitrary expressions.

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



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   rules the system has. Precisely, a specification is a tuple  , where:

  •   is a set of constants, the sorts.
  •   is the set of "axioms." It is a set of statements of the form  , where   and   are sorts.
  •   is the set of "rules." It is a set of triples  , where   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   be a specification for a pure type system. The typing rules for the system described by the specification are:

(axioms)   if  
(start)   if  
(  rules)



These rules are the same as the rules for the systems of the λ-cube, except that the axioms are suitably generalized and the   rules replace the   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:


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,  , with the axiom  . Here is the specification:


As we have already noted, the assumption that   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  ; 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)):


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   and and   β-reduces to  , then  .

Not all pure type systems have the 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   and any context  , if two expressions   and   are such that   and  , then  .

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:


In this pure type system,   has two non-β-convertible types --   and   -- 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   is such that no sort appears on the left hand side of more than one statement in  , 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."