Stream: MetaCoq

Topic: Monad utils / new ExtLib dependency

view this post on Zulip Jason Gross (Apr 24 2023 at 20:11):

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:

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.


view this post on Zulip Bas Spitters (Apr 25 2023 at 07:28):

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

view this post on Zulip Karl Palmskog (Apr 25 2023 at 07:32):

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