# Comparing indexed induction to recursion

Many indexed inductive families can be "equivalently" defined by recursion over their indices. For instance, the type family of vectors:

data Vec (A : Set) : ℕ → Set where
nil : Vec A zero
cons : {n : ℕ) → A → Vec A n → Vec A (suc n)


can equivalently be defined recursively to consist of right-associated product types:

Vec : (A : Set) → ℕ → Set
Vec A zero = ⊤
Vec A (suc n) = A × Vec A n


Similarly, the inequality predicates on natural numbers, like:

data _≤_ : ℕ → ℕ → Set where
zero≤ : (n : ℕ) → zero ≤ n
suc≤suc : (m n : ℕ) → (m ≤ n) → (suc m ≤ suc n)


can also be defined recursively on both arguments:

_≤_ : ℕ → ℕ → Set
zero ≤ _ = ⊤
suc m ≤ zero = ⊥
suc m ≤ suc n = m ≤ n


Of course, this is only possible when the types of indices of the indexed inductive family are themselves inductive types, and the indices of each constructor are constructors of the types of indices. (Which, perhaps coincidentally, is also the case in which indexed inductive families work best -- no "green slime".)

In a situation where both definitions are possible, what are the advantages and disadvantages of the two choices? Why should we choose one over the other?

• This this a duplicate of this question? proofassistants.stackexchange.com/questions/2136/… Commented Feb 4 at 5:39
• @JasonRute It's certainly closely related, but a lot of the answers to that question focus on what you can do with inductive families and not with recursive ones, whereas I'm specifically asking about how they differ in the case when you can do both. Commented Feb 4 at 7:04
• Out of curiosity, are the two approaches equivalent, mathematically speaking? (Let's say we limit attention to initial algebras of polynomial functors with parameters.) Commented Feb 4 at 7:38
• @AndrejBauer I don't know of a formal theorem saying that they are, but I would expect so. Commented Feb 5 at 5:27
• Assuming that is the case, the question is "about judgmental equality", it seems. Commented Feb 5 at 7:17

Since I am familiar with Coq, so I talk about some experiences when I did both in Coq.

In most cases, the indexed inductive type would be a greater option. The recursive fashion may require less effort and appear to be intuitive, but it is somehow awkward for proof automation. In Coq, for example, when you get a recursively defined type, say v: Vec A (S n), then applying simpl on v would expand the function, and then you will get a pair type, but this certainly does not help very much, and even worse, it makes your proof context unreadable if you are handling a relatively large proof body; sometimes we just want to hide the thing behind this boilerplate. It also makes pattern-matching (syntactical) problemsome because your recursive type is a "pair" not the "Vec" you are expecting; but inductive types can be happily pattern-matched.

Another bad thing about the recursive style is that it only captures types that have simple structures that are determined solely by the indices. This can be a severe limitation if you are dealing with complex data structures like program syntax which is impossible to define as "recursively right-associated product types".

As you conjecture in the comments, I also think the two presentations are isomorphic in the "nice enough" case, so I would say this is a question of usage. The exact definitional behaviour of the two definitions will probably differ slightly on open terms, but I can't say which one is best. In any case this is probably quite limited, because I think the pseudo-constructor and pseudo-induction principle you get for the recursive type satisfy the definitional β-rules of the inductive variant, or at least this is the case for vectors.

The first point, maybe not so obvious, but often relevant, is that the inductive definition is, I believe, clearer. In particular, if you have a complicated indexed datatype, then presenting it solely as an inductive fixed point might risk people getting suspicious, and/or taking them a bit more energy to understand what you mean. I would say the indexed definition is a better specification. But then maybe it is because I have been bred these since forever and this is just Stockholm syndrome.

The second is that taking one or the other presentation can have subtle meta-theoretic consequence. A good example of this are inductive definitionally irrelevant propositions. In the SProp paper, they give a criterion for when a proposition can be safely eliminated to SProp back to type, which basically amounts to saying it can be expressed as a fixed point (btw, the paper also contains a pretty interesting description of when this is possible, based on Jesper's earlier work on pattern-matching compilation).

The third, and maybe most important, is how you reason with these things. This is basically a trade-off: the inductive definition gives you "for free" an induction principle, but you have to use it to prove inversion principles (eg. for vectors, the fact that any v : Vec A (S n) can only be some cons a v'). In Coq, you have tactics for this, and in Agda fancy pattern-matching does a similar job. For the fixed point definition, things are turned around: you have the inversion for free (because this is basically the definition of the type), but have to prove induction. I suspect in Agda this is subpar, because working with induction principles rather than the primitive equations presentation is a pain, but in Coq this is not so bad.

But at the end of the day, when working heavily with fancy inductive datatypes, I often end up re-defining custom induction or inversion principles to better fit my needs of the moment. So whether the original type was defined as inductive or recursive makes relatively little difference, because I will end up proving the structure that is not given to me primitively, and using both. Although I generally phrase inversion principles in a slightly different way than the full recursive definition, as explained in the other thread.

• In the recursive case, can't you get essentially the same induction principle you would get from the inductive definition by just doing induction on the indices? In particular, in Agda you could just split directly on the indices rather than going to the pain of explicitly calling an induction function. Commented Feb 5 at 19:27
• I think this is true only if your inductive type has the same structure as your indexing type (thinking about ornaments here). But if you have a more complicated relation, this might not be as simple. For instance, if you have a "catch-all" constructor that can be used to construct a value for any index (think conversion rule for inductively defined typing), then you'll have a corresponding case for each index, and you'll end up repeating that case. Commented Feb 6 at 9:41
• I feel like this might be similar to the use of functional induction, ie an induction principle that follows the structure of a recursive functions, which might be more complicated than the one corresponding to the induction principle for the inductive type. Here too you want an induction principle "of the right shape", which is not the same as that of the underlying datastructure. But maybe all this is easier to do with Agda's pattern-matching. Commented Feb 6 at 9:44
• I didn't mean to include an inductive family with a "catch-all" constructor among the "situations where both definitions are possible" that I said in the question I wanted to restrict to. I suppose in that case you could get something like a recursive version by duplicating the catch-all constructor at each index, as you suggest, but it wouldn't be as strongly equivalent since, for instance, you wouldn't be able to apply the catch-all constructor without first destructing the index. Commented Feb 6 at 21:11