Effect Handlers in Scope
📜 Abstract
Algebraic effect handlers are a powerful means for describing effectful computations. They provide a lightweight and orthogonal technique to define and compose the syntax and semantics of different effects. The semantics is captured by handlers, which are functions that transform syntax trees. Unfortunately, the approach does not support syntax for scoping constructs, which arise in a number of scenarios. While handlers can be used to provide a limited form of scope, we demonstrate that this approach constrains the possible interactions of effects and rules out some desired semantics. This paper presents two different ways to capture scoped constructs in syntax, and shows how to achieve different semantics by reordering handlers. The first approach expresses scopes using the existing algebraic handlers framework, but has some limitations. The problem is fully solved in the second approach where we introduce higher-order syntax.
✨ Summary
The paper identifies a modularity problem in algebraic effect handlers: when handlers both define effect semantics and delimit effect scope, changing handler order can alter scopes as well as effect interactions. The authors demonstrate this problem using nondeterministic pruning, parsing, exception handling, and cooperative multi-threading. They propose two solutions: first-order scope markers, which encode scope boundaries as syntax, and higher-order syntax, which embeds scoped computations and their continuations directly in effect signatures. Higher-order syntax is more expressive and supports cases such as forking, where first-order syntax cannot correctly distinguish a child computation from the parent continuation. The paper shows that handler reordering can then provide alternative, useful interpretations, such as local versus shared state, without changing the syntactic scope.
The work became an early reference point for scoped effects. Later research explicitly characterizes scoped-effect semantics as separating the scope of an operation from the code that interprets it, and identifies this paper as the first work to study native support for scoped operations in Haskell. (pls-lab.org) Its higher-order-effect approach also influenced practical Haskell libraries: the fused-effects project states that its higher-order algebraic-effects encoding follows the recipes of this paper and uses the resulting separation to support scoped operations such as local and catchError. (github.com) Subsequent work investigated efficient implementations, including SpEff, which adapts evidence-passing techniques to support scoped effects, and formal developments such as structured handling of scoped effects and parameterized algebraic theories. (icfp22.sigplan.org)