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:
;
;
;
; or
,
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.
