Skip to content

Software Quality

Effect systems

An effect system extends a function's type to say what the function does, not just what it returns. Reading state, performing I/O, throwing, allocating, suspending, diverging — each becomes a row in that type, so the compiler can reject not just "this int was used as a string" but "this function was declared pure and tried to read a file."

What it catches

  • Effect leaks. A function declared pure that performs I/O fails to type-check.
  • Async-in-sync misuse. Calling an async function from a sync context without declaring the effect is a type error.
  • Unhandled exceptions. Effect-typed exceptions (Koka's exn, F*'s Exn) force handlers or propagation declarations at every call site.
  • Hidden state. A function that reads from a global counter in a "pure" context is rejected; the read effect must be in the type.
  • Divergence (non-termination). Koka's div effect separates total functions from potentially-diverging ones.
  • Capabilities and resource use. Effekt and Frank use capability-typed handlers — the function can use only the resources its handlers grant.

Effect systems do not catch logic bugs that respect the declared effects: a function declared <state, exn> can still write the wrong value to state.

Effect rows also improve maintainability: when a function's effects change, every caller still declaring the old ones stops compiling.

Tools

Algebraic effects (modern flavor)

  • Koka (Leijen 2014)1 — row-polymorphic algebraic effects; designed to show what a fully effect-typed language looks like in practice. Built-in effects: total, exn, div, ndet, alloc⟨h⟩, read⟨h⟩, write⟨h⟩, io, console.
  • Effekt — modern algebraic-effects language with second-class capabilities and practical ergonomics; handler scopes are guaranteed safe.
  • Frank — strict, call-by-push-value effects-and-handlers language.
  • Eff — research language; the design ancestor for many modern algebraic-effect implementations.

Algebraic effects in mainstream languages

  • Multicore OCaml (production OCaml since 5.0) — user-defined effects with handlers; backed by an effect-tracking type system.
  • Unison — abilities (Unison's term for algebraic effects) are a first-class language feature; the content-addressed code store ensures effect types are stable across versions.

Effect tracking via monads

  • Haskell monads — the long-standing way to track effects in a type system; IO, ST, State, Reader, monad transformers, mtl-style classes. More cumbersome than algebraic effects but the most-deployed effect tracking in mainstream code.
  • Scala with Cats Effect, ZIO, Kyo — monad-based effect systems; ZIO's ZIO[R, E, A] makes resources, errors, and result type explicit in every signature.
  • PureScript — Haskell-style purity in a TypeScript-target language; effects via Effect a and Aff a.

Effects in dependently-typed / verification languages

  • F* (Project Everest) — effects are first-class and the effect system supports refinement reasoning. See refinement and dependent types.
  • Idris 2 — effects via algebraic-effect handlers; useful as a teaching example because the syntax is gentler than F*'s.

When to use, when not

Use:

  • New systems where pure-vs-effectful boundary maintenance is worth the static-checking cost — verified protocols, financial code, code where reasoning about effects matters more than syntactic convenience.
  • Languages where algebraic effects are first-class (Koka, Effekt, Multicore OCaml, Unison). The ergonomic gap vs monadic effects is closing.
  • Verified systems programming. F*'s effect system carries proof obligations alongside ordinary type-checking; see theorem proving.
  • Per-axis test planning. An effect system makes the code's effect a property of the signature; the test plan reads it off the type.

Don't:

  • In a codebase that's already getting value from a simpler type system. The ergonomic cost of adding monadic-style effect tracking to a mainstream stack is high; consider runtime capability-passing patterns (constructor injection, reader contexts) first.
  • As a substitute for testing. Effect tracking proves what the function can do, not what it does correctly.
  • For one-off scripts. The ceremony exceeds the value.

Evidence

  • Multicore OCaml shipped algebraic effects in production OCaml 5.0 (2022), establishing that the mechanism is implementable in a mainstream typed language.
  • F* / Project Everest. F*'s dependent types and multi-monadic effects verified key portions of an existing TLS 1.2 implementation (Swamy et al. 2016)2.

No controlled comparison of effect-tracked against effect-untracked code is cited here. The definitional point carries the method — an effect system rules out unintended effects by construction — and the implementations named answer cost rather than efficacy.

Classification

  • Quality dimensions: Functionality, Maintainability (effect-boundary refactor-safety — changing what a function does breaks mismatched callers at compile time).
  • Area: Pure-vs-effectful boundary maintenance, concurrency and async code, exception discipline, verified systems programming, language design for testability.
  • Guarantee: Mathematical when paired with a proof assistant (F*, Dafny, Verus); Exhaustive within what a plain effect system can express.

Referenced by

References

  1. Leijen, Daan. 2014. "Koka: Programming with Row Polymorphic Effect Types." Proceedings of MSFP 2014 (Mathematically Structured Functional Programming) 153: 100–126. https://doi.org/10.4204/EPTCS.153.8. ↩

  2. Swamy, Nikhil, Cătălin Hriţcu, Chantal Keller, et al. 2016. "Dependent Types and Multi-Monadic Effects in F*." Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '16), 256–70. https://doi.org/10.1145/2837614.2837655. ↩