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

Datatype-generic programming makes it possible to define a construction once and apply it to a large class of datatypes. This is often useful to avoid code duplication in languages that encourage the definition of custom datatypes. In particular, state-of-the-art dependently-typed languages encourage users to define variants of the same datatype with different type-level invariants, highlighting a desperate need for datatype-generic programming. In addition to giving access to familiar programming constructions for free, datatype-programming in the dependently-type setting allows for useful proof-related constructions. However, the current interfaces available for this purpose are needlessly hard to use or are limited in the range of datatypes they handle. In this paper, we describe the steps undertaken so as to make safe datatype-generic programming available in the Agda programming language. Compared to existing work, our library has the benefit of defining a richer set of constructions that can be used in the safe fragment of Agda. Their interface is mostly free of any reference to the underlying encoding, making it almost as natural to work with as handwritten code. Furthermore, we provide building blocks so that users can too define their own datatype-generic constructions.

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 Institute of Information Science, 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