Zulip Chat Archive

Stream: general

Topic: Generlized algebric data type


Alice Laroche (Jun 25 2021 at 15:44):

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 (Jun 25 2021 at 15:47):

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

Horatiu Cheval (Jun 25 2021 at 15:47):

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

Alice Laroche (Jun 25 2021 at 15:48):

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 (Jun 25 2021 at 15:48):

Right

Horatiu Cheval (Jun 25 2021 at 15:49):

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

Alice Laroche (Jun 25 2021 at 15:50):

Yes it's working, thanks

Horatiu Cheval (Jun 25 2021 at 15:57):

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 (Jun 25 2021 at 16:06):

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 (Jun 25 2021 at 16:11):

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 (Jun 25 2021 at 16:12):

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 (Jun 25 2021 at 16:13):

After you first declare universe u somewhere before your definition

Horatiu Cheval (Jun 25 2021 at 16:16):

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 (Jun 25 2021 at 16:27):

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

Horatiu Cheval (Jun 25 2021 at 16:32):

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 (Jun 25 2021 at 17:08):

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 (Jun 25 2021 at 17:22):

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 (Jun 25 2021 at 17:25):

You can use ulift \nat instead of \nat

Alice Laroche (Jun 25 2021 at 17:28):

Thanks


Last updated: Dec 20 2023 at 11:08 UTC