There are quite a few existing options, but I wonder specifically, for those familiar with Haskell, whether there is any equivalent to Haskell’s Scrap your boilerplate or GHC.Generics?
Feel free to share any of your thoughts about the broader topic of metaprogramming in Coq here as well.
Other solutions I’m aware of:
Dependent types and type classes. They do offer a flavor of what would be metaprogramming in other languages.
Tactics.
Plugins.
MetaCoq, which is roughly an equivalent of Template Haskell.
Tactics and plugins have the issue that they’re not Gallina, so you have to use another language, and we can’t reason about them within Coq. Furthermore, plugins take heavy maintenance because the interface is unstable.
MetaCoq is definitely nice by most standards. As far as I can tell, it manipulates ASTs, which I consider rather heavyweight.
The flavor of metaprogramming I’m looking for can be seen as an extension of 1, programming with good old dependent types. The main missing bit is an automatically generated first-class representation of a (co)inductive type’s definition, and the similarity with metacoq stops here because then you’re manipulating actual values. Recursion and universes certainly seem problematic though. If you have any details to offer, I’m all ears.
The answer to your question could very well be Mtac2. Full disclosure: I happen to be one of the developers of Mtac2.
Mtac2 is built on top of Gallina and it makes heavy use of dependent types. Thus it can get away without manipulating ASTs most of the time. I have not yet finished the full interface for interacting with inductive types in a type-safe way (using first-class representations that can be interpreted with plain Coq functions) but I am happy to make that a priority if there is demand for that. As it stands now, inspecting inductive types doesn’t give you a lot of type information to work with. You can recompute all that information, of course. Still, you would probably have to come up with your own representation of inductives.
Coincidentally, I am currently writing a series of blog posts that will (once it’s finished) show how to get rid of boilerplate that usually comes with reflection/reification tactics. I plan to incorporate both the inspection of inductive types as well as the generation of new inductives (and lemmas/definitions). It should be instructive for the kind of meta-programming that you are interested in. It should also give me an idea of what the right representation of inductive types in Mtac2 will be, eventually.
Most of my time working on Mtac2 goes into new features. Consequently, there is very little documentation. The repository’s README.md has a link to our most recent paper on Mtac2. That paper contains a general introduction to Mtac2 metaprogramming. The blog posts will also serve as some kind of introduction to Mtac2 once they are done. Apart from that, it’s best to contact the developers directly. If you want to do something and it’s not clear how to do that, you can create an issue in the github repository and we’ll try to guide you towards a solution. Hopefully, over time, we can convert these issues into a FAQ document or something like that.
