Open Lysxia opened 4 years ago
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.
On a related note, what's the purpose of PMonad
again?
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.
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).
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.
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.
Original title: Use single-method class for Monad
Proposal: put
bind
andret
into their own classes, and letMonad
be a dummy class indexed by those two:That way,
bind
andret
don't simplify away when used with concrete monads. This also allowsret
to be shared withApplicative
, since of course I am extending my proposal to all multi-field classes.