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

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

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