论用户自定义效果的表现力：效果处理程序，一元反射，分隔控制
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control
摘要：
我们比较了三个编程抽象的表达能力，用户定义的计算效果：鲍尔和Pretnar的效果处理程序，Filinski的一元反射，并分隔控制没有答案类型修改。这种比较允许对每种编程抽象的相对表达性进行精确的讨论。它还展示了用户定义的效果的相对表现力对看似正交的语言特征的敏感性。我们提出了三个演算，每个抽象，扩展利维的呼叫推值。对于每一个演算，我们提出的语法，操作语义，一个自然的类型和效果系统，效果处理程序和一元反射，一套理论的指称语义。我们建立其基本的元理论属性：安全性，终止性，并在适用的情况下，健全性和充分性。使用Felleisen的宏观翻译的概念，我们表明，这些抽象可以宏观表达对方，并显示哪些翻译保持可输入性。我们使用足够的有限集合理论的指称语义的一元演算，效果处理程序不能宏表示，同时保留类型由一元反射或分隔控制。我们补充我们的发展与机械化阿贝拉正规化。
英文摘要：
We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answer-type-modification. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features. We present three calculi, one per abstraction, extending Levy's call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic meta-theoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen's notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. We supplement our development with a mechanised Abella formalisation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
