For the sake of example, let’s say I want to represent semigroups in Coq. There are quite a few different ways to go about this.
A semigroup is a set plus a binary operation, which is associative.
Record Sg := {
C : Type;
app : C -> C -> C;
assoc : forall a b c, app (app a b) c = app a (app b c);
}.
1: Should Sg have its carrier as a field (as above), or as an index?
Record Sg (C : Type) := {
app : C -> C -> C;
assoc : ...;
}.
This makes it easier to represent types which are carriers of multiple structures.
(* A function for C that is both a Sg and a Foo *)
Definition f (C : Type) (Sg_C : Sg C) (Foo_C : Foo C) := ...
But you could also say the same of the app operation in the Sg record, it could be associated with different algebraic structures, so should it be an index too?
2: Should the laws be in a separate record?
Record Sg (C : Type) := {
app : C -> C -> C;
}.
Record LawfulSg (C : Type) (sg : Sg C) : Prop := {
assoc : ...
}.
There are various advantages of keeping proof terms separate from “computational” terms. One is performance (you don’t need to worry about choosing an evaluation order which avoids reducing expensive proof terms if they don’t occur in the first place). Another is that if you have proof terms lying around sooner or later you’ll run into issues of proof relevance, as you try to relate functions which consume or produce proof terms.
3: Here again we have the choice of representing the subject of the laws as an index (above) or as a field:
Record LawfulSg (C : Type) := {
sg :> Sg C;
assoc : ...;
}.
What other alternatives are there? Is there a recommended approach? Can you point me to literature discussing the trade-offs?
