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.