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

Thu Sep 14 08:45:18 EDT 1995