Nested inductive datatypes with vectors

Stream: new members

[James Parker]

Hi. I'm attempting to write something along the lines of the following:

inductive Foo (f: Type) where
| Bar: (foos: Vector (Foo f) 3) -> Foo f

This results in the error invalid nested inductive datatype 'Eq', nested inductive datatypes parameters cannot contain local variables.. Can anyone explain why this errors, but switching the Vector to an Array works?

inductive Foo (f: Type) where
| Bar: (foos: Array (Foo f)) -> Foo f

[Robin Arnez]

Well, the answer is that Vector is a subtype and therefore contains a property on the recursion. However, it is not supported when a type within the constructor depends on another one with recursion. Take this variant:

inductive Foo (f : Type) where
  | Bar (foos : Array (Foo f)) (h : foos.size = 3) : Foo f

foos is recursive and it's being referenced in h. This is simply not allowed.
(I'm not 100% sure about the "why", maybe someone else can help with that)

[James Parker]

That's helpful, thanks! I didn't realize Vector was defined that way since its definition is hidden by the docs.

[James Parker]

It would be nice to understand why this isn't allowed. Is it unsound or is the type checker being conservative?

[Robin Arnez]

I guess one thing is that generally allowing this makes you lose the ability to translate between equivalent definitions:

unsafe inductive GenericProperty (α : Type u) (β : α → Type v) (p : ∀ {γ}, (a : α) → (β a → γ) → Prop) where
  | mk (a : α) (f : β a → GenericProperty α β p) (h : p a f)

unsafe inductive GenericPropertyOther (α : Type u) (β : α → Type v) (p : ∀ {γ}, (a : α) → (β a → γ) → Prop) where
  | mk (a : α) (f : β a → GenericPropertyOther α β p) (h : p a f)

unsafe def translate : GenericProperty α β p → GenericPropertyOther α β p
  | .mk a f h =>
    let g := fun x => translate (f x)
    .mk a g sorry -- have h : p a f, need p a g (impossible!)

Takes this other type in contrast:

inductive MyList (α : Type u) where
  | nil
  | cons (a : α) (l : MyList α)

def translate : List α → MyList α
  | .nil => .nil
  | .cons a l => .cons a (translate l)

[Robin Arnez]

I'm not sure whether this is unsound but ... probably..?