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:
What is the extraneous _
doing at the end of Arguments Ok {OkType ErrType} _.
?
The command works fine even if _
is omitted.
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!
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.
Regarding the extra _
, for Ok
it corresponds to the x : OkType
.
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).
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!
Regarding the extra
_
, forOk
it corresponds to thex : OkType
.
Ah, makes sense, only now then I realise every result
constructors takes two extra arguments due to the polymorphic declaration.
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
Jiahong Lee has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC