Description
This is a proposal intended for further discussion.
Goal. Eliminators, recursors, traversals, and other generic functions should be generated by the reflection framework to reduce the duplicated work. It is also an experiment on the reflection framework.
Background. It is known that every strictly positive data type is associated with a canonical induction principle (eliminator), and it is fairly straightforward to define one for each individual case. The existing reflection principle allows us to define functions by metaprograms, so eliminators and recursors in theory can be derived automatically, similarly for map, traverse, etc. We can also try out other applications of reflection like converting general recursion to structural recursion (Bove & Capretta, 2005) as implemented in Idris (Christiansen & Brady, 2016).
Evaluation. This is doable but very time-consuming, since the User Manual on reflection is rather brief and unfriendly even to experienced users. It is not easy to debug metaprograms either. By doing so, I anticipate the standard library needs to support more programming-oriented features, e.g., instance arguments. Eventually, we may want a proper Prelude module similar to Norell's agda-prelude https://github.com/UlfNorell/agda-prelude.
It is unclear where to start first, but at least I'd like to mention the idea. This could also be a student project (or a few) on metaprograms.