The basic components of the type theory employed by the Nuprl
system are
the atomic types int, atom
and void. In addition
to the atomic types, there is an integer--indexed family of predefined types
called universes ,
. Universes are
types whose canonical elements are types. All the atomic types are members
of 
, and 
is a member of 
.
More complex
types are built from the atomic types and the universes
by using type constructors,
operators which take
types and build new types from them. The type constructors used in Nuprl
are
The meaning of these type constructors has been briefly discussed in chapter
2 and will be discussed in detail in chapter 8. The first three type
constructors are binary, and all have equal precedence .
They all associate
to the right. We can also form types by using the forms `` element in
type'' and `` element = element in type''.
As explained in chapter 2, these are two of the basic judgement
forms. The symbols in and = can be viewed as a type constructor
for the purposes of the present discussion. Viewed in this way, in
associates to the left. The symbol = binds more tightly than the
symbol in. The type constructors in the list above also bind more
tightly than does in. The binding and scope conventions are described
in chapter 2.