What in general is a recursor?

Question

I've been reading the Homotopy Type Theory Book, and in the first section is lists out all the kinds of types (function, pair, dependent function ...).

Each time that it mentions a new type, it presents a function called the "recursor." For example, the recursor for the unit type is:

$rec_1 : \Pi_{C:U} C \to 1 \to C $ where $rec_1(C,c,*) : \equiv c$

But what is a recursor in general? The book gives a function that has something to do with each type it introduces and calls it the recursor, but what makes it different from any function that can be defined?

Answer 1

It actually doesn't give a recursor for every type it introduces, and particularly not for two of the types you mention. In particular, functions and dependent functions. Another exception is the universes. However, it does for every other type. This is because all the other types are special cases of inductive types (or, later on, higher inductive types).

Quoting the first sentence of section 5.6:

So far, we have been discussing only particular inductive types: $\mathbf 0$, $\mathbf 1$, $\mathbf 2$, $\mathbb N$, coproducts, products, Σ-types, $\mathsf W$-types, etc.

The "et cetera" does not include dependent functions or universes. This section in particular and that chapter in general go into more detail of what a "recursor" is. The short answer is that a recursor, or rather the more general dependent eliminator, is what shows that an inductive type is defined "uniquely" in terms of its constructors.

For the traditional example of an inductive type, the natural numbers, it is not enough to merely state that there is a natural number of called $0$, and for every natural number $n$, another natural number called $\mathsf{succ}(n)$. We need something that states "and nothing else is a natural number". This is what the dependent eliminator does. For $\mathbb N$, the dependent eliminator corresponds to the traditional (second-order) induction principle. The dependent eliminator in this case, i.e. the traditional induction principle, states that if a "predicate" holds for $0$ and for each $n:\mathbb N$ the same "predicate" holds for $\mathsf{succ}(n)$ whenever it holds for $n$, then the "predicate" holds for all $n:\mathbb N$. In other words, we only need to consider these two cases to cover all cases.

With non-trivial inductive families there are some subtleties to this, most notably in the identity type case. These subtleties are arguably the launching point for the whole program of homotopy type theory.

Answer 2

Ok I've figured it out. In type theory, we need a way for functions to discriminate between different values of the type they are inputting.

So for example, suppose we have $f : \mathbb{N} \to \mathbb{N}$ and we want to define what the function does. We could define $f(n) = 6$ for all $n$, but if we want anything other than a constant function then we need some way of discriminating between the different possible inputs.

The recursors and inductors in the HoTT book provide this way of discriminating between values of a type: that is, we use them to define functions. In programming languages that implement type theory, like agda, one uses pattern matching in the place of recursors and inductors to define functions.

Basically, if anyone reading this wants to understand a recursor or inductor, think of it as describing how pattern matching works on a given type.

So for example, in agda/haskell/any language with pattern matching, I would define a function on $\mathbb{N}$ by specifying $f(0)$ and $f(S(n))$ (S means successor). If you look at the recursor for $\mathbb{N}$, you will see that it too requires a value for $f(0)$ and an expression for $f(S(n))$

Finally, the recursors are for defining regular functions, and the inductors for dependantly typed functions.