search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
583 stars 236 forks source link

Use reflection to automatically derive generic functions #825

Open L-TChen opened 5 years ago

L-TChen commented 5 years ago

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.

MatthewDaggitt commented 5 years ago

I am 100% behind the idea of improving the standard library's reflection tools. And your use-cases all sound great, I know I'd certainly use them in some of my projects :+1:

Just to note though that I'm not quite sure how much we'd actually want to use such features in the library itself. Apart from areas where it is difficult to avoid and has enormous benefits (e.g. solvers), I think it's best to simply provide the tools for others to use. As you say reflection can be a bit mysterious, and ideally we'd like people to be able to understand the core part of the library without having to wade into reflection.