Intersecting a Family of Types

x:A. B(x)

x  A

More precisely, u = v  (x:A. B(x)) when u = v  B(x) for all x  A (see Types). Consequently,

Thm* B:(AType), a:A. (x:A. B(x))  B(a)

If A is empty, then (x:A. B(x)) has exactly one member, and every (closed) expression denotes it (Thm* whatever1 = whatever2  (x:Void. Whatever(x))). See Types.

The type (A:Type. (A List)(A List)), for example, is the type of "polymorphic" operations on lists that don't depend on the type of the elements. For example,

(as.rev(as))  (A:Type. (A List)(A List))

where rev(as) is the list reversing function,

Def rev(as) == Case of as; nil  nil ; a.as'  rev(as') @ [a]  (recursive)

For more examples about intersection see Polymorphism.

Guarded Types: T(given A)

In the special case of "x:A. B(x)" where some expression T not actually using x is used in place of B(x), then the intersection, denoted "T(given A)", is a way of "guarding" membership in T by whether A has a member.

If A has a member, then the type T(given A) is T (extensionally). If A is empty, then T(given A) is degenerate, having one member which is denoted by every closed expression (see Types).

So for example, in Nuprl, in order for AB to denote a type, A must also denote a type, but B need only denote a type if A has a member. If A is empty, then B may be any closed term, and AB then denotes simply the one-element function space with empty domain. See Function Types.

This well-formedness condition can be expressed using guarded types thus:

Thm* A:Type, B:Type(given A). AB  Type

The restriction of B to Type(given A) escapes the absolute condition of B simply being in Type.

See Guarded Types for more on guarded types and propositions.

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