Comparing indexed induction to recursion

Question

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?

Answer 1

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".

Adam's book may also help answer this question: http://adam.chlipala.net/cpdt/html/DataStruct.html

Answer 2

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.