一句话：为 Agda 设计了一个安全易用的数据类型泛型编程库：泛型构造是普通 Agda 函数，可一行特化到原生数据类型。
数据类型泛型编程让同一构造可复用于大量数据类型，在依赖类型语言中还能构造泛型证明，但现有接口要么难以使用，要么所支持的数据类型范围有限。本文在 Agda 中设计了一个安全且易用的数据类型泛型编程库：其核心是一个覆盖广泛数据类型的 universe，泛型构造仍是普通的 Agda 函数，却可以通过一行代码特化到原生 Agda 数据类型；库还提供可复用的构建块，使库设计者能够自行定义新的泛型构造。作者以库实现与示例说明了该设计在可用性和覆盖范围上的改进，从而在依赖类型设定下兼顾安全性与实用性。
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.
@article{paperbot1486,
title = {Practical generic programming over a universe of native datatypes},
author = {Lucas Escot and Jesper Cockx},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547644}
}