Koka v3 is a research language that is currently under development and not quite ready for production use.

Latest release: v3.2.9, 2026-09-17

(Install).

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 is an advanced compilation method for reference counting. Together with evidence passing, this lets Koka compile directly to C code without needing a garbage collector or runtime system. Perceus also performs reuse analysis and optimizes functional-style programs to use in-place updates when possible.

To learn more:

• Install Koka and compile your first programs.
• Read the Koka book for a tour of the Koka language and its specification.
• Browse the library documentation.
• Help with development

Enjoy, Daan Leijen

Special thanks to: Tim Whiting and Fredrik Wieczerkowski for their work on the VS Code language integration, Anton Lorenzen for his work on one-hole context (pdf), fully in-place programming [11] and frame-limited reuse in Perceus [10], Ningning Xie for her work on the theory and practice of evidence passing [9,6] and the formalization of Perceus reference counting [8], Alex Reinking for the implementation of the Perceus reference counting analysis