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.
翻译:计算概念可以通过单子来建模。代数效应利用代数操作和等式公理刻画单子,其中操作是基本编程特性(如读取或更新状态),公理则指定可观察上等价的表达式。然而,许多实用的编程特性依赖于额外机制,例如限定作用域或动态分配资源。此类机制可通过代数效应的扩展(包括作用域效应和参数化代数理论)得到支持。我们通过将作用域效应转化为参数化代数理论的变体,提出一种全新视角。该转化为作用域效应的等式推理提供了新方法,并基于生成元及涉及作用域操作与代数操作的等式,给出单子的另一种刻画。我们通过若干已知作用域效应模型的等式特征化,展示了这一新视角的强大能力。