Zulip Chat Archive

Stream: new members

Topic: Nested datatypes and vector

view this post on Zulip Borja Sierra (Jan 21 2020 at 17:55):

Hello, I was trying to define a datatype of propositional formulas over an arbitrary language in the following way:

 structure prop_lang :=
mk :: (Symb : Type) (Arity : Symb  )

inductive Form (Var : Type) ( : prop_lang)
| V {} : Var  Form
| Conn {} : Π (c : .Symb) , vector Form (.Arity c)  Form

but using the standard vector datatype (lists with fixed length) it gives me the following error:

nested inductive type compiled to invalid inductive type
nested exception message:
nested occurrence 'subtype.{1} (_nest_1_1.list.Form Var ℒ) (fun (l : _nest_1_1.list.Form Var ℒ), (eq.{1} nat (list.length.{0} (_nest_1_1.Form Var ℒ) l) (prop_lang.Arity ℒ c)))' contains variables that are not parameters

while if I define it with:

inductive myvector (α : Type) : nat  Type
| nil {} : myvector 0
| cons   : Π {n}, α  myvector n  myvector (n +1)

everything goes okay. I imagine this is because vector isn't really a datatype but it is a set over the list datatype while myvector is a proper datatype. After this I have some questions:
1) The error is really due to what I am supposing to?
2) It is a good idea to work with myvector datatype? I know it is quite standard in other languages (like Agda) but it seems that in lean it is not so used.
3) It is possible to define Form with vector (set of lists of fixed length) as a datatype (not as a set of well-formed formula over
a datatype where ill-formed formulas can be build).
Thanks to everyone!

view this post on Zulip Mario Carneiro (Jan 21 2020 at 22:00):

My recommendation is to avoid nested inductive types in lean 3 (and maybe lean 4, we'll see). You should just code it as a regular inductive type. One way to do this, similar to what is done in the flypitch project:

structure prop_lang :=
mk :: (Symb : Type) (Arity : Symb  )

inductive PreForm (Var : Type) ( : prop_lang) :   Type
| V {} : Var  PreForm 0
| Symb (c : .Symb) : PreForm (.Arity c)
| App {n} : PreForm (n + 1)  PreForm 0  PreForm n

def Form (Var : Type) ( : prop_lang) := PreForm Var  0

view this post on Zulip Mario Carneiro (Jan 21 2020 at 22:03):

That is, you say "everything goes okay with myvector" but actually you will have issues when you want to e.g. define functions out of the nested inductive

Last updated: May 13 2021 at 06:15 UTC