We
conclude the introduction of the type theory with
some remarks about two, more complex type constructors, the subtype
constructor and the quotient type constructor.
Informal reasoning about functions and types involves the
concept of subtypes.
A general way to specify subtypes uses a concept similar
to the * set comprehension* idea in set theory; that is,
is the type of all **x** of type **A** satisfying the
predicate **B**.
For instance, the nonnegative integers
can be defined from the integers as .
In Nuprl
this is one of two ways to specify a subtype.
Another way is to use the type .
Consider now two functions on the nonnegative integers
constructed in the following two ways.

The function

The difference between these notions of subset is more pronounced with a more involved example. Suppose that we consider the following two types defining integer functions having zeros.

It is easy to define a function

One can think of the set constructor, , as serving two purposes. One is to provide a subtype concept; this purpose is shared with . The other is to provide a mechanism for hiding information to simplify computation.

The quotient operator builds a new type from a given
base type, **A**, and an equivalence relation, **E**, on **A**.
The syntax for the quotient is .
In this type the equality relation is **E**,
so the quotient operator is a way of redefining equality
in a type.

In order to define a function one must
show that the operation respects **E**, that is, implies
.
Although the details of showing **f** is well--defined may
be tedious, we are guaranteed that concepts defined in
terms of **f** and the other operators of the theory respect
equality on .
As an example of quotienting changing
the behavior of functions, consider defining the
integers modulo 2 as a quotient type.

We can now show that successor is well--defined on by showing that if then . On the other hand, the maximum function is not well--defined on because but and , meaning that it is not the case that .

Thu Sep 14 08:45:18 EDT 1995