The quotient type provides a powerful abstraction mechanism and puts a user--defined equality into the theory so that the rules for reasoning about equality (the equality and substitution rules and all the intro rules for equality of noncanonical members) can be applied to it. The obverse of this is that if x is declared in a hypothesis list to be in a quotient type then any type T which appears as a later hypothesis or as the conclusion must be independent of the representation of x; that is, it must yield equal types when different but equal elements of the quotient type are substituted for x. For example, for t in T to be true under the assumption that x is in some quotient type, it is required that both t and T be independent of the representative for x (see the quotient--elim rule). Therefore, if we define the rational numbers to be the obvious quotient on pairs of integers whose second component is nonzero, then we will not be able to show that the following definition of less--than is a type:
<x:Q> < <y:Q> in Q ==
fst(<x>)*snd(<y>) < fst(<y>)*snd(<x>).
The difficulty here is that type equality in Nuprl
is strong;
two types are equal if they are structurally the same, and
so there are types which have the same members but are not equal.
In particular,
two less--than types can be shown to be equal
only if it can be shown that their corresponding components
are equal as integers.
Therefore, if we could show that the above were a type
then for any pairs of integers <i,j>, <i',j'>, and
<m,n>
such that
<i,j> and <i',j'> are equal as rational numbers, we would have
( i*n < m*j ) = ( i'*n < m*j' ) in U1. In particular, we would have
i*n = i'*n in int,which is not always true. Thus we cannot use the above definition of less--than over the quotient--type Q. However, we are only interested in the truth value of less--than, i.e., whether or not it is inhabited, and this property is independent of representatives. In this situation, we squash the type. Define
||<T:type>|| == {0 in int|<T>}.
This squashes a type in the sense that given a type T,
it produces a type which has one element if T is
inhabited and is empty otherwise.
For the less--than example, we define less--than to be
the squash of what it was before, and the result is a
type, since to show that two set types are equal
involves showing the proposition parts are equivalent
instead of equal. (See the
rule for equality of set types.) More specifically, to prove
||T|| = ||
|| in Ui ,
one only has to be able to prove
T => 
and
=> T.
In general, this use of the squash operator will often be
required when
one wishes to create a type which deals with the representations
of objects from a quotient type.
Note that squashing does away with any computational content that the
type might have had (this will be discussed further later in
this section). If you are interested in that content and you cannot
reformulate so as to bring out from under the squash operator the part
you are interested in, you cannot use the quotient type and must treat
the equality you want as you would any other defined relation.
More precisely, suppose that Q is some quotient type and 
is some property of members of Q that one wishes to express in Nuprl
.
If, as above, one is interested only in the truth value of 
,
i.e., whether or not its type representation is inhabited, and if
the truth value respects the equality relation of Q, then the squash
operator can be applied. Usually in this case the type resulting
from a direct translation of 
according to the propositions--as--types
principle will have at most one member, and that member will be known in
advance (e.g., axiom), so one would lose nothing by squashing.
Often, however, P will have some content of interest; for example,
it might involve an assertion of
the existence of some object, and one might wish to construct
a function which takes a member x of Q satisfying 
to the object
whose existence is asserted, but this may not be possible if the
property has been squashed. What one has to do in this case is to
separate 
into two pieces so that it can be expressed by a type
z:T # ||
||, or equivalently, {z:T|
}, where T
represents the computationally interesting part and 
represents the
part of which only the truth value is interesting. This requires
that the type T respect equality in x and
that for any two representatives chosen for x the collection
of computationally interesting objects be the same.
We illustrate the points raised above with an example. The usual formulation of the constructive real numbers is as a certain set of sequences of rational numbers with known convergence rates, where two such sequences are considered equal if they are the same in the limit. One crucial property of real numbers is that each one has a rational approximation to within any desired accuracy. Given a particular real number, obtaining such an approximation simply involves picking out an element suitably far along in the sequence, since the convergence rate is known. However, clearly one can have two different but equal real numbers for which this procedure gives two different answers, and in fact it is impossible constructively to come up with approximations in a way which respects equality. Since many computations over the real numbers involve approximations, one cannot bury the property of having a rational approximation under the squash operator. The upshot is that the constructive reals cannot be ``encapsulated'' as a quotient type; one must take the reals to be just the type of rational sequences and treat the equality relation separately. However, one can still use the quotient type to some extent in a situation such as this. For example, in the real number case one can still form the quotient type and use it to express the equality relation. Thus, although hypothetical real numbers will be members of the unquotiented version, one can express equality between reals as equality in the quotient type and so can use the equality rule, etc., to reason about it.
It should not be concluded from the preceding discussion that one should never represent anything with the quotient type. There is a wide class of domains for which the quotient as a device for complete abstraction with respect to equality is a safe choice. This class consists of those domains where the desired equality is such that canonical representatives exist, i.e., where one can prove the existence of a function from the quotient type to its base type which takes equal members of the quotient type to the same member of the equivalence class in the base type. This will allow one to express properties which do not respect equality by having them refer to the canonical representative. An example of a common domain with this property is the rational numbers, where the canonical representative for a fraction is the fraction reduced to lowest terms.
The squash operation defined earlier is just one particular use of the information--hiding capability of the set type. It can also be used to remove from the ``computational part'' of the theorem information whose computational content is uninteresting and which would otherwise reduce the efficiency of the extracted code or information which would make the theorem weaker than one desired. As an example of the first kind of information, we could define the type of integers which are perfect squares two different ways:
n:int # Some m:int. (n=m*m in int)or
{ n:int | Some m:int. (n=m*m in int) }.
Suppose we had some variable declared in a hypothesis
to be in one of the perfect square types. In each case we could
eliminate it to get an integer which we know to be a
perfect square. In the first case we could do another elimination
to get our hands on the integer whose square is the first integer,
and we could use this square root freely in the proof of the conclusion.
However, this will not be allowed in the second case.
The system will ensure that the proof that the number is
a square is not used in the
term which is built
as the proof of the conclusion. On the other hand, if one
is interested only in the integer which is a perfect square, and
only needs the perfect square property to prove something about
a program which does not need the square root, then the
second version can be used to get
a more efficient extracted object.
As an example of the second kind of information hiding referred to above, consider the specification of a function which is to search an array of integers for a given integer and return an index, where it is known in advance that the integer occurs in the array. If integer arrays of length n are represented as functions from {1..n} to the integers, where {1..n} is defined to be the appropriate subset of the integers, a naive translation of the requirements for the search program into the Nuprl logic might be the following:
All n:N. All a:{1..n}->int. All k:int.
Some i:{1..n}. a(i)=k in int
=> Some i:{1..n}. a(i)=k in int
This specifies a trivial function which requires as an argument the
answer which it is to produce,
and so it does not capture the meaning of the informal
requirements.
This problem is solved by use of the set type to ``hide''
the proof of the fact that k occurs in the array.
If we make the Nuprl
definition
All <x>:<T> where <P>. <P'> ==
<x>: {<x>:<T>|<P>} -> <P'>
then we can give the correct specification as
All n:N. All a:{1..n}->int.
All k:int where ( Some i:{1..n}. a(i)=k in int ) .
Some i:{1..n}. a(i)=k in int
In a proof of this assertion, if one has done intro steps to
remove the universal quantifiers and thus has n,
a and k declared in the hypothesis list, then the type that
k is in is a set type. The only way to get at the information
about k (i.e., that it occurs in the array) is to use the elim
rule on it. However, doing so will cause the desired information
to be hidden (see the set elim rule), and it will not become
unhidden until the proof has proceeded far enough so that the required
function has been completely determined. Thus, the information can be
used only to prove that the constructed function meets the
specification, not to accomplish the construction itself.
The set type should be regarded
primarily as an information--hiding
construct. It cannot be used as a general device for
collecting together all objects (from some type) with a certain property,
as it would in conventional mathematics.
One of the reasons has just been discussed:
if the set type is used to represent a subtype of a given type then
being given a member of the subtype does not involve being given a proof
of its membership; that is, the proof that the member is a member
will be hidden, and in the Nuprl
theory this means that information
is irretrievably lost. Another reason is that for x a member of a type A
the property of being a member of {x:A|B} cannot be
expressed unless it is always true. This is because the type t
in T is really a short form for t=t in T; it
expresses an equality judgement and is well--formed only if t is a
member of T. The problem remains of how to form the type which
represents the power set of a given type. Bishop [Bishop 67] defines
a subset of a given set S to be a set A together with an injection
i from A into S. If one takes this definition and does the
obvious translation into Nuprl
then it turns out that the collection
of such subsets (within some fixed universe Ui) of a given type T
is equivalent to the function type
T->Ui. This latter formulation, where we identify a subset with
the predicate which ``identifies'' the members of the subset, is much
simpler to deal with than Bishop's version. For example, the
proposition that x (for x in T) is in a subset P is expressed
just by P(x); the union of two subsets P and 
is just
x.P(x)|
(x).
Notice that being given the fact that x
is in a subset includes being given the proof that it is. Of
course, one can still use the set type in this context to hide
information when desired.