monad library about coq-ext-lib HOT 6 OPEN

More questions from email discussion with @gmalecha:

The first question is whether the laws should be in the same record as the operations. Doing this simplifies a lot of things, but does introduce some issues because sometimes the laws require functional extensionality which breaks reduction if used poorly.

The other thing is that, because monads are higher-order, there are questions about the equivalence relation. the general structure is a function : (a -> a -> Prop) -> m a -> m a -> Prop that has the appropriate properties.

The easier option is to require the relation on a to be equality. That simplifies things, but often requires functional extensionality for monad transformers. This is solved by higher inductive types, but those (sadly) still do not exist in Coq.

So maybe that summarizes the questions that need to be answered.

from coq-ext-lib.

Thanks! As I mentioned in the email, it seems like two concrete steps are:

• catalog the existing implementations of Monad, Functor, Applicative
• determine the "right" definitions. This involves universes, where the laws are, the "correct" levels.

We might want to talk to people who have done other implementations before doing the second one, as an existing definition might work.

from coq-ext-lib.

Regarding the relations, this seems to require a basic notion of equivalence for every type, and this is where things get opinionated because Coq doesn't provide a canonical solution. Type classes (something like type in ext-lib) or canonical structures.

Any way you slice it, to phrase the laws conveniently, you will probably need one of these.

from coq-ext-lib.

I've noticed that ExtLib.Core.Type is gone along with things like type_libniz. I guess this will help with the equality problem?

from coq-ext-lib.

I think this depends on how you define "help". To properly do the monad laws, we need a way to define setoids and we lost that when we dropped ExtLib.Core.Type. But there wasn't any good example on actually using ExtLib.Core.Type so it is debatable how useful it is.

from coq-ext-lib.

I think the interface is fine as it is, with the Laws separate and no setoids. One has the option not to use extlib if they want something else, and the existing copies are enough to justify a separate coq-monads library (IMHO)

from coq-ext-lib.