Simplify Monad

[Lysxia]

Original title: Use single-method class for Monad

Proposal: put bind and ret into their own classes, and let Monad be a dummy class indexed by those two:

Class Bind m := bind : forall a b, m a -> (a -> m b) -> m b.
Class Return m := ret : forall a, a -> m a.  (* And some are starting to prefer "pure" to "return" in Haskell *)
Class Monad m `{Bind m} `{Return m} := {}.
Instance MonadWith m `{Bind m} `{Return m} : Monad m := {| |}.

That way, bind and ret don't simplify away when used with concrete monads. This also allows ret to be shared with Applicative, since of course I am extending my proposal to all multi-field classes.

[Lysxia]

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.

[Lysxia]

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

[gmalecha]

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.

[gmalecha]

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

[Lysxia]

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.

[gmalecha]

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.