monad library

[vzaliva]

My original suggestion:

I have seen many projects putting together their own Monad stuff in Coq. Sometimes poorly. Ideally, they should all use ExtLib, but I think it has more than people really need and they are hesitant to bring another foundation library as a dependency.

Have you thought about breaking down ExtLib and moving Mondas into a separate small library? Call it something 'coq-monads' so people can easily find it. I think that will lower the barrier to entry and many more projects will adopt it. How knows, this could be a "gateway drug" to use the rest of ExtLib later :)

Comment from @gmalecha (PR #77):

I also wonder if there would be interest from the community to pull out Monad, Functor, Applicative as a separate library. There are a lot of libraries with exactly the same definitions and it is kind of annoying to have the same code in multiple dependencies because they don't interoperate. Specifically, I am thinking about stdpp, extlib, and meta-coq, but I wouldn't be surprised if there are others.

[vzaliva]

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.

[gmalecha]

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.

[gmalecha]

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.

[vzaliva]

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

[gmalecha]

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.

[mattam82]

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)