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 g takes a pair
as an argument, where x
is an integer and p is a proof that the integer is nonnegative.
The set construct is defined in such a way that f takes only
integers as arguments to the computation; the information
that the argument is nonnegative can only be used noncomputationally
in proofs.
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 g mapping
into int
such that for all p in 
, 
.
(Notice that p is a pair 
, where 
and e is
a proof that f has a zero, so 
.)
That is, the function g simply picks out the witness for
the quantifier in 
.
There is no such function h from 
because the only input to h is the function f, so
in order to find a zero value h would need to search
through int for a zero. In the language described
so far there is no unbounded search operator to use
in defining h.
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 
.
