Datatype-Generic Programming Meets Elaborator Reflection
Datatype-generic programming is natural and useful in dependently typed languages such as Agda. However, datatype-generic libraries in Agda are not reused as much as they should be, because traditionally they work only on datatypes decoded from a library’s own version of datatype descriptions; this means that different generic libraries cannot be used together, and they do not work on native datatypes, which are preferred by the practical Agda programmer for better language support and access to other libraries. Based on elaborator reflection, we present a framework in Agda featuring a set of general metaprograms for instantiating datatype-generic programs as, and for, a useful range of native datatypes and functions —including universe-polymorphic ones— in programmer-friendly and customisable forms. We expect that datatype-generic libraries built with our framework will be more attractive to the practical Agda programmer. As the elaborator reflection features used by our framework become more widespread, our design can be ported to other languages too.
Tue 13 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
15:50 - 16:50 | Generic Programming and EducationICFP Papers and Events at Linhart Chair(s): Nicolas Wu Imperial College London | ||
15:50 20mTalk | Datatype-Generic Programming Meets Elaborator Reflection ICFP Papers and Events Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica, Liang-Ting Chen Academia Sinica, Tzu-Chi Lin Institute of Information Science, Academia Sinica Link to publication DOI Media Attached | ||
16:10 20mTalk | Practical generic programming over a universe of datatypes ICFP Papers and Events DOI | ||
16:30 20mTalk | Structural Versus Pipeline Composition of Higher-Order FunctionsVirtualExperience Report ICFP Papers and Events DOI |