Compiling nested inductive types

Dealing with multiple nested applications of the same inductive type

Consider the following inductive type declaration:

inductive foo (A : Type) : nat → Type :=
| mk : Π (n : nat), prod (foo A 0) (foo A 1) → prod (foo A n) (foo A (n+1)) → foo A (n+2)

There are two separate occurrences of inductive type applications with foo inside:

prod (foo A 0) (foo A 1)
prod (foo A <n>) (foo A (<n> + 1))

There are at least two different options for how to encode this into a mutually inductive type.

Option 1: Abstract all indices

Since foo occurs twice in the first inductive type application, we can create a copy of prod that takes two indices (one for each foo occurrence), and which otherwise mimics prod:

foo_prod : ℕ → ℕ → Type
foo_prod.mk : Π (n₁ n₂ : ℕ), foo A n₁ → foo A n₂ → foo_prod n₁ n₂

We can then search for other occurrences in the declaration of foo that match the pattern prod (foo A ?M1) (foo A ?M2). The second occurrence matches this and so can be captured by foo_prod as well. The resulting mutually inductive type is as follows:

inductive foo (A : Type) : nat → Type :=
| mk : Π {n : nat}, fprod A 0 1 → fprod A n (n+1) → foo A (n+2)
with fprod : nat → nat → Type :=
| mk : Π {n₁ n₂}, foo A n₁ → foo A n₂ → fprod A n₁ n₂

definition real_foo.mk (A : Type)
                       (n : nat)
                       (p₁ : prod (foo A 0) (foo A 1))
                       (p₂ : prod (foo A n) (foo A (n+1)))
                         : foo A (n+2) :=
match p₁, p₂ with
| prod.mk f₁ f₂, prod.mk f₃ f₄ :=  foo.mk (fprod.mk f₁ f₂) (fprod.mk f₃ f₄)
end

Option 2: Only abstract non-parameter locals

The other option is to only generalize as much as is necessary to process each nested application in sequence. For prod (foo A 0) (foo A 1), we do not need our new inductive type to have any indices. However, since it does not syntactically match prod (foo A <n>) (foo A (<n> + 1)) (up to locals-renaming), we need to create a second copy of prod as well, and this second copy must take <n> as an index. Here is the result:

inductive foo (A : Type) : nat → Type :=
| mk : Π {n : nat}, fprod₁ A → fprod₂ A n → foo A (n+2)
with fprod₁ : Type :=
| mk : foo A 0 → foo A 1 → fprod₁ A
with fprod₂ : nat → Type :=
| mk : Π {n : nat}, foo A n → foo A (n+1) → fprod₂ A n

definition real_foo.mk (A : Type)
                       (n : nat)
                       (p₁ : prod (foo A 0) (foo A 1))
                       (p₂ : prod (foo A n) (foo A (n+1)))
                         : foo A (n+2) :=
match p₁, p₂ with
| prod.mk f₁ f₂, prod.mk f₃ f₄ := foo.mk (fprod₁.mk f₁ f₂) (fprod₂.mk f₃ f₄)
end

Trade-offs

I don't think it matters much, and the second one is probably easier to implement. However, the first one may be preferable if we expect many nested applications that will unify semantically but not syntactically.

Conclusion

I will implement option #2.

Dealing with indices

Example 1: foo occurs inside a parameter argument to another inductive type.

Consider the following inductive declaration:

inductive foo (A : Type) : ℕ → Type :=
| mk : Π (n : nat), vector (foo A n) (n+1) → foo A (n+2)

The inductive type vector already has one index, and abstracting the local <n> adds an additional index. The fact that <n> appears in the position of vector's index is irrelevant, and the two indices of the copied vector type are "uncoupled":

inductive foo : ℕ → Type :=
| mk : Π (n : ℕ), fvector n (n+1) → foo (n+2)
with fvector : nat → nat → Type :=
| vnil  : Π (n₁ : ℕ), fvector n₁ 0
| vcons : Π (n₁ : ℕ) (n₂ : ℕ), foo n₁ → fvector n₁ n₂ → fvector n₁ (n₂+1)

definition fvector_to_vector : Π (n₁ n₂ : ℕ), fvector n₁ n₂ → vector (foo n₁) n₂
| n₁    0     (fvector.vnil n₁)         := @vector.vnil (foo n₁)
| n₁    (k+1) (fvector.vcons n₁ k f v)  := @vector.vcons (foo n₁) f k (fvector_to_vector n₁ k v)

Example 2: foo occurs inside an index argument to another inductive type

Consider the following inductive declarations:

inductive bar : Type → Type :=
| mk : bar ℕ

inductive foo (A : Type.{1}) : A → Type.{1} :=
| mk : Π (a : A), bar (foo A a) → foo A a

Note that (foo A a) is an index argument to bar. I do not see any reasonable way to handle this case. Suppose we try the following:

inductive foo (A : Type.{1}) : A → Type.{1} :=
| mk : Π (a : A), foo_bar A a → foo A a
with foo_bar : A → Type.{1} :=
| mk : Π (a : A), foo_bar A ℕ -- does not type-check

This does not type-check, because we no longer have the arbitrary Type index. On the other hand, if we keep both indices, we have nothing reasonable to pass for the second index:

inductive foo (A : Type.{1}) : A → Type.{1} :=
| mk : Π (a : A), foo_bar A a _ → foo A a       -- We have nothing reasonable to put for the _
with foo_bar : A → Type.{1} -> Type.{1} :=
| mk : Π (a : A), foo_bar A a ℕ

Conclusion

When foo appears inside a parameter argument, we add new indices for every local that appears in the parameter arguments, and keep the old indices completely unconstrained. When foo appears inside an index argument, it is an error.