跨Orbit传输函数
Transporting Functions across Ornaments
摘要：
使用依赖类型进行编程是一种祝福，也是一种诅咒。能够将不变量烘焙到数据类型的定义中是一件幸事：我们终于可以编写出构造正确的软件了。然而，这种极端的准确性也是一种诅咒：数据类型是结构化介质与特殊用途逻辑的组合。这些特定于域的逻辑阻碍了在类似结构的数据之间进行代码重用的任何努力。在本文中，我们通过将装饰的概念适应于归纳族的宇宙来驱除我们的数据类型。然后，我们将展示如何代码重用可以实现的功能。使用这些函数装饰，我们捕捉到了函数之间的关系，例如自然数的加法和列表的连接。有了这些知识，我们演示了前者的实现如何通知后者的实现：用户可以要求将添加的定义提升到列表中，并且她只会被要求进行添加列表而不是数字所需的细节。我们的演示文稿是正式的类型论与宇宙的数据类型和我们所有的建设已被实现为通用程序，不需要扩展的类型论。
英文摘要：
Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of data-types: we can finally write correct-by-construction software. However, this extreme accuracy is also a curse: a data-type is the combination of a structuring medium together with a special purpose logic. These domain-specific logics hamper any effort of code reuse among similarly structured data. In this paper, we exorcise our data-types by adapting the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornament, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. With this knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: the user can ask the definition of addition to be lifted to lists and she will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in a type theory with a universe of data-types and all our constructions have been implemented as generic programs, requiring no extension to the type theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
