nested data types

Stream: general

[Hans-Dieter Hiep]

Hi! I am trying to define a nested data type, but encounter some confusing error messages. I have reduced the problem to the following small case:

inductive tree (α : Type) (current : {x : α // true})
| ite: α → list tree → list tree → tree

It gives the error: nested occurrence 'list.{0} (tree α current)' contains variables that are not parameters.
Removing the parameter current gets rid of the error.
Can someone explain what is going on?
How can I still make use of such a parameter?

[Mario Carneiro]

what is it doing there? You aren't using it

[Hans-Dieter Hiep]

True, but in the definition with the same error, I do use it.

[Hans-Dieter Hiep]

inductive stmt (α : Type) (H : signature α)
    (self : class_name α) (e : tenv self) : Type 1
| ite: pexp e (boolean α) → list stmt → list stmt → stmt
| while: pexp e (boolean α) → list stmt → stmt
| assign {ty : type α} (l : svar e ty):
    pexp e ty → stmt
| async {c : class_name α} {m : method_name c}
    {H : m ≠ constructor c}
    (o : rvar e (ref c))
    (τ : arglist e m): stmt
| alloc {c : class_name α}
    (l : svar e (ref c))
    (τ : arglist e (constructor c)): stmt

[Mario Carneiro]

Also this is a nested inductive, those aren't handled well

[Mario Carneiro]

If you can avoid list stmt it will be better

[Mario Carneiro]

for example adding a seq constructor

[Mario Carneiro]

and nop I guess

[Hans-Dieter Hiep]

Yes, that was my previous approach. However, I was trying to find out whether working with nested lists of stmt would work too.

[Mario Carneiro]

Why the type 1?

[Hans-Dieter Hiep]

That's because ty : type \alpha consists of all inhabited Types with decidable equality.

[Mario Carneiro]

I think this is just an issue with nested inductive compilation. It's pretty buggy, we're working on a replacement

[Mario Carneiro]

You can also do the nested inductives yourself if you really want it like this

[Hans-Dieter Hiep]

OK, that seems reasonable. Thanks, @Mario Carneiro !

[Mario Carneiro]

This is what it looks like as a plain inductive:

inductive stmt (α : Type) (H : signature α)
    (self : class_name α) (e : tenv self) : bool → Type 1
| ite: pexp e (boolean α) → stmt tt → stmt tt → (stmt ff)
| while: pexp e (boolean α) → stmt tt → (stmt ff)
| assign {ty : type α} (l : svar e ty):
    pexp e ty → (stmt ff)
| async {c : class_name α} {m : method_name c}
    {H : m ≠ constructor c}
    (o : rvar e (ref c))
    (τ : arglist e m): (stmt ff)
| alloc {c : class_name α}
    (l : svar e (ref c))
    (τ : arglist e (constructor c)): (stmt ff)
| nil : stmt tt
| cons : stmt ff → stmt tt → stmt tt

[Mario Carneiro]

the actual stmt is stmt ff here, and stmt tt is isomorphic to list (stmt ff)

[Hans-Dieter Hiep]

Wow, that seems to be what I was looking for! So, if I understand correctly, the bool argument determines what constructors are applicable.

[Mario Carneiro]

right. This is actually what the nested inductive type you wrote (is supposed to) compile to

[Edward Ayers]

Mutual inductives also compile down to something like this right?

[Mario Carneiro]

yes, technically it's two-step, the nested inductive translates to a mutual inductive of stmt and list_stmt, and that gets compiled to an indexed inductive like the above

[Edward Ayers]

So if I may highjack the converstation; am I right in remembering there were talks to put mutual inductives in the kernel? Why bother if you can get them to compile down?

[Mario Carneiro]

because they are slow

[Mario Carneiro]

the kernel "sees" the entire compilation process when trying to reduce the computation rule

[Mario Carneiro]

Also they are slow to compile the initial definitions; if you watch how long it takes to compile a nested inductive vs a plain inductive it's way slower

[Mario Carneiro]

And mutual defs have to be done by well founded recursion, which is hit or miss

[Hans-Dieter Hiep]

You can also do the nested inductives yourself if you really want it like this

Similarly, I can solve the mutual inductive definition by doing it myself:

inductive pexp (e : tenv self) : list (type α) → Type 1
| const (c : constant_name α): pexp [result_type c]
| app (f : function_name α):
    pexp (args_type f) → pexp [result_type f]
| lookup {ty : type α}: rvar e ty → pexp [ty]
| requal {c : class_name α}:
    pexp [type.ref c] → pexp [type.ref c] → pexp [boolean α]
| nil: pexp []
| cons {ty : type α} {l : list (type α)}:
    pexp [ty] → pexp l → pexp (ty::l)

Is accepted without error.