一句话：提出基于 elaborator 反射的 Agda 框架，使数据类型泛型程序可直接实例化到原生数据类型与函数。
在 Agda 等依赖类型语言中，数据类型泛型编程自然且有用，但现有泛型库通常只作用于由库自身数据类型描述解码出的类型，导致不同泛型库难以互操作，也无法直接用于程序员更偏好的原生数据类型。本文基于 elaborator reflection 提出一个 Agda 框架，提供一组通用元程序，可将 datatype-generic 程序实例化为面向原生数据类型和函数（包括宇宙多态类型）的形式，且实例化方式对程序员友好、可定制。该工作预期能让基于此框架构建的泛型库对实践中的 Agda 程序员更具吸引力；随着 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.
@article{paperbot1496,
title = {Datatype-generic programming meets elaborator reflection},
author = {Hsiang-Shang Ko and Liang-Ting Chen and Tzu-Chi Lin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547629}
}