一句话：在 Curry 风格依赖类型论中用恒等函数内部化泛型复用，使非索引与索引数据类型及其程序零开销复用。
依赖类型语言长期存在代码复用难题：传统非索引代数数据类型（如列表）与众多索引变体（如向量）并存，函数常需针对本质相同的数据类型分别重写，造成重复。本文在 Curry 风格依赖类型论中工作，其中同一无类型项可同时被归类为非索引与索引版本的数据类型。作者利用这一特点，提出一种依赖类型泛型编程方案，将零开销复用内部化为 Curry 风格理论中的恒等函数，从而既能复用数据与程序，又避免运行时开销。摘要未报告实验评估。
Dependently typed languages are well known for having a problem with code reuse. Traditional non-indexed algebraic datatypes (e.g. lists) appear alongside a plethora of indexed variations (e.g. vectors). Functions are often rewritten for both non-indexed and indexed versions of essentially the same datatype, which is a source of code duplication. We work in a Curry-style dependent type theory, where the same untyped term may be classified as both the non-indexed and indexed versions of a datatype. Many solutions have been proposed for the problem of dependently typed reuse, but we exploit Curry-style type theory in our solution to not only reuse data and programs, but do so at zero-cost (without a runtime penalty). Our work is an exercise in dependently typed generic programming, and internalizes the process of zero-cost reuse as the identity function in a Curry-style theory.
@article{paperbot277,
title = {Generic zero-cost reuse for dependent types},
author = {Larry Diehl and Denis Firsov and Aaron Stump},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236799}
}