Why is Monoid a record rather than a Class

[lastland]

Monoids in coq-ext-lib are defined as follow:

coq-ext-lib/theories/Structures/Monoid.v

Lines 11 to 14 in ee71d14

	Record Monoid@{} : Type :=
	{ monoid_plus : S -> S -> S
	; monoid_unit : S
	}.

Is there a special reason that the definition is a Record rather than a Class? I know that, under the hood, they are the same thing, but if my understanding is correct, you will not be able to declare a data structure as an instance of a Monoid unless you use Existing Class Monoid (why cannot be found in coq-ext-lib).

[gmalecha]

The reason is that the index of the data structure (T) does not uniquely determine the Monoid. You could have + and 0, or * and 1, etc. We could go the Haskell route and wrap things, but I chose not to go that way initially because the wrapping incurs a performance cost.

[vzaliva]

But unlike Haskell Coq allows multiple typeclass instances for a type.
I do not have statistics on this but I suspect that in most practical uses there will be one monoid per type and using typeclass will make it much easier to work with it. In rare cases when there are multiple monoids per type they will have to specify which instance to use implicitly.

[p3rsik]

Is this is the intended way of doing monoid-related things(suppose I need Monoid (list ..) instance for WriterMonad:

Existing Class Monoid.
Existing Instance Monoid_list_app.

?

[gmalecha]

My understanding is that Existing Class is "infectious", so if you use it, then everyone who depends on you is also forced to use it. If this is the recommended style, then ExtLib should change Monoid into a Class and users should specify instances manually when there are multiple of them.

An alternative is to use Local notations for certain things, e.g.

Local Notation "a ++ b" := (Monoid_list_app.(monoid_plus) a b) ...

[p3rsik]

I'm not writing a lib, I need it only for a certain class of definitions... What is a Local notations thing? How can it help me to write MonadWriter instances? Maybe you know a better way to do this?

[gmalecha]

If you can provide more information, I'm happy to see if I can find a nice way to address your problem.

[p3rsik]

It would be very nice.
Basically, the problem is that I got an error while trying to use tell(from MonadWriter) saying:

Error: Cannot infer the implicit parameter MT of tell whose type is "Monoid (list Z)".

In this definition:

Definition test : cM unit := tell (cons 1%Z nil).

Where cM is a custom monad that has MonadWriter instance.
If I understood this problem correctly, it all comes down to the fact, that Monoid isn't a typecleass, so resolver don't even know about it and it's instances.
If I'm not mistaken there must be some common way to do this, because every MonadWriter instance needs a log that is a Monoid instance.
So, what is the best solution for this?

[p3rsik]

I have a short example here for you to play with
https://gist.github.com/p3rsik/5c57b38c6f37734bece81b675dd0b238

[vzaliva]

@gmalecha I am also curious to see if there is a better solution.

[gmalecha]

Sorry for not responding earlier. The hacky way to solve this problem is something like:

Local Notation tell := (tell (M:=Monoid_list_app _))

You can also convert this into a definition like:

Definition tellN (n : list Z) : Writer nat unit :=
  tell (M:=Monoid_list_app ...) n.

A better solution, however, would be ideal. Perhaps that is to make Monoid a type class and wrap things the way that Haskell does, i.e. you might not have an instance for Monoid nat but rather for something like:

Record Plus : Set := mkPlus
{ unplus : nat }.
Coercion mkPlus : nat >-> Plus.
Instance Monoid_Plus : Monoid Plus :=
{ monoid_plus a b := mkPlus (Nat.add a.(unplus) b.(unplus))
; monoid_unit := mkPlus 0 }.

... MonadWriter Plus T.

This is a lot of boilerplate though.