Why is Monoid a record rather than a Class about coq-ext-lib HOT 10 OPEN

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

from coq-ext-lib.

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.

from coq-ext-lib.

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.

from coq-ext-lib.

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.

?

from coq-ext-lib.

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) ...

from coq-ext-lib.

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?

from coq-ext-lib.

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?

from coq-ext-lib.

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

from coq-ext-lib.

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

from coq-ext-lib.

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.

from coq-ext-lib.