Sparkles

Appearance

Theory and Compilation of Algebraic Effects ​

A synthesis of how algebraic effects relate to established abstractions, how they are typed, and how they are compiled to efficient code across languages and runtimes.

Algebraic Effects vs. Monads ​

Moggi (1991) proposed monads as a uniform representation of computational effects: computations returning values of type A are elements of T A for a suitable monad T. Plotkin and Power (2001-2003) refined this by observing that many monads of interest arise as free models of algebraic theories -- that is, they are generated by a signature of operations and equational laws. Exceptions, mutable state, nondeterminism, and interactive I/O are all algebraic in this sense. The notable exception is continuations: the continuation monad is not generated by any algebraic theory.

This gives the central correspondence: algebraic effects correspond to free monads. An effect signature (a set of operations with arities) freely generates a monad whose elements are syntax trees of operations. A handler interprets these trees by providing a model of the algebra -- concretely, by folding over the tree with a case for each operation.

Why Monads Do Not Compose ​

Given two monads S and T, the composition S . T is not in general a monad. Monad transformers address this by defining, for each monad T, a transformer T' that can wrap an arbitrary inner monad M to produce T' M. However:

  1. O(n^2) boilerplate: Each new transformer must define how it interacts with every existing transformer (the "n^2 instance problem" in Haskell's mtl).
  2. Order dependence: StateT s (ExceptT e m) and ExceptT e (StateT s m) have different semantics -- the transformer stack encodes operational choices implicitly.
  3. Lifting overhead: Operations must be lifted through each layer; each monadic bind traverses the full stack.

Algebraic effects compose freely because union of effect signatures is just union of operation sets. No transformer machinery is needed: handlers are composed by nesting, and the order of nesting makes the operational semantics explicit rather than implicit.

When Monads Are Still Preferable ​

Monads provide equational laws (e.g., the state monad laws guarantee that get after put v yields v) that constrain implementations. Free monads, by contrast, admit any handler -- including ones that violate expected invariants. When strong behavioral contracts matter more than composability, lawful monads and typeclasses remain valuable. The paper "Monad Transformers and Modular Algebraic Effects: What Binds Them Together" (Schrijvers, Pirog, Wu, Jaskelioff, Haskell 2019) formally establishes that modular algebraic effects and a specific subclass of monad transformers are equivalent in expressiveness.

Evidence Passing ​

The paper "Effect Handlers, Evidently" (Xie, Brachthaeuser, Hillerstroemm, Schuster, Leijen, ICFP 2020) introduced evidence-passing semantics for algebraic effect handlers. The core idea is to compile away the runtime search for a handler by threading evidence -- a proof that a handler exists -- directly to each operation call. This technique is used by effectful, cleff, and Koka.

Evidence Vectors ​

In the evidence-passing translation, every effectful function receives an additional parameter: an evidence vector w mapping effect labels to evidence triples (m, h, w'), where:

  • m is a marker identifying the prompt (handler boundary) on the stack
  • h is the handler itself (the collection of operation clauses)
  • w' is the evidence vector that was in scope when h was installed

When an operation is invoked, it indexes into the evidence vector to find the handler directly -- no stack walking or dynamic search required. This gives O(1) dispatch for effect operations.

Scoped Resumptions ​

The original evidence-passing translation requires scoped resumptions: when a handler resumes a captured continuation, the resumed computation runs under the same set of handlers it had before being suspended. This rules out "non-scoped" uses where a resumption is invoked under a different handler configuration, which the authors argue is undesirable in practice because it breaks local reasoning about effects.

The effectful Library ​

Haskell's effectful library applies a pragmatic version of evidence passing. Its Eff monad is essentially ReaderT Env IO, where Env is a mutable environment indexed by Int-based offsets. Looking up a handler is an O(1) array index operation. The :> constraint carries evidence that an effect exists in the environment. This design achieves performance on par with hand-written ST code for static dispatch and outperforms mtl for dynamic dispatch.

Generalized Evidence Passing ​

The follow-up paper "Generalized Evidence Passing for Effect Handlers" (Xie, Leijen, ICFP 2021) extends the approach to handle all algebraic effect programs, not just those with scoped resumptions. It introduces yield bubbling: when an operation needs to capture a continuation, it yields a "bubble" (like an exception) that propagates up to the handler, which then captures the delimited continuation. The paper presents a complete compilation pipeline: algebraic effects to multi-prompt delimited control to generalized evidence passing to yield bubbling to a monadic translation in plain lambda calculus.

Capability Passing ​

An alternative framing views effects not as labels in a type-level row but as capabilities: values that grant permission to perform operations. A function can only perform an effect if it holds a handle to the corresponding capability. This connects to the object-capability security model, where authority is determined by which references are in scope.

Bluefin (Haskell) ​

Bluefin represents effects as value-level handles rather than type-level labels. Each handle is scoped using a mechanism similar to Haskell's ST trick: the handle cannot escape the lexical scope of its handler. Having two State Int effects in scope is trivial because they are distinct values, whereas type-level approaches require awkward disambiguation. The bluefin-algae extension adds algebraic effects on top of this design using GHC's delimited continuation primops.

[Scala 3 Capture Checking] ​

Scala 3 introduces capture checking as an experimental feature that tracks which capabilities a value captures through the type system. Rather than adding a separate effect row, it extends the existing type system: a closure type A -> B becomes A ->{c1, c2} B indicating that the closure captures capabilities c1 and c2. Effect polymorphism emerges naturally -- map is classified as pure because it does not use capabilities itself, but its type propagates the capabilities of whatever function argument is passed to it. Minimal annotations are needed for strict code; they only become necessary for delayed effects (lazy lists, side-effecting iterators).

[OCaml Eio] ​

Eio, the effects-based direct-style IO library for OCaml 5, adopts an object-capability model. All authority originates at Eio_main.run, which receives an env value containing capabilities for the network, filesystem, clock, and so on. Functions receive only the capabilities they need. For example, a function that only takes a net capability visibly cannot access the filesystem. Since OCaml is not a pure capability language, code can bypass Eio and use the stdlib directly, but the design still aids auditing and testing of non-malicious code.

Benefits of Capability Passing ​

  • Scoping is explicit: A capability's lifetime is bounded by its lexical scope.
  • Disambiguation is trivial: Two effects of the same type are two different values.
  • Auditing is local: You can determine a function's effects by examining its parameters.
  • Testing is straightforward: Pass mock capabilities to test effectful code.

Type-and-Effect Systems ​

A type-and-effect system extends a standard type system to track not only the types of expressions but also their computational effects. The design of the effect type language has significant consequences for usability and expressiveness.

Koka and Links represent effect types as rows -- extensible sequences of effect labels. A function type carries its effect row: (a) -> e b means "given a, produces b with effects e." Row polymorphism allows abstracting over unknown effects:

koka
fun map(xs : list<a>, f : (a) -> e b) : e list<b>

Here e is a polymorphic effect variable: map is agnostic to what effects f performs. Duplicate labels are permitted, and type inference follows Hindley-Milner-style algorithms. This avoids the undecidability issues that arise when combining polymorphism with subtyping.

Set-Based Effect Types ​

An alternative is to treat effect types as sets. Java's checked exceptions are the most widely deployed example of a set-based effect type system -- and serve as a cautionary tale. Key problems:

  • Cascading signatures: Adding a new exception to a low-level method forces changes to every caller in the chain.
  • Incompatibility with abstraction: An interface cannot anticipate which exceptions its implementations will throw.
  • Incompatibility with higher-order functions: Lambda expressions in Java cannot throw checked exceptions through functional interfaces like java.util.Function.
  • Swallowed exceptions: Developers routinely catch and discard exceptions to satisfy the compiler.

Every major JVM language after Java (Scala, Kotlin, Groovy, Clojure) declined to adopt checked exceptions.

Subeffecting and Effect Coercion ​

Subeffecting is a subtyping-like relation on effects: a pure computation can be used where a stateful one is expected. In an intermediate language, these promotions can be made explicit as coercions that witness the subeffecting proof. The paper "Explicit Effect Subtyping" (Koprivec, Pretnar) shows how to reify subtyping appeals as explicit casts, and proposes algorithms that soundly reduce redundant coercion parameters to achieve performance comparable to monomorphic code.

Effect Inference ​

Many effect systems infer effects automatically. Koka infers full effect types without programmer annotations. The challenge intensifies with higher-rank polymorphism and subeffecting: the recent paper "Deciding not to Decide: Sound and Complete Effect Inference" (2025) addresses these interactions by delaying constraint solving and reducing effect constraints to propositional logic.

Untyped Effects (OCaml 5) ​

OCaml 5 introduced algebraic effects without typing them -- effects are not tracked in function signatures. This was a pragmatic decision: the delta for OCaml 5 was already large (multicore GC plus effects), and typed effects will be introduced in a future release. The trade-off is clear: untyped effects provide the runtime benefits (structured concurrency, direct-style IO, no monadic overhead) without the static safety guarantees. An unhandled effect is a runtime error, not a compile-time one.

Compilation Strategies ​

Compiling algebraic effects efficiently is challenging because effect handlers capture delimited continuations -- slices of the execution context that can be suspended and resumed. Different strategies make different trade-offs between generality, performance, and implementation complexity. See WasmFX for a cross-language compilation target for effect handlers.

CPS Transformation ​

Convert the entire program (or the effectful parts) to continuation-passing style. Each function takes an extra argument representing "what to do next," making continuations explicit and capturable as ordinary closures.

  • Pros: Works on any target platform; no special runtime support needed.
  • Cons: Whole-program CPS inflates code size and disables many optimizations; all calls become tail calls through closures, defeating inlining.

Monadic Translation ​

Compile effectful code into a target-language monad. Each effectful operation returns a monadic value (Pure v or Yield op k), and binds sequence them.

  • Pros: Portable; works with any lambda-calculus target.
  • Cons: Monadic binds introduce allocation; every intermediate result is wrapped.

Evidence Passing ​

Thread evidence vectors through effectful code. Operations index into the vector for O(1) handler lookup. Combine with a monadic translation only for operations that actually need to capture continuations.

  • Pros: Fast path for tail-resumptive operations (no allocation); O(1) dispatch.
  • Cons: Requires a type-directed compilation phase; more complex compiler infrastructure.

Direct Stack Manipulation ​

Capture and restore actual stack frames at runtime. The program runs on segmented stacks (fibers), and performing an effect pops fiber frames to create a continuation object.

  • Pros: Zero overhead on the fast path (no CPS, no monadic wrapping); natural call conventions preserved.
  • Cons: Requires runtime support (GHC primops, OCaml fiber runtime, WasmFX instructions); platform-specific.

Selective CPS ​

Only CPS-transform functions whose types indicate they may capture continuations. Functions that are total or only use tail-resumptive effects remain in direct style.

  • Pros: Minimizes code expansion (in Koka, less than 20% of core library functions need CPS); preserves tail calls for pure code.
  • Cons: Requires type-directed analysis; polymorphic effect variables need special handling (code duplication to pick the correct runtime representation).

Bubble Semantics (Yield Bubbling) ​

When an operation needs to capture a continuation, it sets a thread-local flag and returns a sentinel "yield" value that propagates up through monadic binds until it reaches the handler. The handler then captures the continuation.

  • Pros: Avoids special runtime support for continuation capture; the fast (pure) path checks a single flag and avoids allocation.
  • Cons: Every monadic bind must check the yield flag; conceptually complex.

Comparison ​

StrategyLanguages / LibrariesPerformanceContinuation SupportComplexity
CPS transformationLinks (JS backend)Moderate; code bloat from full CPSFull multi-shotLow (well-understood transform)
Monadic translationEff (original), Haskell free/freerSlow; allocation per bindFull multi-shotLow
Evidence passingeffectful, Ev.Eff, Koka (partial)Fast; O(1) dispatch, zero-alloc tail-resumptiveOne-shot (scoped)Medium (type-directed)
Direct stack manipulationOCaml 5 fibers, GHC primops, WasmFXFastest; native call conventionsOne-shot (OCaml), multi-shot (GHC)High (runtime support)
Selective CPSKoka (C backend)Fast; direct style on pure pathsFull (via CPS'd paths)Medium (type-directed code duplication)
Bubble semantics / yieldKoka (generalized), Mp.EffFast; flag check on pure pathFull one-shotMedium-high

Evidence Passing Semantics: A Deeper Dive ​

The evidence-passing compilation pipeline deserves closer examination because it reveals a spectrum of optimization opportunities depending on the structure of effect operations.

Tail-Resumptive Operations ​

An operation is tail-resumptive if its handler clause resumes the continuation in tail position and does nothing afterward. The canonical examples are State operations:

text
get ()  -> resume(s)          -- returns the state and resumes
put(s') -> resume(())         -- updates the state and resumes

In both cases the handler immediately resumes with a value. There is no need to capture the continuation at all -- the operation can execute in place, like a regular function call into the handler. The handler reads or writes its state and returns; the calling code never knows a "context switch" happened.

Why Tail Resumptions Avoid Continuation Capture ​

When an operation resumes in tail position, the stack frame layout before and after the operation is identical. Nothing needs to be saved. The evidence-passing translation exploits this: for a tail-resumptive operation, the generated code calls the handler function directly (found via the evidence vector at a known offset) and uses its return value as the operation's result. No yield, no bubble, no continuation object.

In Leijen's C implementation of algebraic effects, this optimization yields an order-of-magnitude improvement: up to 150 million tail-resumptive operations per second, compared to roughly 10 million operations requiring full continuation capture.

The Optimization Spectrum ​

Real effect systems exist on a spectrum from pure evidence passing (no continuation capture at all) to full delimited control:

Operation KindExampleContinuation CaptureEvidence Passing Optimization
Tail-resumptiveState.get, State.putNoneDirect function call via evidence
Scoped resumptionReader.localDelimited, one-shotYield bubble; resume under same handlers
General resumptionNonDet.chooseDelimited, potentially multi-shotFull continuation capture required
No resumptionException.throwNone (abort)Unwind stack to handler

In practice, the vast majority of effect operations in real programs are tail-resumptive. Leijen reports that almost all effects use either tail resumptions or resumptions that stay within the scope of the handler. This makes evidence passing an extremely effective optimization: the common case is fast, and the rare case (full continuation capture) falls back to a general mechanism.

Effect-Selective Monadic Translation ​

Koka's compiler combines evidence passing with a type-selective monadic translation: functions whose effect type is total (no effects) are compiled without monadic wrapping at all. Functions that use only tail-resumptive effects get evidence-passing dispatch but no monadic overhead. Only functions that may perform general (non-tail-resumptive) operations are compiled monadically. This ensures the fast path -- the overwhelmingly common path -- incurs no allocation.

Sources ​