A type
is a collection of objects having similar
structure. For instance, integers,
pairs of integers and functions over integers are
at least three distinct types. In both mathematics
and programming the collection of functions is further subdivided
based on the kind of input for which the function makes sense, and these
divisons are also called types, following the vocabulary of the very
first type theories [Whitehead & Russell 25].
For example, we say that the integer successor function
is a function from integers to
integers,
that inversion is a function from invertible functions to functions
(as in ``subtraction is the inverse of addition''), and that the operation
of functional composition is a function from two functions to their composition.
One modern notation for the type of functions from type A into type B
is 
(read as A ``arrow'' B).
Thus integer successor has type 
,
and the curried form of the composition of integer
functions has type 
.
For our first look at types we will consider only those built from
type variables 
using arrow.
Hence we will have 
, etc.,
as types,
but not 
.
This will allow us to examine the general properties of functions without
being concerned with the details of concrete types such as integers.
One of the necessary steps in defining a type is choosing a notation for
its elements.
In the case of the integers, for instance, we use notations such as
.
These are the defining notations, or canonical forms, of the type.
Other notations, such as 1+1, 
and 2-1, are not
defining notations but are derived notations or noncanonical forms.
Informally, functions are named in a variety of ways.
We sometimes use special symbols like + or 
.
Sometimes in informal mathematics one might abuse the notation and say
that x+1 is the successor function.
Formally, however, we regard x+1 as an ambiguous
value of the successor function and adopt a notation for the function
which distinguishes it from its values.
Betrand Russell [Whitehead & Russell 25] wrote 
for the
successor function, while
Church [Church 51] wrote 
.
Sometimes one sees the notation 
, where 
is used as a ``hole'' for the
argument.
In Nuprl
we adopt the lambda notation, using 
as a printable
approximation to 
.
This notation is not suitable for all of our needs, but it is an adequate
and familiar place to start.