Effect Systems

Every useful program reaches outside itself: it reads a file, writes to a database, throws an exception, or draws a pixel. We call these side effects — things a function does beyond returning a value.

The problem is that ordinary type systems ignore them. A function readUser(id: Int) -> User promises a User, but says nothing about whether it hits the network, mutates global state, or crashes. All of that is hidden in the implementation. You discover it at runtime — or worse, in production.

Effect systems fix this by extending the type checker to track effects alongside values. Instead of just Int -> String, you write Int -> String ! {IO, Throw}, where the annotation ! {IO, Throw} is the effect row — a set declaring exactly what the function is allowed to do. The type checker then verifies that every call site permits those effects, and that functions claiming to be pure really are.

This idea was formalized in the late 1980s by Gifford and Lucassen (1988), and has since surfaced in languages like Koka (effect rows, 2014), Effekt, OCaml 5 (effects + continuations), and as an influence on Rust's async/Send/Sync traits. Related ideas: the Halting Problem shows some properties can never be checked statically, while program synthesis explores generating correct programs from specs.

Each colored block below is a primitive operation with a known effect: IO (read/write), State (mutable memory), Throw (exceptions), or Pure (no side effects at all). Click the blocks to toggle them on or off and compose a function body. The checker on the right infers the effect row — the union of all effects — and compares it against the allowed set you choose.

<!-- {{c_html_intro}} -->
<div class="layout">
  <div class="panel left-panel">
    <h3 class="panel-title">{{title_ops}}</h3>
    <p class="panel-desc">{{desc_ops}}</p>
    <div id="op-list" class="op-list">
      <!-- {{c_ops_injected}} -->
    </div>
    <div class="allowed-row">
      <span class="allowed-label">{{label_allowed}}</span>
      <div id="allowed-list" class="allowed-list">
        <!-- {{c_allowed_injected}} -->
      </div>
    </div>
  </div>
  <div class="panel right-panel">
    <h3 class="panel-title">{{title_inferred}}</h3>
    <div id="effect-row" class="effect-row">—</div>
    <div id="verdict" class="verdict"></div>
    <p class="panel-desc" id="explain"></p>
    <button id="reset-btn" class="reset-btn" type="button">{{btn_reset}}</button>
  </div>
</div>

/* {{c_css_reset}} */
* { box-sizing: border-box; margin: 0; padding: 0; }
body { font-family: system-ui, sans-serif; color: #222; font-size: 14px; }
.layout { display: flex; gap: 12px; padding: 10px; min-height: 360px; }
.panel { flex: 1; background: #f4f7fa; border-radius: 10px; padding: 14px; }
.panel-title { font-size: 1rem; font-weight: 700; margin-bottom: 6px; color: #1d3557; }
.panel-desc { font-size: .82rem; color: #555; margin-bottom: 10px; line-height: 1.4; }

/* {{c_css_ops}} */
.op-list { display: flex; flex-direction: column; gap: 7px; margin-bottom: 12px; }
.op-item { display: flex; align-items: center; gap: 8px; padding: 8px 10px;
           border-radius: 8px; cursor: pointer; border: 2px solid transparent;
           transition: all .15s; user-select: none; font-weight: 600; font-size: .88rem; }
.op-item:hover { filter: brightness(.93); }
.op-item.active { border-color: #1d3557; }
.op-item .badge { width: 28px; height: 28px; border-radius: 6px;
                  display: flex; align-items: center; justify-content: center;
                  font-size: .75rem; font-weight: 800; flex-shrink: 0; }
.op-io   { background: #dbeafe; } .op-io   .badge { background: #3b82f6; color: #fff; }
.op-state{ background: #dcfce7; } .op-state .badge { background: #16a34a; color: #fff; }
.op-throw{ background: #fee2e2; } .op-throw .badge { background: #dc2626; color: #fff; }
.op-pure { background: #f3f4f6; } .op-pure  .badge { background: #6b7280; color: #fff; }
.op-item.active.op-io   { border-color: #3b82f6; }
.op-item.active.op-state{ border-color: #16a34a; }
.op-item.active.op-throw{ border-color: #dc2626; }
.op-item.active.op-pure { border-color: #6b7280; }

/* {{c_css_allowed}} */
.allowed-row { margin-top: 4px; }
.allowed-label { font-size: .8rem; color: #555; display: block; margin-bottom: 6px; font-weight: 600; }
.allowed-list { display: flex; gap: 6px; flex-wrap: wrap; }
.allow-toggle { padding: 4px 10px; border-radius: 20px; border: 2px solid #aaa;
                cursor: pointer; font-size: .8rem; font-weight: 600; background: #fff;
                transition: all .15s; user-select: none; }
.allow-toggle.on { background: #1d3557; color: #fff; border-color: #1d3557; }

/* {{c_css_right}} */
.effect-row { font-size: 1.1rem; font-family: ui-monospace, monospace;
              background: #fff; border-radius: 8px; padding: 10px 14px;
              min-height: 44px; margin-bottom: 10px; color: #1d3557;
              border: 1px solid #cdd9e3; word-break: break-all; }
.verdict { font-size: .95rem; font-weight: 700; margin-bottom: 8px; min-height: 1.3em; }
.verdict.ok  { color: #0a7d33; }
.verdict.bad { color: #c92f3c; }
.reset-btn { margin-top: 10px; padding: 6px 16px; border-radius: 8px;
             border: 1px solid #1d3557; background: #fff; color: #1d3557;
             font: 600 13px system-ui, sans-serif; cursor: pointer; }
.reset-btn:hover { background: #1d3557; color: #fff; }
@media (max-width: 480px) { .layout { flex-direction: column; } }

// Code not found

Notice the asymmetry: checking that a given effect row is a subset of the allowed set is a simple set-inclusion test — instant. Inferring the full effect row of an arbitrary program, on the other hand, requires solving a system of effect-variable constraints (similar to unification in type inference), and deciding whether two effect-polymorphic functions can be composed safely is the core challenge effect-system designers face.

How do effect systems work, and how hard is the inference problem?

• Effect rows as sets. The simplest model attaches a finite set of effect labels to each function type: f : A -> B ! {e1, e2, ...}. Checking safety is set inclusion: the caller's allowed set must contain the callee's effect row. This is $O(n)$ in the size of the row — trivially fast.

• Row polymorphism. A function like map should work over callbacks that have any effect row, not just a fixed one. The solution is effect variables: map : (A -> B ! e) -> List A -> List B ! e. The variable $e$ is filled in at each call site by unification, exactly as type variables are in Hindley–Milner inference. Inference stays in PTIME for first-order programs.

• Algebraic effects and handlers. Koka and Effekt go further: effects are not just labels but operations with signatures, and handlers intercept them — like resumable exceptions. This gives you concurrency, parsers, and state all as library code, without built-in primitives. The price is that handler-based programs require delimited continuations, which complicates the runtime but not the type-checking complexity.

• Effect polymorphism and decidability. When higher-order functions interact with effect polymorphism, inference can become undecidable in the most general setting (shown by various authors in the 1990s). Practical systems sidestep this with syntactic restrictions or explicit annotations, keeping the common case decidable and the type checker fast.

• Subeffecting. Pure $\subseteq$ State $\subseteq$ IO is a natural lattice: a pure function can always be used where an IO function is expected. This subtyping — called subeffecting — is the effect analogue of subsumption in ordinary type systems.

The key insight: most of the hard cases (undecidability, exponential blowup) arise only with unrestricted higher-order effect polymorphism. For the fragment that real languages implement, effect checking is as fast as ordinary type-checking.

Effect tracking has found its way into production languages and major systems:

• Haskell's IO monad: the oldest mainstream effect system. Any function that performs IO must return IO a; pure functions cannot be called from impure ones without explicit lifting. The type system enforces the boundary.
• Rust's async / Send / Sync: not labeled "effects," but functionally equivalent — trait bounds that propagate through the call graph and are checked at compile time.
• Koka (Microsoft Research, Daan Leijen, 2014–present): the canonical research language for algebraic effects. Every function's type includes its effect row; handlers can intercept and resume effects like cooperative coroutines.
• OCaml 5 effects: algebraic effects landed in OCaml's mainstream release in 2022, bringing effect-based concurrency (Eio) without callback hell.
• Java checked exceptions: the earliest mainstream attempt — methods declare which exceptions they throw, and callers must handle or re-declare them. Widely criticized for verbosity, but the core idea is an effect system.
• Capability-based security: treating "can access the network" as an effect passed as a capability object is an active area of language design (Scala 3's capture checking, 2024).

Effect systems let architects draw a purity boundary in the codebase and enforce it mechanically. Pure core logic becomes easier to test, parallelize, and reason about — while side-effectful shells are confined to well-marked regions.

Effect systems answer a deceptively simple question: what does this function do to the world? By recording the answer in the type, the compiler can check it, enforce it, and refuse to compile code that breaks the contract.

The idea is older than most programmers realize (Gifford & Lucassen, 1988), yet it keeps resurfacing because the problem it solves never goes away. Every time a bug sneaks in through an unexpected database write or a surprise network call, an effect system would have caught it before the code ever ran.

The Halting Problem reminds us that no type system can catch everything statically. But effect systems carve out a rich, useful slice of program behavior — purity, IO, state, exceptions — and put it squarely under the type checker's watch.