Simplify Monad about coq-ext-lib HOT 6 OPEN

Another alternative is to prevent bind and ret from simplifying, which solves that one problem, but not the one about sharing identifiers. More generally, it's kind of an arbitrary choice to bundle a certain set of methods together in a record, while indexed classes make it easier to mix and match.

from coq-ext-lib.

On a related note, what's the purpose of PMonad again?

from coq-ext-lib.

PMonad was introduced to allow for talking about well-formed types without needing to introduce axioms such as functional extensionality. It was never used extensively and is a good candidate for removal.

On the ret and bind, my only worry with this is terms will get much larger. Rather than simply forall m : Type -> Type, Monad m -> .... you will end up with forall (m : Type -> Type) (rm : Ret m) (bm : Bind m), Monad m rm bm -> ... which can be a lot of extra type checking and a lot of places where resolution can (potentially) get confused. Also, Ret isn't a very good typeclass name. I believe that it is usually called Pointed or something like that.

from coq-ext-lib.

One other thing, I get the impression that there are some users of ExtLib and this change would be a breaking change. We should ensure that if we do this, that we bump the major version number and leave the old packages in Opam (possibly also maintaining them for a little while depending on interest).

from coq-ext-lib.

I've experimented with this a bit and I have to agree that unbundling the Monad class like that makes things too heavyweight.

If we can drop PMonad that would also be great.

from coq-ext-lib.

I think dropping PMonad is a good idea, we really need a better notion of equivalence in Coq otherwise most of these things are too painful.

from coq-ext-lib.