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.
- 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.