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 socalled rules, which relax the restriction that function types formed from types of sorts and must have the sort of the codomain type.
Syntax
[edit  edit source]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.
Specifications
[edit  edit source]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
[edit  edit source]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  
(weakening)  
(application)  
(abstraction)  
(conversion)  
( rules) 

if 
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
[edit  edit source]Every explicitly typed λcalculus we have described so far can be formulated as a pure type system. For example, the secondorder λ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)
[edit  edit source]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
[edit  edit source]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."