Stream: Coq users

Topic: ✔ Define Polymorphic Datatype

Jiahong Lee (Jun 02 2022 at 05:09):

Hi, I'm very new to Coq.

I'm given this sample code to define a polymorphic datatype:

Inductive result (OkType ErrType:Type) : Type :=
| Ok (x : OkType)
| Error (x : ErrType).

Arguments Ok {OkType ErrType} _.
Arguments Error {OkType ErrType} _.

It works, but too verbose. Suppose I have five or tens or hundreds of data constructors, I would have to repeat the Arguments command for that many times. Inspired by how I can define an implicit argument for a function, I figure out I can do something like this:

Inductive result2 {OkType ErrType:Type} : Type :=
| Ok2 (x : OkType)
| Error2 (x : ErrType).

I put curly braces surrounding the signatures of the datatype parameters.

Questions:

1. What is the extraneous _ doing at the end of Arguments Ok {OkType ErrType} _.?
   The command works fine even if _ is omitted.

2. Is result2 the right shorthand to define implicit arguments for data constructors?
   Although Ok2 and Error2 work fine for my purpose, their types are different from Ok and Error. To illustrate:

Ok
     : ?OkType -> result ?OkType ?ErrType
where
?OkType : [ |- Type]
?ErrType : [ |- Type]

Error
     : ?ErrType -> result ?OkType ?ErrType
where
?OkType : [ |- Type]
?ErrType : [ |- Type]

Ok2
     : ?OkType -> result2
where
?OkType : [ |- Type]
?ErrType : [ |- Type]

Error2
     : ?ErrType -> result2
where
?OkType : [ |- Type]
?ErrType : [ |- Type]

That's why I'm not sure whether result2 is the correct shorthand to define a polymorphic datatype.

Thanks!

Théo Winterhalter (Jun 02 2022 at 05:53):

The second is the way to go I think, but it also makes the parameters implicit in the type, you can add the line

Arguments result2 _ _ : clear implicits.

to fix it.

Théo Winterhalter (Jun 02 2022 at 05:53):

Regarding the extra _, for Ok it corresponds to the x : OkType.

Théo Winterhalter (Jun 02 2022 at 05:54):

Arguments can work on a prefix of the arguments (thankfully because there is no distinction between a function with one argument returning a function and a function with two arguments).

Jiahong Lee (Jun 02 2022 at 08:32):

Théo Winterhalter said:

The second is the way to go I think, but it also makes the parameters implicit in the type, you can add the line

Arguments result2 _ _ : clear implicits.

to fix it.

Thanks, this works!

Jiahong Lee (Jun 02 2022 at 08:33):

Regarding the extra _, for Ok it corresponds to the x : OkType.

Ah, makes sense, only now then I realise every result constructors takes two extra arguments due to the polymorphic declaration.

Jiahong Lee (Jun 02 2022 at 08:39):

Arguments can work on a prefix of the arguments (thankfully because there is no distinction between a function with one argument returning a function and a function with two arguments).

I see, I thought that holds for every command due to function currying? Not sure, I'm just getting started

Notification Bot (Jun 02 2022 at 08:40):

Jiahong Lee has marked this topic as resolved.

Last updated: Sep 28 2023 at 11:01 UTC