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 .