Introduction

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.

Try It

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.

<!-- Effect System demo: compose operations and check the inferred effect row -->
<div class="layout">
  <div class="panel left-panel">
    <h3 class="panel-title">Function Body</h3>
    <p class="panel-desc">Click operations to add them to your function. Each carries an effect tag.</p>
    <div id="op-list" class="op-list">
      <!-- operations injected by JS -->
    </div>
    <div class="allowed-row">
      <span class="allowed-label">Allowed effects for this function:</span>
      <div id="allowed-list" class="allowed-list">
        <!-- toggles injected by JS -->
      </div>
    </div>
  </div>
  <div class="panel right-panel">
    <h3 class="panel-title">Inferred Effect Row</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">Reset</button>
  </div>
</div>

/* global 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; }

/* operation items */
.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; }

/* allowed toggles */
.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; }

/* right panel */
.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; } }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Effect System demo — operations have effect tags; the checker infers
// the effect row (union of tags) and tests subset against the allowed set.

const OPS = [
  { id: 'read-file',    effect: 'IO',    label: 'Read file (IO)',    cls: 'op-io'    },
  { id: 'write-log',    effect: 'IO',    label: 'Write log (IO)',    cls: 'op-io'    },
  { id: 'read-state',   effect: 'State', label: 'Read counter (State)',   cls: 'op-state' },
  { id: 'write-state',  effect: 'State', label: 'Update counter (State)',  cls: 'op-state' },
  { id: 'throw-err',    effect: 'Throw', label: 'Throw error (Throw)',    cls: 'op-throw' },
  { id: 'pure-compute', effect: null,    label: 'Pure computation (no effect)', cls: 'op-pure'  }
];

// available effect labels for the allowed set
const ALLOW_OPTS = ['IO', 'State', 'Throw'];

const active = new Set();       // currently active operation ids
const allowed = new Set(['IO']); // start with IO allowed

function buildUI() {
  // render each operation as a clickable block
  const opList = document.getElementById('op-list');
  OPS.forEach(op => {
    const el = document.createElement('div');
    el.className = `op-item ${op.cls}`;
    el.dataset.id = op.id;
    el.innerHTML = `<span class="badge">${op.effect || '∅'}</span><span>${op.label}</span>`;
    el.addEventListener('click', () => toggleOp(op.id));
    opList.appendChild(el);
  });

  // render the allowed-set toggles
  const allowList = document.getElementById('allowed-list');
  ALLOW_OPTS.forEach(eff => {
    const btn = document.createElement('button');
    btn.className = `allow-toggle${allowed.has(eff) ? ' on' : ''}`;
    btn.dataset.eff = eff;
    btn.textContent = eff;
    btn.addEventListener('click', () => toggleAllowed(eff));
    allowList.appendChild(btn);
  });

  update();
}

function toggleOp(id) {
  // toggle an operation on/off
  active.has(id) ? active.delete(id) : active.add(id);
  document.querySelectorAll('.op-item').forEach(el => {
    el.classList.toggle('active', active.has(el.dataset.id));
  });
  update();
}

function toggleAllowed(eff) {
  // toggle an effect in/out of the allowed set
  allowed.has(eff) ? allowed.delete(eff) : allowed.add(eff);
  document.querySelectorAll('.allow-toggle').forEach(btn => {
    btn.classList.toggle('on', allowed.has(btn.dataset.eff));
  });
  update();
}

function inferredEffects() {
  // collect the union of effects from active operations
  const effs = new Set();
  active.forEach(id => {
    const op = OPS.find(o => o.id === id);
    if (op && op.effect) effs.add(op.effect);
  });
  return effs;
}

function update() {
  // recompute and display the effect row and verdict
  const inferred = inferredEffects();
  const rowEl = document.getElementById('effect-row');
  const verdictEl = document.getElementById('verdict');
  const explainEl = document.getElementById('explain');

  if (inferred.size === 0) {
    rowEl.textContent = '∅  (Pure)';
  } else {
    rowEl.textContent = '{ ' + [...inferred].join(', ') + ' }';
  }

  // verdict: inferred effects must be a subset of allowed
  const bad = [...inferred].filter(e => !allowed.has(e));
  if (bad.length === 0) {
    verdictEl.textContent = '✓ Effect row fits within allowed set.';
    verdictEl.className = 'verdict ok';
    if (inferred.size === 0) {
      explainEl.textContent = 'No active operations — the function is pure. It can be called from anywhere.';
    } else {
      explainEl.textContent = 'All inferred effects are permitted. The type checker would accept this function at this call site.';
    }
  } else {
    verdictEl.textContent = fmt('✗ Leaked effects not in allowed set: %bad%', { bad: bad.join(', ') });
    verdictEl.className = 'verdict bad';
    explainEl.textContent = 'The function performs effects the call site does not permit. Add those effects to the allowed set, or remove the offending operations.';
  }
}

document.getElementById('reset-btn').addEventListener('click', () => {
  // clear all active operations
  active.clear();
  document.querySelectorAll('.op-item').forEach(el => el.classList.remove('active'));
  update();
});

buildUI();
Result
Console

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.

The Theory

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)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 ee 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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/effect-systems/Content licensed under CC BY-NC 4.0.