归纳族的自定义表示

归纳族为使用依赖类型进行编程提供了一种便捷的方式。然而在编译时，其默认的链接树运行时表示，以及在同一数据的不同索引视图之间进行转换的需求，可能导致不令人满意的运行时性能。在本文中，我们引入了一种带有依赖类型和具有可自定义表示的归纳族的语言。这种表示是 Wadler 视图的一个版本，像 Epigram 中那样被改进以适用于归纳族，但具有编译保证：一个被表示的归纳族不会留下任何运行时痕迹，而无需依赖诸如去森林化之类的启发式方法。通过这种方式，我们可以基于最简的原语集构建一个便捷的归纳族库，其重新索引和转换函数在编译期间会被擦除。我们展示了如何表达优化技术，例如将类 Nat 类型表示为 GMP 风格的大整数，而无需在编译器中进行特殊处理。借助依赖类型，通过提供的模态，对数据表示进行推理也成为可能。这产生了原始数据与被表示数据之间在计算上不相关的同构。