一句话：提出四类引入/消去（左/右）规则构成的编程语言设计空间，并用双表达性原则与证明/反驳对偶分析其模块化影响。
函数式编程语言设计长期受自然演绎框架影响，将语言构造分为值的引入规则和消去规则。在基于相继式演算的语言中，左引入规则可替代右消去规则，为值的使用者提供专门子语言。该文提出并分析一个更广的设计空间，其中规则在引入/消去与左/右两个维度上共有四类组合。文章考察规则选择对程序结构与模块化的影响，识别出“程序结构跟随数据结构”的四种实现方式，并说明它们分别对应四类规则选择。作者还提出双表达性（bi-expressibility）原则，以指导和验证联结词规则的设计，并借助证明/反驳对偶深化不同联结词之间的对偶关系。评估以理论分析与设计空间刻画为主。
Functional programming language design has been shaped by the framework of natural deduction, in which language constructs are divided into introduction and elimination rules for producers of values. In sequent calculus-based languages, left introduction rules replace (right) elimination rules and provide a dedicated sublanguage for consumers of values. In this paper, we present and analyze a wider design space of programming languages which encompasses four kinds of rules: Introduction and elimination, both left and right. We analyze the influence of rule choice on program structure and argue that having all kinds of rules enriches a programmer’s modularity arsenal. In particular, we identify four ways of adhering to the principle that ”the structure of the program follows the structure of the data“ and show that they correspond to the four possible choices of rules. We also propose the principle of bi-expressibility to guide and validate the design of rules for a connective. Finally, we deepen the well-known dualities between different connectives by means of the proof/refutation duality.
@article{paperbot1505,
title = {Introduction and elimination, left and right},
author = {Klaus Ostermann and David Binder and Ingo Skupin and Tim Süberkrüb and Paul Downen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547637}
}