Inductive types are very general, which is excellent for their usefulness and applicability, but makes them difficult to study as a whole. Fortunately, they can all be formally reduced to a few special cases. It is beyond the scope of this book to discuss this reduction — which is anyway irrelevant to the mathematician using type theory in practice — but we will take a little time to discuss the one of the basic special cases that we have not yet met. These are Martin-Löf’s -types, also known as the types of well-founded trees. -types are a generalization of such types as natural numbers, lists, and binary trees, which are sufficiently general to encapsulate the “recursion” aspect of any inductive type.
A particular -type is specified by giving two parameters and , in which case the resulting -type is written . The type represents the type of labels for , which function as constructors (however, we reserve that word for the actual functions which arise in inductive definitions). For instance, when defining natural numbers as a -type, the type would be the type inhabited by the two elements and , since there are precisely two ways to obtain a natural number — either it will be zero or a successor of another natural number.
The type family is used to record the arity of labels: a label will take a family of inductive arguments, indexed over . We can therefore think of the “-many” arguments of . These arguments are represented by a function , with the understanding that for any , is the “-th” argument to the label . The -type can thus be thought of as the type of well-founded trees, where nodes are labeled by elements of and each node labeled by has -many branches.
In the case of natural numbers, the label has arity 0, since it constructs the constant zero; the label has arity 1, since it constructs the successor of its argument. We can capture this by using simple elimination on to define a function into a universe of types; this function returns the empty type for and the unit type for . We can thus define
where the superscript serves to distinguish this version of natural numbers from the previously used one. Similarly, we can define the type of lists over as a -type with many labels: one nullary label for the empty list, plus one unary label for each , corresponding to appending to the head of a list:
In general, the -type specified by and is the inductive type generated by the following constructor:
The constructor (short for supremum) takes a label and a function representing the arguments to , and constructs a new element of . Using our previous encoding of natural numbers as -types, we can for instance define
Put differently, we use the label to construct . Then, evaluates to , as it should since is a nullary label. Thus, we need to construct a function , which represents the (zero) arguments supplied to . This is of course trivial, using simple elimination on as shown. Similarly, we can define
and so on.
We have the following induction principle for -types:
When proving a statement about all elements of the -type , it suffices to prove it for , assuming it holds for all with . In other words, it suffices to give a proof
How would we define the function on natural numbers encoded as a -type? We would like to use the recursion principle of with a codomain of itself. We thus need to construct a suitable function
which will represent the recurrence for the function; for simplicity we denote the type family by .
Clearly, will be a function taking as its first argument. The next step is to perform case analysis on and proceed based on whether it is or . This suggests the following form
If is , the type becomes . Thus, given and , we want to construct an element of . Since the label represents , it needs zero inductive arguments and the variables and are irrelevant. We return as a result:
Analogously, if is , the type becomes . Since the label represents the successor operator, it needs one inductive argument — the predecessor — which is represented by the variable . The value of the recursive call on the predecessor is represented by the variable . Thus, taking this value (namely ) and applying the successor operator twice thus yields the desired result:
Putting this together, we thus have
with as defined above.
The associated computation rule for the function is as follows.
For any and we have
In other words, the function satisfies the recurrence .
By the above computation rule, the function behaves as expected:
and so on.
Just as for natural numbers, we can prove a uniqueness theorem for -types:
Let be two functions which satisfy the recurrence
i.e., such that
Then and are equal.