Zulip Chat Archive

Stream: general

Topic: nested data types


view this post on Zulip Hans-Dieter Hiep (Feb 14 2019 at 10:41):

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?

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:42):

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

view this post on Zulip Hans-Dieter Hiep (Feb 14 2019 at 10:42):

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

view this post on Zulip Hans-Dieter Hiep (Feb 14 2019 at 10:42):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:43):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:43):

If you can avoid list stmt it will be better

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:43):

for example adding a seq constructor

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:43):

and nop I guess

view this post on Zulip Hans-Dieter Hiep (Feb 14 2019 at 10:44):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:45):

Why the type 1?

view this post on Zulip Hans-Dieter Hiep (Feb 14 2019 at 10:45):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:47):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:47):

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

view this post on Zulip Hans-Dieter Hiep (Feb 14 2019 at 10:48):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:48):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:49):

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

view this post on Zulip Hans-Dieter Hiep (Feb 14 2019 at 10:52):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 11:04):

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

view this post on Zulip Edward Ayers (Feb 14 2019 at 11:07):

Mutual inductives also compile down to something like this right?

view this post on Zulip Mario Carneiro (Feb 14 2019 at 11:08):

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

view this post on Zulip Edward Ayers (Feb 14 2019 at 11:09):

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?

view this post on Zulip Mario Carneiro (Feb 14 2019 at 11:09):

because they are slow

view this post on Zulip Mario Carneiro (Feb 14 2019 at 11:10):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 11:11):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 11:12):

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

view this post on Zulip Hans-Dieter Hiep (Feb 19 2019 at 12:23):

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.


Last updated: May 15 2021 at 00:39 UTC