Generlized algebric data type

Stream: general

[Alice Laroche]

I wanted to implement a simple GADT to experiment with when i encountered a problem :

inductive expression : Type -> Type
| number : ℕ -> expression ℕ
| boolean : bool -> expression bool
| add : expression ℕ -> expression ℕ -> expression ℕ
| mul : expression ℕ -> expression ℕ -> expression ℕ
| and : expression bool -> expression bool -> expression bool
| or : expression bool -> expression bool -> expression bool
| ifThenElse : expression bool -> expression a -> expression a -> expression a

I wanted a to represent any type but i don't know how to do that, can someone help me ?

[Horatiu Cheval]

You can set a as an argument of type Type to your constructor

[Horatiu Cheval]

ifThenElse (a : Type) : expression bool -> expression a -> expression a -> expression a

[Alice Laroche]

Yeah i tried of course, but then i got this error universe level of type_of(arg #1) of 'expression.ifThenElse' is too big for the corresponding inductive datatype

[Horatiu Cheval]

Right

[Horatiu Cheval]

Does it work if you let expression be of type Type -> Type 1?

[Alice Laroche]

Yes it's working, thanks

[Horatiu Cheval]

If it helps, the trouble was that since you were quantifying over any Type you needed something larger the Type for your definition to live in, which is provided by Type 1

[Alice Laroche]

Yeah i understanded , Now i wonder if there is a way to make a automatic type level ? So i can use every types level expression and not only type level 0

[Yaël Dillies]

Yeah, up to technical details that other people are more qualified to explain than me, you can use Type* to mean any type level.

[Horatiu Cheval]

Sure there is. The a argument in your constructor would be of type Type u and your inductive would be of type Type u -> Type (u+1)

[Horatiu Cheval]

After you first declare universe u somewhere before your definition

[Horatiu Cheval]

Or like Yaël says, you can in general use Type* to mean a type at any universe level. Though I am not sure there is a way to work with that in this particular instance, since you need to refer to the successor of the universe level

[Yaël Dillies]

I think it figures out by itself the lowest universe level it can work in.

[Horatiu Cheval]

So you can just write Type* everywhere and it just figures it out? That would be nice (sorry, I'm not at a computer right now and I can't check for myself)

[Eric Rodriguez]

most of the time - sometimes you'll get universe issues, like in the category theory library sometimes, and you have to help out, but otherwise yah

[Alice Laroche]

I already tried to use universe u , but then i got an error :

  ℕ
has type
  Type : Type 1
but is expected to have type
  Type u : Type (u+1)

[Adam Topaz]

You can use ulift \nat instead of \nat

[Alice Laroche]

Thanks