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.