一句话：将作用域效应翻译为参数化代数理论的变体，给出等式推理与用生成元和方程刻画 monad 的新方法。
代数效应通过代数操作与等式公理刻画 monad，但定界作用域、动态分配资源等编程特性需要作用域效应等扩展。本文提出一种新视角：将作用域效应翻译为参数化代数理论的一种变体。该翻译为作用域效应提供了新的等式推理方法，并给出一种替代性的 monad 刻画，其生成元和方程同时涉及作用域操作与代数操作。作者通过对若干已知作用域效应模型给出等式刻画，展示了该方法的表达力。
Notions of computation can be modeled by monads. Algebraic effects offer a characterization of monads in terms of algebraic operations and equational axioms, where operations are basic programming features, such as reading or updating the state, and axioms specify observably equivalent expressions. However, many useful programming features depend on additional mechanisms such as delimited scopes or dynamically allocated resources. Such mechanisms can be supported via extensions to algebraic effects including scoped effects and parameterized algebraic theories . We present a fresh perspective on scoped effects by translation into a variation of parameterized algebraic theories. The translation enables a new approach to equational reasoning for scoped effects and gives rise to an alternative characterization of monads in terms of generators and equations involving both scoped and algebraic operations. We demonstrate the power of our approach by way of equational characterizations of several known models of scoped effects.
@article{MatacheLMSWY25,
title = {Scoped Effects, Scoped Operations, and Parameterized Algebraic Theories},
author = {Cristina Matache and Sam Lindley and Sean Moss and Sam Staton and Nicolas Wu and Zhixuan Yang},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {47},
number = {2},
year = {2025},
doi = {10.1145/3731678}
}