数据-编码对称性及其与求值顺序的交互
摘要：数据类型和共数据类型通常被看作是彼此的对偶。然而，大多数编程语言不能以完全泛化的方式支持它们，或者如果它们可以，它们仍然被视为具有分别定义的类型检查、编译等的不同构造。Rendel等是第一个提出两个标准程序转换的变体（去/去功能化）作为测试来衡量和改善数据类型和共数据类型之间对称性的人。然而，在先前的工作中，共数据和数据仍然被视为分别定义的语言构造，去/去功能化被定义为相似但独立的算法。这些工作还忽略了上述转换与求值顺序之间的交互作用，从而导致了令人愉快的eta展开等式的丢失。我们认为完全对称性的失败是由于自然推理作为语言设计的逻辑基础的固有不对称性。自然推理是不对称的，因为它的重点是类型的生成者（证明），而消费者（上下文、延续、驳回）则具有二等公民地位。受现有基于序演算的语言设计的启发，我们提出了第一个完全对称的语言设计，其中极性（数据类型与共数据类型）和求值顺序（值调用vs名称调用）的问题被解开，成为单个类型声明的独立属性。两个属性，极性和求值顺序，可以通过各自的算法独立地进行更改。特别地，去/去功能化现在是一个算法。求值顺序可以针对每种类型单独定义和更改，与极性无关。通过仅允许特定的求值顺序和极性组合，可以恢复上述eta规则。
作者：David Binder, Julian Jabs, Ingo Skupin, Klaus Ostermann
论文ID：2211.13004
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-11-24