Koka

Established: April 13, 2012

Koka is a strongly typed functional-style language with effect types and handlers.

  • The core of Koka consists of a small set of well-studied language features, like first-class functions, a polymorphic type- and effect system, algebraic data types, and effect handlers. Each of these is composable and avoid the addition of “special” extensions by being as general as possible.
  • Koka tracks the (side) effects of every function in its type, where pure and effectful computations are distinguished. The precise effect typing gives Koka rock-solid semantics backed by well-studied category theory, which makes Koka particularly easy to reason about for both humans and compilers.
  • Effect handlers let you define advanced control abstractions, like exceptions, async/await, or probabilistic programs, as a user library in a typed and composable way.
  • Perceus (opens in new tab) is an advanced compilation method for reference counting. Together with evidence translation (opens in new tab), this lets Koka compile directly to C code without needing a garbage collector or runtime system. Perceus also performs reuse analysis (opens in new tab) and optimizes functional-style programs to use in-place updates when possible.

For more information, see:

People

Portrait of Daan Leijen

Daan Leijen

Principal Researcher