ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Tue 13 Sep 2022 15:50 - 16:10 at Linhart - Generic Programming and Education Chair(s): Nicolas Wu

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 Sep

Displayed 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
20m
Talk
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
20m
Talk
Practical generic programming over a universe of datatypes
ICFP Papers and Events
Lucas Escot TU Delft, Jesper Cockx TU Delft
DOI
16:30
20m
Talk
Structural Versus Pipeline Composition of Higher-Order FunctionsVirtualExperience Report
ICFP Papers and Events
Elijah Rivera Brown University, Shriram Krishnamurthi Brown University, United States
DOI