Koka

Koka is a statically typed functional programming language developed by Daan Leijen at Microsoft Research, designed around algebraic effects and handlers as its core abstraction for computational effects. Unlike languages that treat effects as built-in primitives or monadic encodings, Koka builds effect tracking directly into its type system: every function carries an effect row in its type signature, making visible not only what a function returns but what effects it may perform.

This effect-tracking type system enables Koka to guarantee that pure functions are truly pure — they perform no I/O, no mutation, no exceptions — while still allowing effectful code to be written in direct style. The compiler uses this information for aggressive optimizations, including automatic parallelization and tail-call optimization, that would be unsafe in languages without effect tracking.

Koka demonstrates that algebraic effects can be implemented with performance competitive to mainstream languages. Its significance lies in bridging the gap between research concepts and practical engineering: it is a proof that effect handlers need not be slow, and that effect tracking need not burden the programmer with excessive annotation.