Koka

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:

• Why Koka? (opens in new tab)
• The Koka book (opens in new tab) for a tour of the Koka language and its specification.
• Browse the repository at github.com/koka-lang/koka (opens in new tab)