Nuprl Basics - Subtyping and Polymorphism

Definitions NuprlPrimitives Sections NuprlLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Subtyping and Polymorphism

As explained in Equality, a single notation can be used to denote values in multiple types, and a pair of notations can be used to denote distinct values of one type and yet denote a single value in another type.
(One consequence is that one cannot always simply "read off" an intended type from an expression.)

Subtyping: Void A; {x:A| P(x) } A; A (x,y:A//E(x,y)); (x:A. B(x)) B(a); A Top

Recall that Functions are denoted by Computationally significant expressions that operate on notations for the arguments. It often happens that functional notations working on notations of one type "T" will also "automatically" work on all notations of some other type "S". Or equivalently, the notations of type "S" are also notations of type "T". Then we may say

Def S T == x:S. x T,

and consequently, when S T, then (TA) (SA), i.e. f:(TA). f SA.
See also Subtype Relation for an alternative to this definition.
One obvious way for S T to happen is simply for S to be a subclass of T, e.g.

  , or more generally,
{x:A| P(x) }  A (see Comprehension Subtypes), and as an extreme case,
Void  A.

But there is also a subtler aspect of subtyping. Recall from Functions that the core criterion for being a notation for a function over a domain type D is that its application to any notations of D denoting the same input value must yield notations for the same output value. Thus,

Thm* f:(( mod 2)A). f A

since the notations of " mod k" are just those of with certain distinct integer notations becoming identified, namely those x and y such that m:. x-y = mk. Thus,

( mod k), or more generally,
T (x,y:T//E(x,y)) (see Quotient Types)

Another type constructor intimately related to expressing polymorphism is Intersection, x:A. B(x). Here we give six other facts about functions that are polymorphic over all input types. The first says that a function expression completely polymorphic in the domain type may be used as both function and argument in a single application. The second says that if the output type does not depend on the input type, then the function is constant. The third says that identity is the only polymorphic function mapping the domain into itself. The fourth and fifth together say that a function generating a (D List) from a D value, ignoring the choice of D, must generate a list whose length is independent of the input, and all of whose members simply are the input value. The sixth says that the swap function is the only polymorphic CDDC function.

Thm* T:Type, f:(D:Type. DT). f(f)  T
Thm* f:(D:Type. DT), A:Type, a:A, B:Type, b:B. f(a) = f(b)  T
Thm* f:(D:Type. DD), A:Type, a:A. f(a) = a
Thm* f:(D:Type. D(D List)), A:Type, a:A, B:Type, b:B.
Thm* ||f(a)|| = ||f(b)||
Thm* f:(D:Type. D(D List)), A:Type, a,x:A. x list f(a)  x = a
Thm* f:(C,D:Type. CDDC), A,B:Type, a:A, b:B. f(<a,b>) = <b,a>  BA

See Typing Y for another example.

The type Top

Finally, there is a unit type "Top" whose sole member is denoted by every closed expression. It is called "Top" because Thm* A Top.

NOTE that "Top" is not a type of all values, even though every (closed) expression has type "Top" (thus "whatever Top"); it is just that the semantics is so trivial as to exclude no possible notation (the other extreme of triviality is Void, whose semantics trivially excludes every notation). In particular even though (Top Top) is true, this does not mean that the type Top is a member of Top, since equality in Top has nothing to do with equality between types.