Type Implspec

Effect Systems

A type that says what a function does, not just what it returns. You already use several partial effect systems — checked exceptions, `async`, `const`, `unsafe` — and the complaints about function colouring are the honest cost of the idea.

The question

Can the type of a function say what it *does*, not just what it returns?

Source→Lexing→Tokens→Parsing→AST→Semantics→Typed→IR→Optimize→Codegen→Machine code→Link→Execute

What the program is here

A typing judgement with three parts instead of two: an environment, a term, a type, and an effect row — Γ ⊢ e : τ ! {IO, Exn}. The row is inferred and propagated exactly like the type, so calling an effectful function makes the caller effectful unless a handler discharges the effect. The representation exists to answer a question a return type cannot: what happens on the way to producing this value.

What this phase may assume or do

A call is well-typed only if the callee's effect row is contained in the row the calling context permits. An effect leaves a row in exactly one way: a handler discharges it. The payoff for the compiler is the converse — an expression whose row is empty is pure, so it may be reordered, duplicated, eliminated if unused, hoisted out of a loop or evaluated at compile time. That is why tracking purity is worth the annotation burden at all: [[optimization-legality]] is otherwise reduced to guessing.

Key points

An effect system puts what a function *does* in its type, alongside what it returns, and propagates it to callers.
Checked exceptions, async, const, constexpr and unsafe are all partial effect systems already in production use.
A full system adds three things: user-defined named effects, inference, and polymorphism over effects.
A handler discharges an effect, and because handlers can capture the continuation, one construct subsumes exceptions, generators, async and dependency injection.
Function colouring is real and inherent — propagation is the feature — but the duplication it causes is not, and is caused by the absence of effect polymorphism.
Java checked exceptions are the largest deployed experiment and were largely rejected, for the two reasons a modern system aims to fix.
The compiler's payoff is purity: an empty effect row licenses hoisting, elimination, reordering, deduplication and compile-time evaluation.

The effects you already have

Effect systems sound exotic until you notice how many partial ones are already in daily use. Each of the following puts something in a signature that is not the return type, propagates it to callers, and refuses to compile when the propagation is not acknowledged.

Java checked exceptions. throws IOException is an effect annotation. It is inferred nowhere and declared everywhere, it propagates to callers, and a caller must either declare it too or discharge it with a catch — which is precisely a handler. It is the most widely deployed effect system in existence and it is broadly disliked, which is data worth taking seriously rather than an embarrassment to explain away.

`async` in JavaScript, Python and Rust. An async function returns a promise or a future rather than a value, so calling one from a synchronous function does not give you the value; you must be async yourself, or run an executor. That is an effect propagating up the call graph with a discharge point at the top. It is exactly the same shape as checked exceptions with different syntax.

`const` in C++ and `const fn` in Rust. These are purity annotations from the other direction: they constrain what a function may do, and the compiler enforces it. constexpr goes further and makes the reward explicit — a function whose effects are empty enough may be evaluated at compile time, which is [[compile-time-evaluation]].

`unsafe` in Rust. A capability marker on a function that propagates to callers unless discharged by an unsafe block, which is a handler that says "I have discharged the obligation". Same machinery again.

What none of these have is *polymorphism over the effect*, and that omission is the source of essentially every complaint about them. A general-purpose map should work over a pure function and over an effectful one, and in every system above it cannot: you need map and mapAsync, or a throws-generic signature the language cannot express. Full effect systems exist mainly to fix that.

Partial effect systems already in productionimplementation

Mechanism	Effect tracked	Inferred or declared	Discharge	Escape hatch
Java `throws`spec	Checked exceptions	Declared	`catch`	Wrap in an unchecked exception
`async` / `await`implementation	Suspension	Declared by `async`, propagated by `await`	An executor or event loop at the top	Block the thread; `asyncio.run`; `block_on`
C++ `const` / `noexcept`spec	Mutation of the receiver; not throwing	Declared	n/a — it is a constraint, not an obligation	`mutable`, `const_cast`
Rust `const fn`implementation	Compile-time evaluability	Declared	n/a	Use a non-const path
Rust `unsafe`spec	Unverified obligations	Declared	An `unsafe` block	None — the block is the hatch
Haskell `IO`implementation	All side effects	Inferred through types	Only at `main`	`unsafePerformIO`
Koka / Eff / OCaml 5implementation	Arbitrary named effects, with rows	Inferred	A handler, anywhere	Varies by system

What a full effect system adds

implementationThe syntax is Koka-flavoured pseudocode, not a real language's. Koka, Eff, Frank and OCaml 5 differ substantially in how effects are declared, whether rows are inferred, and whether handlers are one-shot or multi-shot — OCaml 5's handlers are one-shot and untyped in the sense that effects do not appear in function types, which is a deliberate trade to avoid changing every signature in the ecosystem.

A research-grade effect system — Koka, Eff, Frank, and the effect handlers now in OCaml 5 — generalises the partial systems in three ways.

First, effects are named and open: you declare effect Log { fun log(msg: string): unit } and it is an ordinary effect like IO or Exn, not a built-in. That means a library can define its own effects, and a caller can see them in the signature.

Second, effects are inferred, so most code carries no annotation and the row appears only in signatures where it matters. This is the difference that makes checked exceptions painful and Koka bearable: Java requires you to write every throws by hand, and there is no inference to relieve you.

Third, and most importantly, functions can be polymorphic over effects. A map can be typed as "whatever effects the supplied function has, map has", which is what removes the need for a separate mapAsync. This is the piece every partial system lacks and the reason colouring hurts.

The handler is the other half. A handler discharges an effect by interpreting it, and because handlers can capture the continuation, one construct expresses exceptions, generators, async, backtracking and dependency injection. That is the theoretical payoff: async/await, iterators and exceptions stop being three separate language features with three separate lowerings — see [[async-lowering]], [[coroutine-lowering]] and [[exception-handling]] — and become three uses of one.

The practical payoff is testing and sandboxing. If the effects a function may perform are in its type, then a test can supply a handler that fakes them, and a runtime can refuse to run code whose row includes an effect it has not granted. That is a capability system by another name, and it is why this idea keeps surfacing in the context of running untrusted or model-generated code — [[typed-tool-calls]] and [[plan-validation]] want exactly this property.

An effect, a function that uses it, and a handler that discharges it

1effect Log {
2  fun log(msg: string): unit
3}
4 
5// The row is inferred: process has effect {Log}
6fun process(items: list<int>): int {
7  var total = 0
8  for (x in items) { log("saw " + show(x)); total := total + x }
9  total
10}
11 
12// A handler discharges it. Two handlers, two behaviours, one function.
13fun main() {
14  with handler { fun log(m) { println(m); resume(()) } }
15  print(process([1,2,3]))          // logs to stdout
16}
17 
18fun test() {
19  var seen = []
20  with handler { fun log(m) { seen := Cons(m, seen); resume(()) } }
21  assert(process([1,2,3]) == 6)    // logs captured, nothing printed
22}
23 
24// Effect polymorphism: map has whatever effects f has.
25fun map<a,b,e>(xs: list<a>, f: a -> e b): e list<b>

The last line is the point of the whole design. Without it you need one map per effect, which is what colouring costs in every mainstream language.

Function colouring, taken seriously

The standard complaint is Bob Nystrom's "What Color is Your Function": once some functions are async, calling one from a normal function is impossible, so async spreads virally up every call path until it reaches the top. You end up maintaining two versions of the same library, and the boundary between the colours is a constant source of friction.

The complaint is correct and it applies to every effect system, including the good ones. If an effect is in the type, it propagates, and propagation is precisely what makes it useful. You cannot have "the signature tells you what it does" and "the signature does not change when what it does changes"; those are the same statement with opposite signs.

What is *not* inherent is the duplication. The reason you need map and mapAsync is that mainstream languages cannot abstract over the colour. A system with effect polymorphism writes map once. So the honest framing is that colouring has two costs — propagation, which is the feature, and duplication, which is a missing feature — and the languages people complain about have the first without the fix for the second.

This is live work rather than theory. Rust's keyword-generics initiative is an attempt to let a single function be generic over async and const; Zig's anytype-driven approach and its earlier async design attacked the same problem; and the periodic argument for "coloured functions considered harmful" in Go is really an argument that Go chose to make every function the same colour by making goroutines cheap enough that nobody needs an async marker. That last one is a legitimate third answer: remove the distinction from the language and pay for it in the runtime.

And the Java data point deserves its weight. Checked exceptions are an effect system that shipped to millions of developers and were largely rejected in practice — swallowed with empty catch blocks, wrapped in RuntimeException, or declared as throws Exception. The reasons are exactly the two above: no inference, so every signature must be maintained by hand; and no polymorphism, so a generic interface like Function<T,R> cannot be written to accommodate a caller's exceptions. Any proposal for a new effect system has to explain why it will not go the same way.

What the compiler gets out of it

typicalMainstream optimizers do exploit purity where they can establish it — LLVM's readnone/readonly/nounwind attributes, GCC's pure/const — and generally infer them intraprocedurally plus for a small set of known library functions. They will not usually establish purity across an opaque call or through a function pointer, which is exactly the gap a declared effect row closes. Whether any particular hoist or elimination happens is an optimizer decision to verify in the output, not to assume.

The reason a compiler writer cares is stated in the legality condition: an expression with an empty effect row is pure, and purity is the precondition for most of the interesting transformations. A pure call may be hoisted out of a loop by [[loop-invariant-code-motion]], eliminated if its result is unused by [[dead-code-elimination]], deduplicated by [[common-subexpression-elimination]], reordered freely, or evaluated at compile time by [[partial-evaluation]]. None of those are legal for a call that might print, allocate observably, throw, or read mutable state.

In a language without effect tracking the compiler has to establish purity itself, by interprocedural analysis, and it usually cannot — which is why C and C++ compilers offer __attribute__((pure)) and const for the programmer to assert what the compiler could not infer. Those attributes are an unchecked effect system, and getting one wrong is undefined behavior rather than a type error, which is the worst possible version of this idea.

The other beneficiary is the human. An effect row in a signature is documentation the compiler maintains: it cannot go stale, it cannot be forgotten in a refactor, and a reviewer can see that a function which was supposed to be a pure computation has acquired a database call. That is the same argument [[algebraic-data-types]] makes for putting failure in the return type, applied to everything else a function might do.

How it works

The steps, in the order the compiler takes them.

The typing judgement is extended with an effect row, so every expression has both a type and a set of effects.
Effect rows are inferred by the same unification machinery as types, with row variables standing for "whatever else the caller has" — which is what makes effect polymorphism possible.
A call site unions the callee's row into the caller's; a function's declared row must contain everything its body can perform.
A handler removes an effect from the row of the expression it wraps, and provides an implementation for each operation of that effect.
Handlers are compiled by capturing the continuation at the point of the operation, so the handler can resume it once, many times, or not at all — which is how one construct expresses exceptions (never resume), generators (resume once, later) and backtracking (resume many times).
The optimizer consults the row: an expression whose row is empty is pure and may be moved, duplicated or removed subject to the ordinary legality rules.
Where a language has only a fixed set of effects (checked exceptions, async), the same machinery degenerates to a declared set with no inference and no row variables.

How it breaks

What the engineer observes when it goes wrong — not what goes wrong internally.

A signature acquires a new effect and the change propagates through forty call sites up to main; the pull request is enormous and the review focuses on the mechanical churn instead of the actual change.
A library exposes a pure-looking callback interface, a caller needs to perform an effect inside the callback, and there is no way to express it — so the effect is smuggled through a mutable variable or an unchecked exception and the signature now lies.
Checked exceptions are declared as throws Exception throughout a codebase to stop the propagation; the annotations are still present, carry no information, and the compiler still enforces them, which is the worst of both.
An empty catch block swallows an exception to satisfy the compiler; the failure becomes silent and surfaces later as missing data with no error anywhere in the logs.
An async function is called from a synchronous path and the returned promise is dropped unawaited; the work runs, its failure is unobserved, and the caller proceeds as though it succeeded.
A purity attribute is asserted by hand on a function that is not pure; the optimizer hoists a call out of a loop, and the observable behaviour changes between optimization levels with no diagnostic at all.

When it helps

Making the cost of a function visible in its signature: that a "getter" performs I/O is exactly the thing a reviewer should not have to discover by reading the body.
Testing, where a handler can replace the real effect with a recording one and no dependency injection framework is required.
Sandboxing and capability control, where refusing to run code whose effect row exceeds what was granted is a static check rather than a runtime interception — the property [[typed-tool-calls]] and [[plan-validation]] are reaching for.
Optimization: an empty row licenses the whole family of transformations that require purity, without an interprocedural analysis that would usually fail.
Unifying language features: exceptions, generators, async and resource scoping as instances of one construct rather than four with separate lowerings.

When it hurts

Any codebase where effects change often, since every change propagates through every caller and the diff is dominated by signature churn.
Languages without effect polymorphism, where the absence forces a duplicated API per colour and the duplication never converges.
Interop with an ecosystem that has no effect information, where every foreign call has to be assigned a row by hand or given a maximally permissive one — at which point the tracking stops meaning anything.
Error messages: a mismatch between two effect rows, especially with row variables involved, produces some of the least readable diagnostics in any type system.
Teams under delivery pressure, where the observed behaviour with checked exceptions is that the escape hatch wins and the annotations become noise.

What it costs

Every one of these is paid by something.

Putting effects in types buys signatures that cannot go stale and a compiler-checked account of what code does, and pays with viral propagation: a change to what a leaf function does edits every signature on the path to main.
Inference buys most of the annotation burden back and pays in diagnostics — an inferred row that does not match an expected one produces an error about types nobody wrote.
Effect polymorphism removes the duplicated-API cost and pays in type-system complexity: row variables, row unification and their error messages are a substantial addition to a language.
Handlers that capture the continuation buy one construct in place of four and pay in implementation cost and in runtime representation — a continuation has to be materialised somehow, and the cheap version is one-shot only.
Unchecked purity attributes (__attribute__((pure))) buy the optimizer's payoff with none of the ceremony, and pay by making a wrong assertion undefined behavior rather than a type error.

What else you could do

What a different compiler or language does instead, and when that is better.

Monads: encode the effect in the return type rather than in a separate row, which needs no new type-system machinery and pays in composition — stacking several monads requires transformers, and the resulting types are hard to read.
Capability passing: hand each function the objects it is allowed to use, so the signature shows the capabilities without any effect machinery. Simpler and enforced only by discipline about not capturing globals.
Dynamic interception — dependency injection, mocking frameworks, LD_PRELOAD — achieves the testing benefit with no static guarantee at all, and is what most ecosystems actually use.
Unchecked annotations (pure, const, noexcept) give the compiler the fact it needs with no verification, which is cheap and turns a mistake into undefined behavior.
Making every function the same colour, as Go does with cheap goroutines and blocking calls: removes the propagation problem by removing the distinction, and pays for it in the runtime rather than in the type system.

See it for yourself

The flag, dump or tool that shows you this directly.

Java: javac -Xlint:all plus a grep for catch (Exception and for empty catch blocks measures how much of the checked-exception system is actually carrying information in a given codebase.
LLVM: clang -S -emit-llvm and look for readnone, readonly, nounwind and willreturn on function declarations — that is the compiler's own effect row, and it is directly readable.
GCC/Clang: mark a function __attribute__((pure)), put a call to it in a loop, and diff the assembly at -O2 with and without the attribute; the hoist is the payoff made visible.
Rust: cargo build will not let an async fn be called without .await, and the #[must_use] lint on futures is what catches the dropped-promise failure mode.
OCaml 5: the effects tutorial in the manual runs handlers directly; Koka's playground shows inferred effect rows on hover, which is the fastest way to see inference and row polymorphism working.

Plausible wrong readings

Stated the way a confident engineer states them.

"Effect systems are academic and nothing uses them." Checked exceptions, async, const, constexpr and unsafe are all partial effect systems in daily production use.
"Function colouring is a design mistake." Propagation is the feature — a signature that did not change when the behaviour changed would be worthless. The mistake is the missing polymorphism that turns propagation into duplication.
"Async is different from checked exceptions." They are the same mechanism: an effect declared on a function, propagated to callers, discharged at a boundary. The syntax differs and the shape does not.
"Tracking purity is only useful for functional programming." It is what licenses hoisting, elimination and compile-time evaluation, which is why C compilers ship an unchecked, undefined-behavior-flavoured version of it.

Misconceptions

The claim, and what is actually true.

An effect system means writing annotations everywhere.

In a system with inference the rows appear only where you declare a signature, and are computed elsewhere. Java requires them everywhere because it has no inference, which is a large part of why it is disliked.

Async and exceptions are unrelated language features.

Both are effects: declared on a function, propagated to callers, discharged at a boundary. With effect handlers they are two uses of one construct rather than two features with two lowerings.

Purity tracking is about mathematical elegance.

It is the precondition for hoisting, deduplicating, eliminating and compile-time-evaluating a call. A compiler that cannot establish purity must assume the worst, which is why C compilers offer an unchecked way to assert it.

Go deeper

The same idea at increasing depth. Stop wherever it stops being useful.

overview

Normally a function's type tells you what it takes and what it gives back. An effect system adds what it does on the way: reads a file, might throw, suspends, mutates state. Callers inherit those effects unless something handles them. You already use small versions of this — throws in Java, async in JavaScript — and the shape is always the same.

practical

Two things transfer to work you are doing today. First, when you feel the pain of colouring — needing an async copy of a function, or a throws you cannot express in a generic interface — recognise it as a missing effect-polymorphism feature rather than as a mistake you made. Second, the testing pattern is available without any of the machinery: pass in the things a function is allowed to do rather than letting it reach for them, and you get most of the substitutability that handlers give, enforced by convention instead of by the compiler. And if you are running code you did not write — a plugin, a model-generated plan — the effect-row idea is the right mental model for what to check before you run it, even where the language will not check it for you.

advanced

The deepest thing effect handlers give you is that the *interpretation* of an effect is separated from its *use*, which is the same separation an interface gives for data, applied to control flow. Because a handler receives the continuation, it decides whether the operation resumes once (a normal call), never (an exception), later (async), or many times (backtracking and probabilistic search). That is why one construct subsumes several language features that otherwise each need their own lowering — [[async-lowering]] and [[coroutine-lowering]] are both compiling a special case of it. The implementation cost is real: a general handler needs a materialised continuation, which means either a segmented stack, a CPS transform of the whole program, or a restriction to one-shot resumption so the continuation can be a stack segment that is moved rather than copied. OCaml 5 took the last option. Which restriction a language accepts determines whether it gets generators, or async, or both, from the same feature.

How much this depends on

Nothing in this domain is true of every compiler. These say how much.

specJava checked exceptions are specified: a method must declare or catch any checked exception its body can throw, and this is enforced by the compiler. The escape hatches — wrapping in RuntimeException, declaring throws Exception — are equally legal, which is why the system's practical strength depends on convention rather than on the specification.

implementationThe claim that async colouring is an effect system describes the shape of the mechanism, not an official framing by any of these languages. The implementations differ substantially: JavaScript async functions always return a promise, Rust futures are inert until polled and require an executor, and Python coroutines require a running loop. The propagation property is common; nothing else is.

implementationOCaml 5 has effect handlers but does not track effects in function types — a deliberate decision to avoid changing every signature in the existing ecosystem. So it has the handlers without the rows, which is a different product from Koka and is worth distinguishing when comparing the two.

typicalProduction optimizers infer purity attributes intraprocedurally and for known library functions, and generally do not establish them across opaque calls or indirect calls. Whether a particular pure call is actually hoisted or eliminated depends on the optimizer, the level and the surrounding code, and should be verified in the emitted output rather than assumed from the attribute.

If you were asked this in an interview

Name three effect systems you have used without calling them that, and say what each tracks and how it is discharged.
Explain the function-colouring complaint. Which part of it is inherent to putting effects in types, and which part is a missing feature?
What can a compiler do with a call it knows is pure that it cannot do otherwise? Give three transformations.

Connections

Concurrencyasync-await coroutines structured-concurrency cancellation futures-and-promises

Securitysandboxing least-privilege trust-boundaries

API Designerror-model error-taxonomy

Agentic AItool-schemas argument-validation

Backenderror-taxonomy

Runtime gain3

Compile cost3

Debuggability3

Implementation5

Context dependence5

Runtime gain comes from the optimizer, not from the annotations: a declared empty row licenses transformations an interprocedural analysis usually cannot establish, and that is worth real time in hot code. Compile cost is moderate — row inference is unification with an extra dimension. Implementation complexity is maximal because effect polymorphism means row variables, row unification and the error messages that come with them, and handlers require materialising continuations. Context dependence is likewise maximal: almost every language has a different fragment of this idea under a different name.