Open lastland opened 4 years ago
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.
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.
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.
?
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) ...
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?
If you can provide more information, I'm happy to see if I can find a nice way to address your problem.
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?
I have a short example here for you to play with https://gist.github.com/p3rsik/5c57b38c6f37734bece81b675dd0b238
@gmalecha I am also curious to see if there is a better solution.
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.
Monoids in
coq-ext-lib
are defined as follow: https://github.com/coq-community/coq-ext-lib/blob/ee71d144bd2a171532d9243198538c93aebb8a58/theories/Structures/Monoid.v#L11-L14Is there a special reason that the definition is a
Record
rather than aClass
? 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 aninstance
of aMonoid
unless you useExisting Class Monoid
(why cannot be found incoq-ext-lib
).