论文标题
数据量表对称及其与评估顺序的相互作用
Data-Codata Symmetry and its Interaction with Evaluation Order
论文作者
论文摘要
顾名思义，数据类型和码头类型通常被视为彼此的双重。但是，大多数编程语言都不以其全部的一般性来支持它们，或者如果这样做，它们仍然被视为具有单独定义的类型检查，汇编等的独特构造。Rendel等人。是第一个提出了两个标准程序转换的变体，即降低和重新调整的变体，以衡量和改善数据和尾巴类型之间的对称性。但是，在以前的作品中，尾巴和数据仍然被视为单独定义的语言构造，而将其定义为相似但单独的算法。这些作品还掩盖了上述转换与评估顺序之间的相互作用，这导致了理想的$η$扩展平等性的丧失。我们认为，完全对称性的失败是由于自然推论作为语言设计的逻辑基础所固有的不对称性。自然扣除是不对称的，因为它的重点是类型的生产者（证明），而消费者（上下文，连续性，反驳）具有二等状态。受现有基于序列的语言设计的启发，我们提出了完全对称的第一语言设计，因为极性（数据类型VS vs codata类型）和评估顺序（呼叫与呼叫与呼叫呼叫）没有缠结并成为单一形式的声明形式的独立属性。属性，极性和评估顺序都可以通过每种算法独立更改。特别是，现在已经是一种算法了。可以独立于极性定义和单独定义和更改评估顺序。通过仅允许评估顺序和极性的某些组合，可以恢复上述$η$法律。
Data types and codata types are, as the names suggest, often seen as duals of each other. However, most programming languages do not support both of them in their full generality, or if they do, they are still seen as distinct constructs with separately defined type-checking, compilation, etc. Rendel et al. were the first to propose variants of two standard program transformations, de- and refunctionalization, as a test to gauge and improve the symmetry between data and codata types. However, in previous works, codata and data were still seen as separately defined language constructs, with de- and refunctionalization being defined as similar but separate algorithms. These works also glossed over interactions between the aforementioned transformations and evaluation order, which leads to a loss of desirable $η$ expansion equalities. We argue that the failure of complete symmetry is due to the inherent asymmetry of natural deduction as the logical foundation of the language design. Natural deduction is asymmetric in that its focus is on producers (proofs) of types, whereas consumers (contexts, continuations, refutations) have a second-class status. Inspired by existing sequent-calculus-based language designs, we present the first language design that is fully symmetric in that the issues of polarity (data type vs codata types) and evaluation order (call-by-value vs call-by-name) are untangled and become independent attributes of a single form of type declaration. Both attributes, polarity and evaluation order, can be changed independently by one algorithm each. In particular, defunctionalization and refunctionalization are now one algorithm. Evaluation order can be defined and changed individually for each type, independently from polarity. By allowing only certain combinations of evaluation order and polarity, the aforementioned $η$ laws can be restored.
