Conversation
|
Is there a reason not to use an existing library? |
|
What library did you have in mind? (I tend to accidentally reinvent the wheel a bunch.) |
|
My reason for adding this is to make writing some TemplateMonad code that manages some state on the side a bit easier, in writing automation for proving well-typedness of quotation. It doesn't seem worth it to add another dependency to MetaCoq just for this purpose, unless we want to rip out all the monad utils and replace them with whatever library we'd be using. |
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. |
JasonGross
force-pushed
the
coq-8.16+state-monad
branch
from
24241a5 to
d0d517b
Compare
|
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. |
|
It would be fine to depend on extlib from my viewpoint. This also avoids unintentional universe/notation clashes when using both MetaCoq and extlib |
3 participants
No description provided.