Algebraic Effects and Effect Rows in the Type System

A type that says Int says nothing about whether producing that integer read a file, threw an exception, or diverged. Effect systems extend the type with that information, and the extension is not cosmetic: it changes what a function’s type means, how it composes with other functions, and what the compiler can prove about the order in which operations happen. Algebraic effects are one family of such systems, distinguished by the fact that effects are operations with handlers rather than fixed labels.

The type of a computation carries its row

The core change is to annotate the arrow with a set of effects: τ₁ --⟨ε⟩--> τ₂, where ε is an effect row — a set of effect labels, possibly open. A pure function has the empty row. A function that may raise has ⟨exn⟩. A function that may raise or print has ⟨exn, io⟩. An open row ⟨exn | μ⟩ means: at least exn, and possibly more described by the variable μ.

The row is structurally the same object as the record row in row polymorphism, and the same unification machinery applies. The difference is in what the row is attached to and how it is consumed: a record row is a description of a value’s fields, an effect row is a permission attached to a computation, and the operation that removes a label is not field restriction but handling.

The composition rule is the important one. Applying a function with row ε₁ to an argument and then feeding the result to a function with row ε₂ gives a computation with row ε₁ ∪ ε₂. The union is computed by row unification, so an open row in one function absorbs the labels of the other. This is what makes effect polymorphism work: a higher-order function such as map has type (a --⟨ε⟩--> b) -> List a --⟨ε⟩--> List b, and the row variable ε is instantiated at the call site with whatever the supplied function actually does. The map implementation is written once, its row is inferred as ε, and the caller’s effect set flows through without map needing to know it.

Operations, not labels

An algebraic effect is declared as a set of operations with signatures. A State s effect declares get : () -> s and put : s -> (), and each operation is a constructor in the effect’s signature. A computation that performs get has the effect State s in its row, and the operation’s return type is part of the signature rather than part of the row. This is the difference from a label-based system, where io is a single opaque marker and the operations it permits are not described by the type.

The operational semantics is where the name comes from. Performing an operation suspends the computation and passes the operation and its arguments to the nearest enclosing handler. The handler receives a continuation representing the rest of the computation, and it may invoke that continuation zero, one, or many times. Invoking it zero times discards the rest of the computation, which is how an exception is encoded. Invoking it once is an ordinary effect. Invoking it twice duplicates the rest of the computation, which is how nondeterminism is encoded.

The continuation is a first-class value, and capturing it is the expensive part. An implementation that keeps the native stack must either copy the segment of the stack between the handler and the operation — which costs time proportional to the depth of that segment — or arrange for the handler to run on the same stack and resume the operation in place, which restricts a handler to resuming its continuation at most once. Implementations that compile to a CPS form or to a bytecode interpreter with an explicit stack avoid the copy by representing the continuation as a heap object, at the cost of heap allocation per suspension. The choice determines whether an effect-heavy program is cheap or expensive, and it is why the same effect system can have very different performance across backends.

Handling discharges the row

A handler is an expression that runs a computation and interprets its effects. Its typing rule is the mechanism worth stating precisely. Let the handled computation have row ⟨op | ε⟩, where op has signature A → B. Each clause binds the operation’s argument x : A and a continuation k : B → ⟨op | ε⟩, and must produce a computation whose row is ε. Under those conditions the handler expression itself has row ε.

    op : A → B          e has row ⟨op | ε⟩
  (x : A) (k : B → ⟨op | ε⟩) ⊢ clause has row ⟨ε⟩
-----------------------------------------------------
   handle e with { op(x) -> k => clause } has row ⟨ε⟩

The handled effect is removed, and every other effect remains. Each operation clause is checked with the continuation k having the row of the whole handled computation, minus the operation being handled, plus anything the handler’s own answer context adds. Because k still carries ⟨op | ε⟩, a clause may call it, or return a value as the new state of a fold; because the clause’s own row is restricted to ε, it cannot silently perform a fresh op outside the continuation. That asymmetry is what lets a handler re-run the continuation under updated state — the standard encoding of a state handler — while leaving any use of the operation itself inside the continuation, where it is again the handler’s business.

Two consequences follow.

Handling is not the same as catching. A handler’s clauses are typed per operation, so an operation left in the row of a computation that reaches main is a type error rather than a runtime failure. This is the property that makes effect rows useful for auditing: the row of main is a complete list of the effects the program may perform. The row’s open tail is unified by the same solver that handles record rows, described in row polymorphism for extensible records, including the lacks constraints that keep labels distinct.

Handlers compose in a specified order. Handling ⟨a, b⟩ with a handler for a leaves ⟨b⟩. Handling with a handler for b first leaves ⟨a⟩. The two orders give different results when the effects interact, and the type system records only the set, not the nesting. This is a real limitation: two programs with the same row can have different behaviour depending on the handler stack, and the type does not distinguish them. Systems that need the distinction add a scoped row that tracks nesting order, at the cost of a more complex row algebra.

Effect polymorphism and its inference

The row variable in map is inferred, not declared, in languages that infer effect rows, and the inference is a row unification problem with the same lacks constraints as records. Languages that declare rows instead, as Koka does with an explicit -> and effect annotation, get the same polymorphism from a declared effect variable at the definition. Either way, generalization at let applies: a let-bound function whose type has an open row becomes polymorphic in that row, and each use instantiates it independently.

The interaction with the value restriction is worth noting. A lambda applied to nothing performs no effect until it is applied, so a let-bound lambda is always a syntactic value and always generalizable, regardless of the row in its type. The effect information lives in the type and the value itself is inert, so the row adds nothing to what the restriction must consider. Languages with both effects and mutable references must still apply the restriction to the reference case, and the two features then interact only through the row of the function that allocates.

Inference is less pleasant when an effect is performed inside a branch. if c then e₁ else e₂ has the union of the branches’ rows, and if one branch is pure and the other performs io, the result has io. The union is computed by row unification, so an open row in one branch absorbs the labels of the other. If the branches have incompatible rows — different type arguments to the same effect constructor, say — the union fails and the expression is rejected, even though a handler could in principle reconcile them. The workaround is to handle each branch separately before joining.

Row polymorphism versus monadic effects

The alternative encoding of effects is a monad, where a computation of type M τ is a value describing the effect, and composition is bind. The two encodings differ in ways that matter for the type system.

A monadic type is closed in the sense that M τ names one effect, and combining two effects requires a monad transformer stack whose order is part of the type. The type StateT s (ExceptT e IO) τ says the effects are layered in that order, and the layering is observable. Effect rows are open: ⟨state s, exn⟩ is a set, and the order of handling is a property of the program rather than the type. Adding an effect to a function’s row does not require changing every caller’s type, because the row is a variable that the caller’s row absorbs; adding a layer to a transformer stack changes the type of every function in the stack.

The cost of the row approach is that the handler’s semantics are not constrained by the type. Two handlers for the same effect can behave differently — one may be a state handler, another a logger that ignores writes — and both typecheck against the same row. In the monadic encoding the behaviour is fixed by which instance the type names. This is a genuine expressiveness trade in both directions: rows admit more programs and prove less about them.

The performance trade runs the other way. A transformer stack is a chain of closures, and each bind allocates; the depth of the stack multiplies the allocation. A row-based implementation with native continuations can handle an effect with a single stack operation and no allocation per suspension. The comparison is not absolute, because a row implementation without native continuations pays the CPS cost instead, and the CPS cost can exceed the transformer cost for shallow stacks.

What effect rows cannot express

Effect interdependence. A row says which effects may occur, not in what order or under what conditions. A function that reads a configuration and then, only if a flag is set, writes a log has row ⟨read, write⟩, and the type does not record that the write depends on the read. Session types and typestate encode such orderings, and they are a different mechanism.

Resource linearity. A row does not say that a file opened must be closed. Linear types and uniqueness types express that, and they compose with rows: the row carries the effect, the linearity carries the obligation.

Effect subtyping in argument position. Rows as sets give a natural subtyping — a computation with fewer effects is usable where more are allowed — but only in the direction that weakens. A function that performs io cannot be used where a pure function is expected, which is the correct direction. The harder case is a higher-order function that requires its callback to have row ε: the callback is an argument, so the rule that would admit a callback with fewer effects is contravariance in the row, and most systems do not implement row subtyping at all. They quantify instead, as map does with its ε, and let each call site instantiate the row to whatever the supplied function performs. A system without that quantification and without row subtyping would reject the call; the practical obstacle is the same as in the variance lattice, where a constructor that both consumes and produces its parameter has no single variance.

Effects on values. A row is attached to a computation, not to a value. A data structure that contains a suspended computation with effects has a type that mentions the row inside the structure’s type argument, so the row becomes a parameter of the structure, and the definition must quantify it. In a language that restricts quantification to the front of a type — the prenex restriction that most inferred systems impose — the row has to be mentioned at the structure’s definition, which is expressible but verbose and is the point where effect systems start to look like monadic ones.