MonadLaws duplicated

[vzaliva]

Interaction Trees defines it's own class MonadLaws (in Monad.v) while there is already similar class in ExtLib (MonadLaws.v).

The comment says:

  (* This should go coq-ext-lib. *)
  Class MonadLaws :=

[YaZko]

Hi Vadim,

Yes we are aware of this comment, but it is not possible to merge for now. We work with monads equipped with their own notion of equivalence, as opposed to Leibniz equality as in the statement of the laws from ExtLib. Extending ExtLib to our setup at some point is probably the right move, but we are still experimenting with further generalizations (branches prop_eqmR_typ most notably, in collaboration with Irene Yoon). We would also need to make sure that the generalization does not break code for users of ext-lib.

So for now we do indeed host our own monad laws locally.

[vzaliva]

That's reasonable. Perhaps we can use different class names to avoid confusion?

[Lysxia]

That's reasonable. Perhaps we can use different class names to avoid confusion?

Sounds good to me. As a concrete proposal, I would rename it as MonadLawsR (with an R suffix to indicate that it's parameterized by an equivalence relation).

I'll work on a new release by early July.

[vzaliva]

I would go with E suffix (for "equality") buy it is a matter of taste :)

I suggest you take a look at how it is done in math-classes library. They have an elaborate setup with Equal and Equivalence typelcasses which is quite nice, except the horrible decision to overload =