5.7 Generalizations of inductive types

The notion of inductive type has been studied in type theoryPlanetmathPlanetmath for many years, and admits of many, many generalizationsPlanetmathPlanetmath: inductive type families, mutual inductive types, inductive-inductive types, inductive-recursive types, etc. In this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath we give an overview of some of these, a few of which will be used later in the book. (In http://planetmath.org/node/87579Chapter 6 we will study in more depth a very different generalization of inductive types, which is particular to homotopy type theory.)

Most of these generalizations involve allowing ourselves to define more than one type by inductionMathworldPlanetmath at the same time. One very simple example of this, which we have already seen, is the coproductMathworldPlanetmath A+B. It would be tedious indeed if we had to write down separate inductive definitions for β„•+β„•, for β„•+𝟐, for 𝟐+𝟐, and so on every time we wanted to consider the coproduct of two types. Instead, we make one definition in which A and B are variables standing for types; in type theory they are called parameters. Thus technically speaking, what results from the definition is not a single type, but a family of types +:𝒰→𝒰→𝒰, taking two types as input and producing their coproduct. Similarly, the type π–«π—‚π—Œπ—β’(A) of lists is a family π–«π—‚π—Œπ—β’(Β―):𝒰→𝒰 in which the type A is a parameter.

In mathematics, this sort of thing is so obvious as to not be worth mentioning, but we bring it up in order to contrast it with the next example. Note that each type A+B is independently defined inductively, as is each type π–«π—‚π—Œπ—β’(A). By contrast, we might also consider defining a whole type family B:A→𝒰 by induction together. The differencePlanetmathPlanetmath is that now the constructors may change the index a:A, and as a consequence we cannot say that the individual types B⁒(a) are inductively defined, only that the entire family is inductively defined.

The standard example is the type of lists of specified length, traditionally called vectors. We fix a parameter type A, and define a type family 𝖡𝖾𝖼n⁒(A), for n:β„•, generated by the following constructors:

  • β€’

    a vector 𝗇𝗂𝗅:𝖡𝖾𝖼0⁒(A) of length zero,

  • β€’

    a function π–Όπ—ˆπ—‡π—Œ:∏(n:β„•)A→𝖡𝖾𝖼n⁒(A)β†’π–΅π–Ύπ–Όπ—Œπ—Žπ–Όπ–Όβ’(n)⁒(A).

In contrast to lists, vectors (with elements from a fixed type A) form a family of types indexed by their length. While A is a parameter, we say that n:β„• is an index of the inductive family. An individual type such as 𝖡𝖾𝖼3⁒(A) is not inductively defined: the constructors which build elements of 𝖡𝖾𝖼3⁒(A) take input from a different type in the family, such as π–Όπ—ˆπ—‡π—Œ:A→𝖡𝖾𝖼2⁒(A)→𝖡𝖾𝖼3⁒(A).

In particular, the induction principle must refer to the entire type family as well; thus the hypotheses and the conclusionMathworldPlanetmath must quantify over the indices appropriately. In the case of vectors, the induction principle states that given a type family C:∏(n:β„•)𝖡𝖾𝖼n⁒(A)→𝒰, together with

  • β€’

    an element c𝗇𝗂𝗅:C⁒(0,𝗇𝗂𝗅), and

  • β€’

    a function cπ–Όπ—ˆπ—‡π—Œ:∏(n:β„•)∏(a:A)∏(β„“:𝖡𝖾𝖼n(A))C⁒(n,β„“)β†’C⁒(π—Œπ—Žπ–Όπ–Όβ’(n),π–Όπ—ˆπ—‡π—Œβ’(a,β„“))

there exists a function f:∏(n:β„•)∏(β„“:𝖡𝖾𝖼n(A))C⁒(n,β„“) such that

f⁒(0,𝗇𝗂𝗅) ≑c𝗇𝗂𝗅
f⁒(π—Œπ—Žπ–Όπ–Όβ’(n),π–Όπ—ˆπ—‡π—Œβ’(a,β„“)) ≑cπ–Όπ—ˆπ—‡π—Œβ’(n,a,β„“,f⁒(β„“)).

One use of inductive families is to define predicatesMathworldPlanetmathPlanetmath inductively. For instance, we might define the predicate π—‚π—Œπ–Ύπ—π–Ύπ—‡:ℕ→𝒰 as an inductive family indexed by β„•, with the following constructors:

  • β€’

    an element 𝖾𝗏𝖾𝗇0:π—‚π—Œπ–Ύπ—π–Ύπ—‡β’(0),

  • β€’

    a function 𝖾𝗏𝖾𝗇s⁒s:∏(n:β„•)π—‚π—Œπ–Ύπ—π–Ύπ—‡β’(n)β†’π—‚π—Œπ–Ύπ—π–Ύπ—‡β’(π—Œπ—Žπ–Όπ–Όβ’(π—Œπ—Žπ–Όπ–Όβ’(n))).

In other words, we stipulate that 0 is even, and that if n is even then so is π—Œπ—Žπ–Όπ–Όβ’(π—Œπ—Žπ–Όπ–Όβ’(n)). These constructors β€œobviously” give no way to construct an element of, say, π—‚π—Œπ–Ύπ—π–Ύπ—‡β’(1), and since π—‚π—Œπ–Ύπ—π–Ύπ—‡ is supposed to be freely generated by these constructors, there must be no such element. (Actually proving that Β¬β’π—‚π—Œπ–Ύπ—π–Ύπ—‡β’(1) is not entirely trivial, however). The induction principle for π—‚π—Œπ–Ύπ—π–Ύπ—‡ says that to prove something about all even natural numbersMathworldPlanetmath, it suffices to prove it for 0 and verify that it is preserved by adding two.

Inductively defined predicates are much used in computer formalization of mathematics and software verification. But we will not have much use for them, with a couple of exceptions in Β§10.3 (http://planetmath.org/103ordinalnumbers),Β§11.5 (http://planetmath.org/115compactnessoftheinterval).

Another important special case is when the indexing type of an inductive family is finite. In this case, we can equivalently express the inductive definition as a finite collectionMathworldPlanetmath of types defined by mutual induction. For instance, we might define the types 𝖾𝗏𝖾𝗇 and π—ˆπ–½π–½ of even and odd natural numbers by mutual induction, where 𝖾𝗏𝖾𝗇 is generated by constructors

  • β€’

    0:𝖾𝗏𝖾𝗇 and

  • β€’


while π—ˆπ–½π–½ is generated by the one constructor

  • β€’


Note that 𝖾𝗏𝖾𝗇 and π—ˆπ–½π–½ are simple types (not type families), but their constructors can refer to each other. If we expressed this definition as an inductive type family 𝗉𝖺𝗋𝗂𝗍𝗒𝗇𝖺𝗍:πŸβ†’π’°, with 𝗉𝖺𝗋𝗂𝗍𝗒𝗇𝖺𝗍⁒(0𝟐) and 𝗉𝖺𝗋𝗂𝗍𝗒𝗇𝖺𝗍⁒(1𝟐) representing 𝖾𝗏𝖾𝗇 and π—ˆπ–½π–½ respectively, it would instead have constructors:

  • β€’


  • β€’


  • β€’


When expressed explicitly as a mutual inductive definition, the induction principle for 𝖾𝗏𝖾𝗇 and π—ˆπ–½π–½ says that given C:𝖾𝗏𝖾𝗇→𝒰 and D:π—ˆπ–½π–½β†’π’°, along with

  • β€’


  • β€’


  • β€’


there exist f:∏(n:𝖾𝗏𝖾𝗇)C⁒(n) and g:∏(n:π—ˆπ–½π–½)D⁒(n) such that

f⁒(0) ≑c0
f⁒(π–Ύπ—Œπ—Žπ–Όπ–Όβ’(n)) ≑cs⁒(g⁒(n))
g⁒(π—ˆπ—Œπ—Žπ–Όπ–Όβ’(n)) ≑ds⁒(f⁒(n)).

In particular, just as we can only induct over an inductive family β€œall at once”, we have to induct on 𝖾𝗏𝖾𝗇 and π—ˆπ–½π–½ simultaneously. We will not have much use for mutual inductive definitions in this book either.

A further, more radicalPlanetmathPlanetmath, generalization is to allow definition of a type family B:A→𝒰 in which not only the types B⁒(a), but the type A itself, is defined as part of one big induction. In other words, not only do we specify constructors for the B⁒(a)s which can take inputs from other B⁒(aβ€²)s, as with inductive families, we also at the same time specify constructors for A itself, which can take inputs from the B⁒(a)s. This can be regarded as an inductive family in which the indices are inductively defined simultaneously with the indexed types, or as a mutual inductive definition in which one of the types can depend on the other. More complicated dependency structuresMathworldPlanetmath are also possible. In general, these are called inductive-inductive definitions. For the most part, we will not use them in this book, but their higher variant (see http://planetmath.org/node/87579Chapter 6) will appear in a couple of experimental examples in http://planetmath.org/node/87585Chapter 11.

The last generalization we wish to mention is inductive-recursive definitions, in which a type is defined inductively at the same time as a recursive function on it. That is, we fix a known type P, and give constructors for an inductive type A and at the same time define a function f:A→P using the recursion principle for A resulting from its constructors — with the twist that the constructors of A are allowed to refer also to the values of f. We do not yet know how to justify such definitions from a homotopical perspective, and we will not use any of them in this book.

Title 5.7 Generalizations of inductive types