Types and Induction

Every mathematician's toolbox contains tuples and subsets for making ideal elements, and proofs by induction. In this chapter we bring together the traditional techniques which form the received view of the foundations of twentieth century mathematics. Afterwards they will be dismantled and reconsidered in the light of later algebraic experience.

At the beginning of his career, Georg Cantor investigated sets of points
of discontinuity which functions could have whilst still admitting Fourier
representations. He also gave a construction of the real numbers from the
rationals, and showed that there are a lot more reals than rationals (Hermann
Weyl later reproached analysts for decomposing the continuum into single
points). Cantor was led to considering *abstract* sets, forming
hierarchies under constructions such as the set of all subsets.

There are historical parallels between mathematics and programming in the development of types. Cantor was concerned with the magnitudes of sets, whereas FORTRAN distinguished between integer and real data types because they have different storage requirements. (Linear logic shows that resource analysis continues to be a fruitful idea.) Both started from the integers and real numbers alone. Bertrand Russell formulated his theory of types as a way of avoiding the vicious circles which he saw as the root of the paradoxes of set theory. On the other hand, the one lesson which the software industry has learned from informatics is that the type discipline catches a very large proportion of errors and thereby makes programs more reliable. Early calculi provided a static universe in advance, but modern type theories and programming languages create new types dynamically from old ones.

What is an abstract set? Some accounts of set theory claim that it is a voluntary
conspiracy of its elements, coming together arbitrarily from independent
sources (the *inductive conception*). But this conflicts with
mathematical practice, and has little backing even in philosophical tradition.
Plato held that members of a class are images of a Form; in practice, we conceive
of the Form and *certain* of its instances first. The totality is only
a semantic afterthought (and the instances are usually not themselves Forms).
Indeed, from Zeno's time, points in geometry *lay on* lines but
did not *constitute* them.

Gottlob Frege defined sets by comprehension of predicates, which at first
he allowed to take *anything* as their subjects. Russell's famous
{*x*|*x* Ï *x*} showed that things couldn't be done quite so
naively , so instead we select the elements *from an already given
ambient set*.

For us, types are not imposed afterwards to constrain the size of the world,
but are a precondition of meaning. In elementary trigonometry sin is
thought of as applying to *angles* only, which are only reduced to
real numbers by choosing a unit of measurement. Physical quantities may
only be added or tested for equality if they measure the same thing (length,
mass, energy, electric charge, *etc* ) in the same units; sometimes
laws of mechanics can be guessed by this dimensional analysis alone, or from
a scale model which preserves the dimensionless part (such as the Reynolds
number in fluid mechanics).

More complex types are formed by processes, such as the powerset, like those generating terms and logical formulae. The establishment of certain standard abstract methods of construction made it possible to state and prove results of a generality that would not have been considered in the nineteenth century. As Michael Barr [BW85, p. 88] put it, ``The idea of constructing a quotient space without having to have the ambient space including it, for example, was made possible by the introduction of set theory, in particular by the advent of the rather dubious idea that a set can be an element of another set. There is probably nothing in the introduction of topos theory as foundations more radical than that.''

On the other hand, the importance of the quotient operation is such that
*it* should perhaps be taken as primitive instead. Modern type
theory builds hierarchies as Cantor and Zermelo did, but using simpler ways
of forming types, such as the product, sum and set of functions. These correspond
very directly to conjunction, disjunction and implication of propositions,
an analogy which will be an important guiding principle for the rest of the
book. We shall find that the structure of the types is characterised, not
by their set-theoretic incarnations, but by certain operations, such as
projection and evaluation maps, which build terms of that type and take them
apart. In particular the l-calculus handles the terms arising
from the function-type.

The second half of the chapter is devoted to induction and recursion. Sections 2.5-2.6 discuss well founded relations, a notion of induction which also comes from the set-theoretic tradition, but we shall motivate it instead from the problem of proving correctness and termination of a wide class of recursive programs. There are classical idioms of induction based on minimal counterexamples and descending sequences, but we shall show how they can often be made intuitionistic. More complicated inductive arguments can be justified by constructing recursion measures using lexicographic products and other methods.

For programming (and foundations), structural recursion over lists, trees and languages is more important. In Section 2.7 we treat lists and Peano induction over the natural numbers in a similar fashion to the function-type. The last section treats second and higher order logic.