Practical generic programming over a universe of native datatypes

Research output: Contribution to journalArticleScientificpeer-review

2 Citations (Scopus)
58 Downloads (Pure)

Abstract

Datatype-generic programming makes it possible to define a construction once and apply it to a large class of datatypes. It is often used to avoid code duplication in languages that encourage the definition of custom datatypes, in particular state-of-the-art dependently typed languages where one can have many variants of the same datatype with different type-level invariants. In addition to giving access to familiar programming constructions for free, datatype-generic programming in the dependently typed setting also allows for the construction of generic proofs. 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 design of a library for safe and user-friendly datatype-generic programming in the Agda language. Generic constructions in our library are regular Agda functions over a broad universe of datatypes, yet they can be specialized to native Agda datatypes with a simple one-liner. Furthermore, we provide building blocks so that library designers can too define their own datatype-generic constructions.

Original languageEnglish
Article number113
Number of pages25
JournalProceedings of the ACM on Programming Languages
Volume6
Issue numberICFP
DOIs
Publication statusPublished - 2022

Keywords

  • Dependent types
  • Generic programming

Fingerprint

Dive into the research topics of 'Practical generic programming over a universe of native datatypes'. Together they form a unique fingerprint.

Cite this