Algebraic effects & handlers have become a standard approach for side-effects in functional programming. Their modular composition with other effects and clean separation of syntax and semantics make them attractive to a wide audience. However, not all effects can be classified as algebraic; some need a more sophisticated handling. In particular, effects that have or create a delimited scope need special care, as their continuation consists of two parts-in and out of the scope-and their modular composition introduces additional complexity. These effects are called scoped and have gained attention by their growing applicability and adoption in popular libraries. While calculi have been designed with algebraic effects & handlers built in to facilitate their use, a calculus that supports scoped effects & handlers in a similar manner does not yet exist. This work fills this gap: we present $\lambda_{\mathit{sc}}$, a calculus with native support for both algebraic and scoped effects & handlers. It addresses the need for polymorphic handlers and explicit clauses for forwarding unknown scoped operations to other handlers. Our calculus is based on Eff, an existing calculus for algebraic effects, extended with Koka-style row polymorphism, and consists of a formal grammar, operational semantics, a (type-safe) type-and-effect system and type inference. We demonstrate $\lambda_{\mathit{sc}}$ on a range of examples.
翻译:代数效应与处理子已成为函数式编程中处理副作用的标准方法。它们与其他效应的模块化组合,以及语法与语义的清晰分离,吸引了广泛受众。然而,并非所有效应都能归类为代数效应;部分效应需要更复杂的处理。特别是那些具有或创建了定界作用域的效应需要特殊关注,因为其续体包含作用域内与作用域外两个部分,且它们的模块化组合会引入额外复杂性。这类效应被称为作用域化效应,并因其在主流库中日益增长的适用性和采纳度而备受关注。尽管已有针对代数效应与处理子内置支持的演算设计用于促进其使用,但尚无类似方式支持作用域化效应与处理子的演算存在。本文填补了这一空白:我们提出了$\lambda_{\mathit{sc}}$,一个原生支持代数效应和作用域化效应与处理子的演算。它解决了多态处理子及显式子句转发未知作用域化操作至其他处理子的需求。我们的演算基于Eff(现有代数效应演算),扩展了Koka风格的行多态性,并包含形式化语法、操作语义、(类型安全的)类型与效应系统及类型推断。我们通过一系列示例展示了$\lambda_{\mathit{sc}}$的能力。