Next: Cartesian Product Up: Extending the Typed Previous: Extending the Typed

## Dependent Function Space

It  is very useful to be able to describe functions whose range type depends on the input. For example, we can imagine a function on integers of the form . The type of this function on input x is . Call this type expression ; then the function type we want is written and denotes those functions f whose value on input n belongs to ().

In the general case of pure functions we can introduce such types by allowing declarations of parameterized types or, equivalently, type--valued functions.  These are declared as . To introduce these properly we must think of itself as a type, but a large type. We do not want to say to express that is a type because this leads to paradox in the full theory. It is in the spirit of type theory to introduce another layer of object, or in our terminology, another ``universe'', called . In addition to the types in , contains so--called large types,    namely and types built from it such as , , and so forth. To say that is a large type we write . The new formal system allows the same class of object expressions but a wider class of types. Now a variable is a type expression, the constant is a type expression, if T is a type expression (possibly containing a free occurrence of the variable x of type S) then is a type expression, and if F is an object expression of type then is a type expression. The old form of function space results when T does not depend on x; in this case we still write .

Figure: Rules for Dependent Functions

The new rules are listed in figure . With these rules we can prove the following goals.

With the new degree of expressiveness permitted by the dependent arrow we are able to dispense with the hypothesis list in the initial goal in the above examples. We now say that an initial goal has the form
[0] , where t is an object expression and T is a type expression. One might expect that it would be more convenient to allow a hypothesis list such as , but such a list would have to be checked to guarantee well--formedness of the types. Such checks become elaborate with types of the form , and the hypothesis--checking methods would become as complex as the proof system itself. As the theory is enlarged it will become impossible to provide an algorithm which will guarantee the well--formedness of hypotheses. Using the proof system to show well--formedness will guarantee that the hypothesis list is well--formed.

Hidden in the explanation above is a subtle point which affects the basic design of Nuprl . The definition of a type expression involves the clause ``F is an expression of type .'' Thus, in order to know that is an allowable initial goal, we may have to determine that a subterm of T is of a certain type; in the example above, we must show that B is of type . To define this concept precisely we would need some precise definition of the relation that B is of type . This could be given by a type--checking algorithm or by an inductive definition, but in either case the definition would be as complex as the proof system that it is used to define.

Another approach to this situation is to take a simpler definition of an initial goal and let the proof system take care of ensuring that only type expressions can appear on the right--hand side of a typing. To this end, we define the syntactically simple concept of a readable expression   and then state that an initial goal has the form , where and are these simple expressions. Using this approach, an expression is either:

a variable:
;
a constant:
;
an application:
;
an abstraction:
; or
an arrow:
,

where a,b and f are expressions. This allows expressions such as or , which do not make sense in this theory. However, the proof rules are organized so that if the initial goal is proved then T will be a type expression and t will be an object expression of type T.

Next: Cartesian Product Up: Extending the Typed Previous: Extending the Typed

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995