There's some discussion at #952 about the monadic utils in MetaCoq and the idea of replacing them with a dependency on ExtLib.

Gregory Malecha said:

- ExtLib has a fairly complete monad library. The itrees work is building on that. I am not certain the status of the theory.
- stdpp has some as well, but it is smaller.
- I'm less certain about other things, but MathClasses probably has something.
Writing a good monad library with theory is not easy due to universes (stdpp has some issues with this) and some of the issues that you highlighted in your paper on category theory in Coq. This is the main reason that I think it would useful to not build another library.

I replied:

Is the ExtLib library universe polymorphic and cumulative? (It looks like right now it's universe polymorphic but not cumulative, which will break some of the MetaCoq code IIRC.) If so, I'd be happy to have the MetaCoq monad library replaced with that (assuming everyone is on board with adding the dependency), though I don't think I have the time to make the replacement myself.

Note, however, that MetaCoq doesn't need any theory associated with the monad operations, because the library is just for convenient syntax for running template programs, and there's no reasoning that needs to be done about them. Similarly, I'm adding a state monad here so that I can get easy management of state when using the template monad, and don't need any fancy theory.

Thoughts?

Indeed :-)

https://github.com/coq-community/math-classes/blob/master/theory/monads.v

I seem to recall it's not dissimilar to the one in extlib, also because we had quite a few discussions between math-classes and extlib at the time.

I agree, it would be great if we could avoid code duplication.

I've been thinking a little about this in the past, and I do think we'll need several monad libraries in Coq (at least one for haskell and one for category theory).

off the top of my head, we already have John Wigley's category theory library with monads, monae library for MathComp, ExtLib, math-classes

Last updated: Jul 23 2024 at 20:01 UTC