# 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 `` 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](https://koka-lang.github.io/koka/doc/index.html)** (Leijen 2014)[^leijen2014] — 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](https://effekt-lang.org/)** — modern algebraic-effects language with second-class capabilities and practical ergonomics; handler scopes are guaranteed safe. - **[Frank](https://github.com/frank-lang/frank)** — strict, call-by-push-value effects-and-handlers language. - **[Eff](https://www.eff-lang.org/)** — research language; the design ancestor for many modern algebraic-effect implementations. ### Algebraic effects in mainstream languages - **[Multicore OCaml](https://ocaml.org/manual/effects.html)** (production OCaml since 5.0) — user-defined effects with handlers; backed by an effect-tracking type system. - **[Unison](https://www.unison-lang.org/)** — 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](https://project-everest.github.io/)) — effects are first-class and the effect system supports refinement reasoning. See [refinement and dependent types](https://quality.stereobooster.com/refinement-and-dependent-types.md). - **[Idris 2](https://www.idris-lang.org/)** — 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](https://quality.stereobooster.com/theorem-proving.md). - Per-axis test planning. An effect system makes the code's [effect](https://quality.stereobooster.com/effect.md) 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)[^swamy2016]. 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](https://dafny.org/), [Verus](https://github.com/verus-lang/verus)); Exhaustive within what a plain effect system can express. ## Referenced by - [Effect scope](https://quality.stereobooster.com/effect.md) · The axes - [Types and effects](https://quality.stereobooster.com/types.md) · Methods - [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI ## References [^leijen2014]: Leijen, Daan. 2014. "[Koka: Programming with Row Polymorphic Effect Types](https://arxiv.org/pdf/1406.2061)." *Proceedings of MSFP 2014 (Mathematically Structured Functional Programming)* 153: 100–126. . [^swamy2016]: Swamy, Nikhil, Cătălin Hriţcu, Chantal Keller, et al. 2016. "[Dependent Types and Multi-Monadic Effects in F\*](https://hal.science/hal-01265793/document)." *Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '16)*, 256–70. .