Koka
Research language from Microsoft that tracks side effects in the type system using algebraic effects and handlers.
static
compiled
since 2012
functionaleffect-oriented
Koka’s type system tracks all side effects — exceptions, state, I/O, concurrency — as first-class row-typed effect labels. Algebraic effect handlers provide a structured way to implement custom control flow, coroutines, and exception systems. Koka pioneered Reuse Analysis, a compile-time technique for in-place mutation of functional data structures that Lean 4 and other languages have adopted.