7 min read
On this page

Effect Systems

Motivation

Pure functions are referentially transparent: replacing f(x) with its result preserves program meaning. Effects (mutation, I/O, exceptions, nondeterminism, concurrency) break this property. Effect systems track which effects a computation may perform, enabling reasoning about purity and effect interactions.

The central question: how to integrate effects into typed functional programming while preserving compositionality and type safety.

Monadic Effects

Monads for Effects (Moggi, 1989; Wadler, 1992)

A monad (T, return, bind) encapsulates effectful computation:

return : A -> T A
bind   : T A -> (A -> T B) -> T B   (written >>= in Haskell)

Monad laws:

  1. Left identity: return a >>= f = f a
  2. Right identity: m >>= return = m
  3. Associativity: (m >>= f) >>= g = m >>= (lambda x. f x >>= g)

Common Effect Monads

| Effect | Monad T A | return a | m >>= f | |---|---|---|---| | Partiality | Maybe A | Just a | case m of Nothing -> Nothing; Just x -> f x | | Exceptions | Either E A | Right a | case m of Left e -> Left e; Right x -> f x | | State | S -> (A, S) | lambda s. (a, s) | lambda s. let (x, s') = m s in f x s' | | Nondeterminism | [A] (list) | [a] | concatMap f m | | I/O | IO A | -- (primitive) | -- (primitive) | | Reader | R -> A | lambda r. a | lambda r. f (m r) r | | Writer | (A, W) | (a, mempty) | let (x, w) = m in let (y, w') = f x in (y, w <> w') | | Continuation | (A -> R) -> R | lambda k. k a | lambda k. m (lambda x. f x k) |

Limitations of Monads

  1. Monad composition: Monads do not compose generically. StateT s (Either e) works, but ListT (IO) does not satisfy the monad laws. Monad transformers provide ad-hoc composition but require specific lift operations.

  2. Effect ordering: Monad transformer stacks impose a fixed effect ordering. StateT s (Either e) and ExceptT e (State s) have different semantics (does state roll back on exception?).

  3. Performance: Deep monad transformer stacks incur overhead. CPS transformation and specialization help but complicate the code.

Algebraic Effects and Handlers

Algebraic Effects (Plotkin-Power, 2003)

An algebraic effect is an interface of operations with specified arities:

effect State S where
  get : () -> S
  put : S -> ()

effect Exception E where
  raise : E -> Empty    -- never returns normally

effect Nondeterminism where
  choose : () -> Bool

Operations are algebraic in that they satisfy equational theories. For State: get followed by put s is equivalent to put s. The equations constrain handler implementations.

Effect Handlers (Plotkin-Pretnar, 2009)

An effect handler gives semantics to operations by defining how each operation is interpreted:

handle (computation) with
  | return x    -> ...            -- pure result
  | get () k    -> ...k(s)...     -- k is the continuation
  | put s' k    -> ...k(())...    -- resume with ()

The handler receives the operation and a delimited continuation k representing "the rest of the computation." The handler can:

  • Resume the continuation (once, multiple times, or never)
  • Transform the result
  • Thread state through the continuation

Example: State Handler

handler stateHandler (init : S) =
  | return x     -> lambda s. x
  | get () k     -> lambda s. (k s) s        -- pass current state to continuation
  | put s' k     -> lambda s. (k ()) s'      -- update state

Running: stateHandler 0 (do put 5; x <- get; return (x + 1)) evaluates to 6.

Example: Nondeterminism Handler (Collect All Results)

handler allResults =
  | return x      -> [x]
  | choose () k   -> (k true) ++ (k false)   -- resume BOTH ways

This calls the continuation twice, collecting all possible results. The ability to invoke k multiple times is what distinguishes handlers from exception handlers.

Effect Polymorphism

Effect polymorphism abstracts over the effects a function may perform:

map : forall a b. forall e. (a -> e b) -> List a -> e List b

Here e is an effect variable. map works with any effectful function without knowing which effects are involved.

Row-Based Effect Systems

Effects are tracked as rows (sets of operation labels):

f : Int -> <State Int, Exception String | e> Int

This says f performs State and Exception effects, plus possibly more effects captured by the effect variable e. The row variable e enables polymorphism.

Row polymorphism (Remy, 1994; adapted for effects by Leijen, 2005):

  • Rows are unordered collections of labels
  • Row variables capture "the rest of the effects"
  • Effect subsumption: <State | e> is a subtype of <State, IO | e>

Effect Inference

Many effect systems support partial or full inference of effect annotations. The programmer writes effectful code; the compiler infers which effects are performed and checks that all effects are handled.

Languages with Algebraic Effects

Koka (Leijen, 2014-)

Koka is a research language designed around algebraic effects:

  • Row-polymorphic effect types
  • Handlers as first-class values
  • Effect inference (programmer rarely writes effect annotations)
  • Perceus reference counting (effect handlers interact with memory management)
effect ask<a>
  ctl ask() : a

fun greeting() : ask<string> string
  val name = ask()
  "Hello, " ++ name

fun main()
  with handler
    ctl ask() resume("Alice")
  greeting().println

Eff (Bauer-Pretnar, 2012)

Eff pioneered the handler-based approach:

  • First-class effects and handlers
  • Type-and-effect system
  • Clean theoretical semantics

Frank (Lindley-McBride-McLaughlin, 2017)

Frank integrates effects directly into the type system via multi-handlers:

  • Handlers are just functions that pattern-match on effectful computations
  • No syntactic distinction between handling and calling
  • "Do be do be do" -- effectful and pure computations interleave naturally

OCaml 5

OCaml 5 added algebraic effects (via Effect.Deep and Effect.Shallow modules) using one-shot continuations. Effects are used for:

  • Cooperative concurrency (fibers)
  • Async I/O
  • Custom schedulers

Delimited Continuations

Effect handlers are closely related to delimited continuations (Felleisen, 1988; Danvy-Filinski, 1990):

  • shift/reset: reset (... shift k. M ...) captures the continuation up to the nearest reset and binds it to k in M.
  • prompt/control: Similar, but control does not include the delimiter in the captured continuation.

An effect handler handle ... with {op k -> ...} is essentially:

  • handle establishes a delimiter (like reset)
  • Performing an operation captures the continuation to the handler (like shift)
  • The handler body decides what to do with the continuation

Theorem (Forster-Kammar-Lindley-Pretnar, 2019): Algebraic effects with handlers and delimited continuations (shift/reset) are macro-expressible in terms of each other.

One-Shot vs Multi-Shot Continuations

  • One-shot: Continuation invoked at most once. More efficient (no copying). Sufficient for exceptions, state, coroutines.
  • Multi-shot: Continuation can be invoked multiple times. Required for nondeterminism, backtracking. Requires copying the continuation (expensive).

OCaml 5 supports only one-shot continuations for performance. Multicore OCaml uses them for fiber-based concurrency.

Free Monads

Free monads provide an alternative encoding of algebraic effects in languages without native handler support:

data Free f a = Pure a | Free (f (Free f a))

-- For State:
data StateF s next = Get (s -> next) | Put s next

type StateFree s = Free (StateF s)

A free monad builds a syntax tree of operations, which is then interpreted by a handler (a natural transformation):

interpret :: (f (Free f a) -> Free g a) -> Free f a -> Free g a

Freer monads (Kiselyov-Ishii, 2015) improve on free monads:

data Freer f a where
  Pure   :: a -> Freer f a
  Impure :: f x -> (x -> Freer f a) -> Freer f a

This CPS-style representation avoids the quadratic bind problem of naive free monads and does not require Functor instances.

Performance

Free/freer monads have overhead from building and interpreting syntax trees. Techniques for optimization:

  • Church-encoded free monads: CPS transform eliminates left-nested binds
  • Fused effects (Haskell library): Uses ReaderT IORef at the bottom, interpreting most effects efficiently
  • Polysemy / Effectful: Modern Haskell libraries using various strategies (type-class dispatch, IO-based)

Comparison of Approaches

| Approach | Composability | Performance | Type Safety | Flexibility | |---|---|---|---|---| | Monad transformers | Manual (lift) | Good (specialized) | Strong | Fixed stack order | | Free monads | Good | Moderate (interpretation overhead) | Strong | Flexible | | Algebraic effects | Excellent | Good (compiled) | Strong | Handler-based | | Effect type classes (mtl) | Good (no lift) | Good (inlining) | Strong | Constrained |

Theoretical Foundations

Lawvere Theories

Algebraic effects correspond to Lawvere theories: a Lawvere theory is a category with finite products where objects are natural numbers. Operations of arity n are morphisms n -> 1. Models are product-preserving functors to Set.

Scoping and Tunneling

Not all effects are algebraic. Scoped effects (Wu-Schrijvers-Hinze, 2014) handle effects with scope (like catch for exceptions, which scopes over a block). Effect tunneling (Zhang-Myers, 2019) ensures that effects propagate correctly through handler boundaries.

Typed Algebraic Effects

Bauer and Pretnar (2014) developed a full type-and-effect system for handlers:

  • Effect types are rows of operation signatures
  • Handler types: A ! E => B ! E' (transform computation of type A with effects E into result of type B with effects E')
  • Effect subtyping via row inclusion

Categorical Semantics

  • Effects as monads (Moggi): The Kleisli category of a monad models effectful computation
  • Effects as adjunctions: Every monad arises from an adjunction; different adjunctions give different computational interpretations (state, continuations, etc.)
  • Handlers as algebra homomorphisms: A handler for effect E is an E-algebra (Plotkin-Pretnar)

Current Research Directions

  • Effect tunneling and lexical effects: Ensuring effects respect lexical scope (not dynamic scope)
  • Higher-order effects: Effects whose operations take effectful computations as arguments (e.g., catch : (() -> a) -> (exn -> a) -> a)
  • Effect inference with principal types: Can effect types be inferred completely?
  • Efficient compilation: Compiling handlers to native code without continuation overhead (evidence-passing, selective CPS)
  • Integration with dependent types: Idris 2 has both effects and QTT; interaction is an active area