Computer Aided Formal Reasoning Fall, 1995 Lecture notes 9 Judith Underwood

Quantification over types

Today we will look at type universes and quantification (both universal and existential) over Type. We have used universal quantification over both Prop and Type, but we have not looked carefully at the difference. We have also not seen how existential quantification extends to Type.

We will introduce rules two new type constructors, called Π and Σ. We are already familiar with Π – it is just another name for the dependent function type we have been using to describe quantification. Σ types are a different form of existential types.

We will first look at typing rules for terms in Π types, then Σ types. We will then give formation rules for Π and Σ types. It is in the formation rules that we shall see how the Π and Σ types differ from the universal and existential quantification in Prop.

Π types

We will begin with Π types, since we are already familiar with them. In Lego, the rules for introduction and elimination of Π are as follows:

                               \frac{G, x:A ⊢b:B}{G ⊢[x:A]b :\{x:A\}B}

The Lego notation [x:A]b : {x:A}B is written elsewhere λx: A.b : Πx: A.B. (Here, Lego has a certain advantage in that it is easier to parse.) In this rule, x may be free in B (but not in G). If x is free in B, it becomes bound in {x:A}.B.

                              \frac{G ⊢f:\{x:A\}B   G ⊢a:A}{G ⊢f a:B[a/x]}

Note that if x is not free in B, these rules are the same as those for the function type A →B. Because of this, Π types are sometimes called “dependent function types”. (They are also called “dependent product types” by those who consider that the operator describes the (possibly infinite) Cartesian product of all the B[x] as x ranges over A.)

The terms in Π types compute the same way that the ordinary functions do – the difference is solely in the fact that the type of the result may depend on the argument to the function. This is the Type version of universal quantification; we’ll compare it to universal quantification in Prop later.

Σ types

The rules for introduction and elimination of Σ are as follows:

                              \frac{G ⊢a:A   G ⊢b:B[a/x]}{G ⊢(a,b):<x:A>B}

Again, x may be free in B. If x is free in B, it becomes bound in <x:A>B.

                                  \frac{G ⊢M:<x:A>B}{G ⊢M.1:A}

                                \frac{G ⊢M:<x:A>B}{G ⊢M.2:B[M.1/x]}

Note that if x is not free in B, these rules just describe a cartesian product type A × B. Because of this, Σ types are sometimes called “dependent product types”. (Recall that Π types are also sometimes called dependent product types. Those who call Π dependent product will call Σ a “dependent sum type,” considering it as a disjoint union of the B[x] as x ranges over A, represented by tagging elements with the associated element of A.)

The terms in Σ types compute the same way that the ordinary pairs do – again, the difference is only in the fact that the type of the second component of the pair may depend on the first component.

Σ and Π as quantification

The dependent Σ and Π types can be interpreted as representing predicative quantification over types. This interpretation entails a particular choice about the meaning of quantification, namely, that quantifiers range over elements of a particular, named type. The fundamental difference between Prop and Type lies in precisely what the quantified variables range over. In Type, we are actually quantifying over type universes Type(0),Type(1), … as explained below.

As with Prop, we can consider Π types to represent universal quantification. {x:A}B asserts that for all x of type A, B holds (really B is inhabited). Thus an element of this type produces something in B[a/x] for every a:A. The type <x:A>B corresponds to ∃x : A.B in the sense that <x:A>B has an inhabitant if there exists a of type A such that we can construct an inhabitant of

B[a/x].

Unlike Prop, we do not wish to include the type currently being defined in the range of the quantified variable. To do this, we construct a hierarchy of universe types (types which contain other types as elements). The idea is to begin with a lowest type universe Prop containing base objects and building on top of it universes Type(i) where in Type(i) types which are defined by quantification over elements of universes Type(j) where j < i. More formally, we can write this as the following type construction rules:

                        \frac{G ⊢A:Type(i)   G, x:A ⊢B:Type(i)}{G ⊢\{x:A\}B : Type(i)}

Note that this Π is created by quantifying over an element of Type(i), not all of Type(i) itself. This means that the quantified type is still in Type(i).

It may be easier to understand this if we consider a different rule:

                    (*)  \frac{G ⊢A:Type(i)   G, x:A ⊢B:Type(j)}{G ⊢\{x:A\}B : Type(max(i,j))}

We have a similar rule for Σ:

                        \frac{G ⊢A:Type(i)   G, x:A ⊢B:Type(i)}{G ⊢<x:A>B : Type(i)}

These rules describe the relationship between the universes:

                                 \frac{G ⊢A:Type(i)}{G ⊢A:Type(i+1)}

                               \frac{i < j}{G ⊢Type(i):Type(j)}

Exercise: Show that (each instance of) rule (*) is derivable from the other rules.

Note that we have lost some of the distinction between terms and types, since types are elements of types as well of terms. Nevertheless, we can make some distinction by declaring those things in some universe type (including Prop) to be types.

In this system, we can only define a type T by quantifying over types T′ which may not contain T. This is called a predicative definition. Compare this with Prop, where we have the rule

                              \frac{G, x:Prop ⊢B:Prop}{G ⊢\{x:Prop\}B : Prop}

In other words, we are defining an element of Prop by quantifying over all elements of Prop – including the one we are currently defining. This is impredicative quantification.

Application

Using Σ types, we can write a specification as a type. For instance, consider the integer square root function, which, given x, returns the greatest integer y less than or equal to \sqrt{x}. In other words, we must have y^{2} ≤ x and x < (y + 1)^{2}. We can now write the type of this function as a logical statement “For all x, there exists y such that y^{2} ≤ x and x < (y + 1)^{2}.” In Lego, this is

{x:nat}<y:nat> (and (or (Lt (times y y) x) (Eq (times y y) x))
                    (Lt x (times (suc y) (suc y))))

(we have expanded ≤ into a disjunction, < or =). Considered as a type, any element of this type is an integer square root function, i.e. if we have that f is in this type, then for any n, we have

(and (or (Lt (times (f n) (f n)) n) (Eq (times (f n)(f n)) n))
     (Lt n (times (suc (f n)) (suc (f n)))))

Very hard exercise: Derive an element of this type. To do this as written, you need a few tricks. As I write this, I am computing the integer square root of 1; it has taken more than 9 minutes so far on craro.

Three part exercise:

1. Meditate on the ways in which Π is a product type and the ways in which it is a function type.

2. Meditate on the ways in which Σ is a sum type and the ways in which it is a product type.

3. Decide to call them Π and Σ types.