Reference. Effect handlers via generalised continuations
Plotkin and Pretnar’s effect handlers offer a versatile abstraction for modular programming with user-defined effects. This paper focuses on foundations for implementing effect handlers, for the three different kinds of effect handlers that have been proposed in the literature: deep, shallow, and parameterised. Traditional deep handlers are defined by folds over computation trees and are the original construct proposed by Plotkin and Pretnar. Shallow handlers are defined by case splits (rather than folds) over computation trees. Parameterised handlers are deep handlers extended with a state value that is threaded through the folds over computation trees. We formulate the extensions both directly and via encodings in terms of deep handlers and illustrate how the direct implementations avoid the generation of unnecessary closures. We give two distinct foundational implementations of all the kinds of handlers we consider: a continuation-passing style (CPS) transformation and a CEK-style abstract machine. In both cases, the key ingredient is a generalisation of the notion of continuation to accommodate stacks of effect handlers. We obtain our CPS translation through a series of refinements as follows. We begin with a first-order CPS translation into untyped lambda calculus which manages a stack of continuations and handlers as a curried sequence of arguments. We then refine the initial CPS translation by uncurrying it to yield a properly tail-recursive translation and then moving towards more and more intensional representations of continuations in order to support different kinds of effect handlers. Finally, we make the translation higher order in order to contract administrative redexes at translation time. Our abstract machine design then uses the same generalised continuation representation as the CPS translation. We have implemented both the abstract machine and the CPS transformation (plus extensions) as backends for the Links web programming language.
Cite
Cited by (2)
Yarrow: Reconciling Effect Handlers and Region-Based Memory Management mathiasen-2026-yarrow
We present a new ML-like programming language Yarrow with algebraic effects and region-based memory management. Reconciling these programming language features into one language is challenging: the non-local control flow of algebraic effects break the stack discipline of function calls and returns that region-based memory management relies on, and multi-shot effect handlers break the invariant that regions can be exited at most once. We present a program logic, called Yarrow Logic (YL), that supports safe and modular reasoning about regions in the presence of one-shot and multi-shot effect handlers. We prove the logic sound w.r.t. the operational semantics of Yarrow which is inspired by the runtime of OCaml but refined for regions. We use YL to prove correctness of a number of case studies with algebraic effects, including checkpointing, asynchronous computation and a LIFO data structure implementation. Since all memory locations used in these case studies are allocated in regions, these case studies avoid using the less efficient garbage collected heap memory. We have formalized Yarrow’s operational semantics, the Yarrow program logic, and all our case studies using the Iris separation logic framework on top of the Rocq Prover.
Doo bee doo bee doo convent-2020-doo
We explore the design and implementation of Frank, a strict functional programming language with a bidirectional effect type system designed from the ground up around a novel variant of Plotkin and Pretnar’s effect handler abstraction. Effect handlers provide an abstraction for modular effectful programming: a handler acts as an interpreter for a collection of commands whose interfaces are statically tracked by the type system. However, Frank eliminates the need for an additional effect handling construct by generalising the basic mechanism of functional abstraction itself. A function is but the special case of a Frank operator that interprets no commands. Moreover, Frank’s operators can be multihandlers which simultaneously interpret commands from several sources at once, without disturbing the direct style of functional programming with values. Effect typing in Frank employs a novel form of effect polymorphism which avoids mentioning effect variables in source code. This is achieved by propagating an ambient ability inwards, rather than accumulating unions of potential effects outwards. With the ambient ability describing the effects that are available at a certain point in the code, it can become necessary to reconfigure access to the ambient ability. A primary goal is to be able to encapsulate internal effects, eliminating a phenomenon we call effect pollution . Moreover, it is sometimes desirable to rewire the effect flow between effectful library components. We propose adaptors as a means for supporting both effect encapsulation and more general rewiring. Programming with effects and handlers is in its infancy. We contribute an exploration of future possibilities, particularly in combination with other forms of rich type systems.
Cites 57 works (5 here)
With notes (5)
Doo bee doo bee doo convent-2020-doo
We explore the design and implementation of Frank, a strict functional programming language with a bidirectional effect type system designed from the ground up around a novel variant of Plotkin and Pretnar’s effect handler abstraction. Effect handlers provide an abstraction for modular effectful programming: a handler acts as an interpreter for a collection of commands whose interfaces are statically tracked by the type system. However, Frank eliminates the need for an additional effect handling construct by generalising the basic mechanism of functional abstraction itself. A function is but the special case of a Frank operator that interprets no commands. Moreover, Frank’s operators can be multihandlers which simultaneously interpret commands from several sources at once, without disturbing the direct style of functional programming with values. Effect typing in Frank employs a novel form of effect polymorphism which avoids mentioning effect variables in source code. This is achieved by propagating an ambient ability inwards, rather than accumulating unions of potential effects outwards. With the ambient ability describing the effects that are available at a certain point in the code, it can become necessary to reconfigure access to the ambient ability. A primary goal is to be able to encapsulate internal effects, eliminating a phenomenon we call effect pollution . Moreover, it is sometimes desirable to rewire the effect flow between effectful library components. We propose adaptors as a means for supporting both effect encapsulation and more general rewiring. Programming with effects and handlers is in its infancy. We contribute an exploration of future possibilities, particularly in combination with other forms of rich type systems.
On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control forster-2019-on
We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar’s effect handlers, Filinski’s monadic reflection, and delimited control. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features. We present three calculi, one per abstraction, extending Levy’s call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic metatheoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen’s notion of a macro translation, we show that these abstractions can macro express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro expressed while preserving typeability either by monadic reflection or by delimited control. Our argument fails with simple changes to the type system such as polymorphism and inductive types. We supplement our development with a mechanised Abella formalisation.
Do be do be do lindley-2017-do
Continuation Passing Style for Effect Handlers hillerstrom-2017-continuation
We present Continuation Passing Style (CPS) translations for Plotkin and Pretnar’s effect handlers with Hillerström and Lindley’s row-typed fine-grain call-by-value calculus of effect handlers as the source language. CPS translations of handlers are interesting theoretically, to explain the semantics of handlers, and also offer a practical implementation technique that does not require special support in the target language’s runtime.
We begin with a first-order CPS translation into untyped lambda calculus which manages a stack of continuations and handlers as a curried sequence of arguments. We then refine the initial CPS translation first by uncurrying it to yield a properly tail-recursive translation and second by making it higher-order in order to contract administrative redexes at translation time. We prove that the higher-order CPS translation simulates effect handler reduction. We have implemented the higher-order CPS translation as a JavaScript backend for the Links programming language.
Handlers in action kammar-2013-handlers
External (52)
- Abstracting algebraic effects (2019)
- Typed equivalence of effect handlers and delimited control (2019)
- Handle with care: Relational interpretation of algebraic effects and handlers (2018)
- Effect handlers for the masses (2018)
- Pyro: Deep Universal Probabilistic Programming (2018)
- Shallow effect handlers (2018)
- Staged generic programming (2017)
- Concurrent system programming with effect handlers (2017)
- Implementing algebraic effects in C - “monads for free in C” (2017)
- On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control (2017)
- MSc(R) thesis (2016)
- Compiling Links effect handlers to the OCaml backend (2016)
- Eff directly in OCaml (2016)
- Fusion for free - efficient algebraic effect handlers (2015)
- Programming with algebraic effects and handlers (2015)
- Effective concurrency through algebraic effects (2015)
- Handlers for algebraic effects in Links (2015)
- In APLAS. LNCS (2012)
- Yield: Mainstream delimited continuations (2011)
- A monadic framework for delimited continuations (2007)
- In FMCO. LNCS (2006)
- In FoSSaCS. LNCS (2001)
- Monads for functional programming (1995)
- Syntactic theories and the algebra of record terms (1993)
- Compiling with Continuations (1992)
- Functional programming with bananas, lenses, envelopes and barbed wire (1991)
- Tupling and mutumorphisms (1990)
- Control operators, the SECD-machine, and the λ-calculus (1986)
- RABBIT: A compiler for SCHEME (1978)
- 10.1145/2633357.2633358
- 10.1016/j.entcs.2015.12.003
- 10.2168/lmcs-9(4:23)2013
- 10.1145/155090.155113
- 10.2307/1967631
- 10.1016/s0304-3975(02)00733-8
- 10.1145/91556.91622
- 10.1007/s10990-007-9010-4
- 10.1145/13310.13333
- 10.1145/3122975.3122977
- 10.1023/a:1020891112409
- 10.4204/eptcs.153.8
- 10.1016/0304-3975(75)90017-1
- 10.1017/s0956796820000027
- 10.1145/231379.231395
- 10.1145/2976022.2976033
- 10.1145/1291151.1291179
- 10.1017/s0960129500001535
- 10.1016/j.tcs.2012.02.025
- 10.1145/3136000.3136007
- 10.1016/s0890-5401(03)00088-9
- 10.1145/3093333.3009872
- 10.1017/s0956796897002864