Koka

Koka is a strongly-typed, functional programming language developed at Microsoft Research by Daan Leijen. It is best known for two intertwined research contributions: a sophisticated effect type system based on row polymorphism with first-class algebraic effect handlers, and Perceus, a precise compile-time reference counting scheme that delivers garbage-collection-free memory management for a higher-order functional language. The name “Koka” (効果) is the Japanese word for “effect,” underscoring the language’s central focus.

History & Origins

Koka emerged in the early 2010s out of Daan Leijen’s work at Microsoft Research. Leijen, who is also known for prior work on libraries and languages such as the Parsec parser combinator library, set out to design a language where the side effects of expressions are tracked precisely in the type system, without imposing the syntactic overhead that pure monadic programming in Haskell sometimes requires.

The first public technical materials on Koka appeared around 2012, and the foundational paper, Koka: Programming with Row-Polymorphic Effect Types, formalized the approach in 2014. Whereas Haskell encodes effects via monads as data, Koka instead annotates every function’s type with a row of effects — an open set of labels such as exn (exceptions), io, div (divergence), or ndet (nondeterminism). This row-polymorphic approach allows generic code to be polymorphic in the effects it permits, much as System F-style polymorphism allows polymorphism in types.

In 2016, Leijen introduced algebraic effect handlers as a first-class language feature in Koka. Algebraic effects, popularized by Plotkin, Power, Pretnar, and Bauer in the Eff language, give programmers a structured, composable alternative to monads for expressing effects like state, exceptions, async/await, generators, and nondeterminism. Koka was one of the first practical languages to integrate handlers with a complete effect type system.

A second major phase began in 2020 with Koka 2.0. The compiler was substantially rewritten to target C as a backend, and the language introduced Perceus, a reference counting system with reuse analysis that allows pure functional code to be compiled to efficient, often in-place, low-level code. The Perceus work was published at PLDI 2021.

Design Philosophy

Koka is shaped by a small set of strong convictions about what a modern functional language should be.

Effects in the Type System

In Koka, every function type carries an effect annotation. A pure function from integers to integers has type int -> int, while a function that might throw an exception has type int -> exn int, and one that performs I/O has type int -> io int. The compiler infers these effects, so the programmer rarely writes them explicitly, but they are always present and checked.

This makes effects first-class properties of code: a function’s signature documents exactly what it can do.

Algebraic Effects and Handlers

Rather than baking specific effects (exceptions, mutable state, async) into the language, Koka lets programmers define effects and their operations, then write handlers that interpret them. A handler is essentially a structured form of delimited continuation: when an operation is invoked, control transfers to the nearest enclosing handler, which can resume the computation zero, one, or many times.

effect ask<a>
  ctl ask() : a

fun add-asked() : <ask<int>> int
  ask() + ask()

fun main()
  with handler
    ctl ask() resume(42)
  add-asked().println

This style unifies exceptions, generators, async, backtracking, and many other control patterns under a single, well-typed mechanism.

Perceus and FBIP

Unlike most functional languages, Koka does not use a tracing garbage collector. Instead, the compiler inserts precise reference count increments and decrements at compile time using the Perceus algorithm. When the compiler can prove that a value’s reference count will drop to one, it generates code that reuses the existing memory for a new value of similar shape — turning what would be allocation and freeing into in-place update.

This enables a programming style Koka calls FBIP — Functional But In-Place. Algorithms written in a purely functional style (immutable trees, lists, etc.) can compile to code with performance comparable to careful imperative implementations, without sacrificing referential transparency in the source.

Minimal Syntax

Koka’s surface syntax aims to be light and readable, with significant emphasis on dot notation for function chaining. list.map(f).filter(p).sum reads left-to-right and desugars to ordinary function application. Statements use indentation-sensitive blocks, and lambdas can be passed as trailing blocks similar to Kotlin or Ruby.

Key Features

Row-Polymorphic Effect Types

Effects in a Koka type are rows — extensible sets of labels:

fun safe-div(x : int, y : int) : exn int
  if y == 0 then throw("division by zero")
  else x / y

A function polymorphic over its effect row can be reused in pure, exception-throwing, or I/O-performing contexts alike.

User-Defined Effects

Programmers can declare new effects and operations, then implement handlers in user code:

effect state<s>
  fun get() : s
  fun set(x : s) : ()

A state handler can implement this by threading a value through resumes, giving mutable-state semantics without the language itself supporting mutation.

Pattern Matching and ADTs

Koka has algebraic data types, pattern matching with exhaustiveness checking, and generic types:

type tree<a>
  Leaf
  Node(left : tree<a>, value : a, right : tree<a>)

Type Inference

Hindley-Milner-style inference is extended to cover effect rows, so most function signatures can be omitted while still benefiting from the full effect discipline.

C, JavaScript, and WebAssembly Backends

The current Koka compiler primarily targets C, producing native executables that link against a small runtime implementing Perceus. Earlier and alternative backends target JavaScript, and experimental WebAssembly support has been explored.

Evolution

Version numbers and dates for ongoing releases should be cross-checked against the official Koka repository, as the language is under active research-driven development.

Current Relevance

Koka remains primarily a research language, but its ideas have had outsized influence on the broader programming language community:

• Algebraic effects have moved from a niche research topic to a feature in mainstream languages. OCaml 5 introduced effect handlers in 2022, and languages like Effekt, Eff, and Frank draw directly on the same line of work that Koka helped popularize.
• Perceus-style reference counting has influenced memory management designs in other modern languages, notably Roc, whose designers have cited Koka’s work as an influence on their reuse-based memory model.
• Effect typing as documentation and safety is increasingly seen as a desirable feature, with proposals for effect tracking appearing in ecosystems ranging from Scala to Rust.

The language is developed openly on GitHub under Microsoft, with documentation, a tutorial, a standard library, and a VS Code extension. Its community is small relative to mainstream languages but highly active in academic and research settings.

Why It Matters

Koka’s importance lies less in widespread industrial adoption and more in the ideas it has proven viable:

1. Effects as types: Koka demonstrated that a full-featured effect type system can coexist with practical programming, type inference, and good ergonomics — without forcing programmers into monadic plumbing.
2. Algebraic effects, productized: While effect handlers originated in academic languages, Koka was among the first to make them feel like a natural part of a general-purpose language.
3. GC-free functional programming: Perceus showed that a higher-order, immutable-by-default language can be compiled to fast, predictable, GC-free code, challenging the assumption that functional languages must rely on tracing collectors.
4. A research bridge: Koka serves as a meeting point between programming language theory and language engineering, with ideas flowing from papers to a working compiler and back to influence other industrial languages.

For programmers interested in the future of functional programming — effect systems, compile-time memory management, and the relationship between mathematical purity and machine efficiency — Koka is one of the most consequential research languages of the 2010s and 2020s.