处理双向控制流：技术报告
Handling Bidirectional Control Flow: Technical Report
摘要：
由于编写异步、事件驱动代码的困难，主流语言最近一直在构建对各种高级控制流特性的支持。与此同时，实验性的语言设计已经建议将效果处理程序作为程序员定义的控制效果的统一解决方案，包括异常，生成器和case-await。尽管有这些趋势，但复杂的控制流-特别是呈现双向模式的控制流-仍然是管理的挑战。我们引入了双向代数效应，这是一种新的编程抽象，它以更自然的方式支持双向控制传输。双向效果的处理程序可以引发更多的效果，以将控制转移回引发初始效果的站点，并且可以使用它们自己来处理它们自己的效果。我们提出了这种表达能力的应用程序，当我们推动有效编程与面向对象编程的统一时，这种表达能力自然会消失。我们正式使用一种核心语言来概括效果操作和效果处理程序，从而确定了机制和统一。控制效果（如异常）的通常传播语义在效果多态性存在时与模块化推理冲突-它破坏了参数性。双向性加剧了问题。因此，我们开始展示核心语言，它建立在现有的隧道语义的代数效果，不仅是类型安全的（没有效果不处理），而且是抽象安全的（没有效果被意外处理）。我们设计了一个步骤索引的逻辑关系模型，并构造了它的参数性和可靠性证明。这些核心结果在Coq中完全机械化。初步实验表明，作为一个一流的语言功能，双向处理程序可以有效地实现。
英文摘要：
Pressed by the difficulty of writing asynchronous, event-driven code, mainstream languages have recently been building in support for a variety of advanced control-flow features. Meanwhile, experimental language designs have suggested effect handlers as a unifying solution to programmer-defined control effects, subsuming exceptions, generators, and async--await. Despite these trends, complex control flow---in particular, control flow exhibiting a bidirectional pattern---remains challenging to manage. We introduce bidirectional algebraic effects, a new programming abstraction that supports bidirectional control transfer in a more natural way. Handlers of bidirectional effects can raise further effects to transfer control back to the site where the initiating effect was raised, and can use themselves to handle their own effects. We present applications of this expressive power, which falls out naturally as we push toward the unification of effectful programming with object-oriented programming. We pin down the mechanism and the unification formally using a core language that generalizes to effect operations and effect handlers. The usual propagation semantics of control effects such as exceptions conflicts with modular reasoning in the presence of effect polymorphism---it breaks parametricity. Bidirectionality exacerbates the problem. Hence, we set out to show the core language, which builds on the existing tunneling semantics for algebraic effects, is not only type-safe (no effects go unhandled), but also abstraction-safe (no effects are accidentally handled). We devise a step-indexed logical-relations model, and construct its parametricity and soundness proofs. These core results are fully mechanized in Coq. Preliminary experiments show that as a first-class language feature, bidirectional handlers can be implemented efficiently.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
