Also see Set Type and Quotient Types for supplementary material.

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: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

`<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

||<T:type>|| == {0 in int|<T>}.This squashes a type in the sense that given a 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,

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

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 intThis 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

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 intIn a proof of this assertion, if one has done

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

Also see Set Type and Quotient Types for supplementary material.

Thu Sep 14 08:45:18 EDT 1995