Algebraic Effects

Origin. Plotkin and Power introduced algebraic effects across a sequence of papers (2001–2003): effects arise as operations generating a free algebra, and the monad is determined by the operations and their equations rather than assumed. Handlers are Plotkin and Pretnar, "Handlers of Algebraic Effects" (ESOP 2009) — joint work, not Pretnar's alone; Pretnar's thesis (2010) and the Eff language with Bauer are the follow-on. Effects as operations with equations. Handlers as interpreters for effects. Foundation for effect systems in programming languages.

Models. Computational effects algebraically. Monad: encapsulate effects (IO, state, exceptions). Algebraic effects: effects as operations, handlers as interpretations. More modular than monads. Separate effect signatures from implementations.

Formalism.

Effect signature: Σ = {opᵢ: Aᵢ → Bᵢ} Operations with parameter and return types.

Example operations:

get: 1 → S (state)
put: S → 1 (state)
raise: E → 0 (exceptions)
choice: 1 → Bool (nondeterminism)

Free monad: Free(Σ, A): computations using ops from Σ returning A. Tree of operations with A at leaves.

Handlers: handler H { return x → e_ret; op(x, k) → e_op }

H interprets operations:

return: what to do with final value
op: how to handle operation (k is continuation)

Effect types: A ! {op₁, ..., opₙ} Computation returning A, may use ops.

Example (state handler): handler { return x → λs. (x, s); get((), k) → λs. k(s)(s); put(s', k) → λs. k(())(s') }

Equations: get; put(s); m = m (put after get irrelevant if not using value) Operations may satisfy algebraic equations.

Symbols.

Symbol	Unicode	Name	Meaning
Σ	U+03A3	Sigma / Effect signature	Set of operation symbols with parameter and arity types
λ	U+03BB	Lambda	Function abstraction in handler clauses
→	U+2192	Arrow	Operation typing op: A → B, and function types
⊗	U+2297	Tensor of theories	Commuting combination of two effect theories
⊕	U+2295	Sum of theories	Free non-interacting combination of two effect theories
op	—	Operation	Effect operation, an algebraic operation on the monad
!	—	Effect annotation	Computation type A ! {ops}: returns A, may perform ops
k	—	Continuation	Rest of the computation, bound in an operation clause
handler	—	Handler	Model of the signature; handling is the induced homomorphism
return	—	Return	Pure value case of a handler
Free	—	Free monad	Initial algebra of A + Σ(−); uninterpreted effect trees
1	—	Unit type	Trivial parameter or return type
0	—	Empty type	Return type of a non-returning operation such as raise

Metatheory. The free-model monad of an equational theory is the effect monad, so state, exceptions, nondeterminism and input/output are recovered from their operations and equations rather than postulated: the theory of a single global store yields the state monad, the theory with one nullary operation per exception yields the exception monad. Plotkin and Power, "Algebraic Operations and Generic Effects" (2003), proved the key correspondence: algebraic operations of arity n on a strong monad T are in bijection with generic effects 1 → T(n), so an operation is the same thing as a computation returning an n-ary choice. Handling is not an algebraic operation, since it fails to commute with sequencing; Plotkin and Pretnar's handler semantics instead reads a handler as a model of the signature and the handling construct as the unique homomorphism out of the free model, which is why handlers are given by a universal property. Hyland, Plotkin and Power, "Combining Effects: Sum and Tensor" (2006), showed that the sum of theories corresponds to non-interacting combination and the tensor to commuting combination, and that familiar monad transformers arise as tensoring with a fixed theory.

Applies to. Programming language design (Eff, Koka, OCaml 5). Effect systems. Exception handling. Async/await. Generators. Delimited continuations. Modular interpreters.

Limitations. Not every monad is algebraic. The continuation monad is the standard counterexample: it is not the free-model monad of any equational theory over Set, so continuations fall outside the algebraic account even though handlers can simulate delimited control operationally. Exception handling is likewise not an operation — handling does not commute with sequencing — so the symmetry between constructing and eliminating effects is broken, and handlers sit outside the algebra. Handlers need not respect the equations of the theory they handle: a handler is typed against the signature alone, so a state handler that violates the get/put laws remains well typed, and equational correctness is an extra proof obligation rather than a consequence of typing. Combination is not canonical, since sum and tensor give different and sometimes both unwanted interactions. Effect signatures are not abstraction-safe: a surrounding handler can intercept operations performed by a client, so effect types leak implementation, and dynamically generated effect instances raise scope-extrusion problems that the plain algebraic theory does not address.