作用域效应作为参数化代数理论
Scoped Effects as Parameterized Algebraic Theories
AI总结：
本文将 scoped effects 翻译为 parameterized algebraic theories 的变体，为其等式推理和 monad 刻画提供新框架，并通过多个已知模型验证该方法。
摘要：
计算概念可以通过 monad 来建模。代数效应依据代数操作和等式公理给出 monad 的刻画，其中操作是基本编程特性，例如读取或更新状态，而公理则规定可观察上等价的表达式。然而，许多有用的编程特性依赖额外机制，如分隔作用域或动态分配的资源。这类机制可以通过对代数效应的扩展来支持，包括 scoped effects（作用域效应）和 parameterized algebraic theories（参数化代数理论）。我们通过将 scoped effects 翻译为一种 parameterized algebraic theories 的变体，提出了关于 scoped effects 的全新视角。该翻译为 scoped effects 的等式推理提供了一种新方法，并依据同时涉及作用域操作和代数操作的生成子与方程，给出了 monad 的另一种刻画。我们通过对若干已知 scoped effects 模型进行等式刻画，展示了这一新视角的能力。
英文摘要：
Notions of computation can be modelled 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 fresh perspective by way of equational characterizations of several known models of scoped effects.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
