Also see Equality for supplementary material.

Next: Propositions as Types Up: Introduction to Type Previous: Atoms and Lists

# Equality and Propositions as Types

So  far we have talked exclusively about types and their members. We now want to talk about simple declarative statements. In the case of the integers many interesting facts can be expressed as equations between terms. For example, we can say that a number n is even by writing . In Nuprl the equality relation on int is built--in; we write . In fact, each type A comes with an equality relation written . The idea that types come equipped with an equality relation is very explicit in the writings of Bishop [Bishop 67]. For example, in The Foundation of Constructive Analysis, he says, ``A set is defined by describing what must be done to construct an element of the set, and what must be done to show that two elements of the set are equal.'' The notion that types come with an equality is central to Martin-Löf 's type theories as well.

The equality relations play a dual role in Nuprl in that they can be used to express type membership relations as well as equality relations within a type. Since each type comes with such a relation, and since is a sensible relation only if a and b are members of A, it is possible to express the idea that a belongs to A by saying that is true. In fact, in Nuprl the form is really shorthand for .

The equality statement has the curious property that it is either true or nonsense. If a has type A then is true; otherwise, is not a sensible statement because is sensible only if a and b belong to A. Another way to organize type theory is to use a separate form of judgement  to say that a is in a type, that is, to regard as distinct from . That is the approach taken by Martin-Löf . It is also possible to organize type theory without built--in equalities at all except for the most primitive kind. We only need equality on some two--element type, say a type of booleans, ; we could then define equality on int as a function from int into The fact that each type comes equipped with equality complicates an understanding of the rules, as we see when we look at functions. If we define a function then we expect that if then . This is a key property of functions, that they respect equality.

In order to guarantee this property there are a host of rules of the form that if part of an expression is replaced by an equal part then the results are equal. For example, the following are rules.

Next: Propositions as Types Up: Introduction to Type Previous: Atoms and Lists

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995