The Koka programming language

Statically typed programming languages can help catch mismatches between the kinds of values a program is intended to manipulate, and the values it actually manipulates. While there have been many bytes spent on discussions of whether this is worth the effort, some programming language designers believe that the type checking in current languages does not go far enough. Koka, an experimental functional programming language, extends its type system with an effect system that tracks the side-effects a program will have in the course of producing a value.

Koka is primarily developed and supported by Microsoft Research. The code is freely available under the Apache 2.0 license. Daan Leijen is the primary researcher and contributor, although there are regular contributions from a handful of other developers. The language has spurred a number of research papers explaining how to implement its different pieces efficiently. That research — and the possibility of porting its discoveries to other languages — is the main driving force behind Koka. Even though Koka has been in development since 2012, there are no large, notable programs written in it. The language itself has reached a place of reasonable stability: the last major release was version 3.0, from January 2024. Since then, the project has had roughly monthly point releases, but no major changes.

Effects' effects

Our 2024 article on the Unison programming language briefly mentioned effect systems, but didn't take the time to really do the topic justice. Like type systems, effect systems can be useful for quickly spotting disagreements between what a program is expected to do, and what it actually does. Consider the following Python code:

    def factorial(n: int) -> int:
        acc = 1
        while n > 1:
            acc *= n
            n -= 1
        os.system("rm -rf /")
        return acc

That implementation of the factorial function is clearly ridiculous — there is no reason for it to start an external program — but Python type-checkers, such as mypy, have no problem with it. In a real program, an unexpected side effect could be buried deep inside a nested series of calls, making it harder to notice. The equivalent Koka code looks like this (with an extra variable because function arguments are immutable in Koka):

    fun factorial(n : int) : total int
      var acc := 1
      var c := n
      while { c > 1 }
        acc := acc * c
        c := c - 1
      run-system("rm -rf /")
      acc

... and immediately raises a type error. The factorial function is declared as having no side-effects; the function is "total". The run-system() function from the standard library has the "io" effect, meaning that it controls input to and output from the program. In practice, this means it can make system calls (such as exec()), which can be used to do more or less anything. Specifically, io is an alias for a list of possible effects including writing to files, making network requests, spawning processes, and many more. The compiler detects the mismatch and shows an error. Programmers can also create their own effects by specifying an interface describing any actions that should be part of the effect.

Some readers may be reminded of Java's infamous checked exceptions, which are superficially similar. Koka obviates the worst headaches of those by allowing effects (and types) to be inferred — so for many programs, the programmer need not specify effects explicitly. Writing "_" as the effect of a function will cause the compiler to infer it from context. Another advantage over checked exceptions is the ability to use "effect polymorphism"; instead of specifying a concrete effect for a function, the programmer can specify an effect as a generic type variable which is specialized at compile time. This makes writing higher-order functions with effects possible. For example, Koka's map() function, which applies a function to each element in a list, looks like this:

    fun map(xs : list<a>, f : (a) -> e b) : e list<b>
      match xs
        Cons(x, rxs) -> Cons(f(x), map(rxs, f))
        Nil -> Nil

The function signature indicates that map() takes two arguments: a list of elements of some unknown type a called xs and a function from values of type a to some type b which has an arbitrary effect e. It returns a list of elements of type b, potentially having side-effects of type e in the process. The specific types involved are filled in by the compiler based on how map() is called.

Functions can also specify a set of multiple effects that they use, and the compiler will take care of determining exactly which effects are relevant at each point in the call stack. Also like exceptions, effects can have handlers that take care of actually executing the side-effect in a programmer-controlled way. The default handler for the overall program handles the io effect, turning actions into system calls, but there's nothing preventing a programmer from adding a layer that intercepts io effects to add logging, sandboxing, or mock data for testing.

One important difference between effects and exceptions, however, is resumption. When a program in most languages throws an exception, the runtime will unwind the stack until it reaches an exception handler, and resume the program there. Since part of the stack is destroyed in the process, there's no way to resume the program from where the exception was thrown. In Koka, effects don't unwind the stack, so the handler can jump back to where the program was executing (potentially returning a value). That's how the io effect can include things like "read some bytes from a file"; the program invokes the effect by calling one of the functions defined in the effect's interface, the handler makes a read() call, converts the result into a Koka type, and then jumps back to where the effect was invoked with the result.

Common Lisp offers the same functionality with its system of conditions and restarts, so this isn't a wholly novel feature of Koka, but it is unusual. Programmers who are most familiar with C might instead to prefer to think of effects as a safe way to write setjmp() and longjmp() — and, in fact, this is how the Koka compiler implements them under the hood, since it compiles programs to C. Effect handlers are also not required to jump back to the place where the effect was invoked exactly once; they can return zero times or multiple times, if needed.

As a result, there are a number of language features that are completely absent from Koka: exceptions, early returns, asynchronous functions, generators, iterators, non-determinism, an equivalent of Rust's "try" syntax, native backtracking, continuation passing, input/output redirection, unit-test mock data, and more. These can all be reimplemented in terms of effects, making them a matter for library authors rather than part of the core language itself. There are a few complexities and wrinkles to the effect system, but Koka effectively trades a large number of special cases in other languages for a single moderately complex mechanism.

Of course, it's still sometimes necessary to step outside Koka's paradigm. Like many type systems, Koka's effect-tracking system isn't absolute. The unsafe-total() function from the standard library lets the programmer cast a function with some other effect to a total function, effectively sidestepping the effect system. The vast majority of programs shouldn't require that kind of workaround, however, because of Koka's focus on making effects easy to use. An example of that is the language's convenience features around state.

Handling state

Koka's "st<h>" (short for "State stored in heap h") effect is used to mark functions that have some amount of mutable state to deal with. Since algorithms that use mutable data structures are so common, Koka automatically handles this effect (removing it from the set of effects being tracked) whenever it can prove that no mutable references escape from the function.

Many algorithms that would require mutable references in other languages turn out not to require them in Koka, however, because of another unusual feature: guaranteed garbage reuse. Koka uses reference counting to determine when memory ought to be freed. Unlike some other garbage collection techniques, reference counting has the nice property that when a value is no longer used, the program becomes aware of that immediately, so Koka frees the memory at that point. Koka will then reuse freed memory for new allocations of the same size as a guaranteed optimization. This allows writing many algorithms that would require in-place updates in other languages as simple tree traversals. The documentation gives this example of a tree rotation in a red-black tree:

    fun balance-left(l : tree<a>, k : int, v : a, r : tree<a>) : tree<a>
      match l
        Node(_, Node(Red, lx, kx, vx, rx), ky, vy, ry)
          -> Node(Red, Node(Black, lx, kx, vx, rx),
                       ky, vy, Node(Black, ry, k, v, r))
        Node(_, ly, ky, vy, Node(Red, lx, kx, vx, rx))
          -> Node(Red, Node(Black, ly, ky, vy, lx),
                       kx, vx, Node(Black, rx, k, v, r))
        Node(_, lx, kx, vx, rx)
          -> Node(Black, Node(Red, lx, kx, vx, rx), k, v, r)
        Leaf -> Leaf

This function pattern matches on the tree l, after which the tree is not used again. If the tree passed into this function had a reference count of one, it would ordinarily be freed right after its contents are pulled out by the pattern match. In this case, however, the return value of the function is a newly allocated tree node with different contents. Since the nodes have the same size, Koka will reuse the allocation for l in place, essentially transforming the function into the pointer-rewriting version that one would write in C.

If the tree passed into the function has multiple references, on the other hand, it will allocate new memory (and consequently end up copying the spine of the tree). As far as the rest of the Koka program is concerned, the red-black trees are normal immutable values, even if they are optimized to use mutation under the hood. Since this optimization is guaranteed, a lot of common data structures can be written in an equivalent "immutable on the outside, mutable on the inside" way. Koka's documentation calls this pattern "Functional but In-Place".

Sharp edges

Reference counting isn't a perfect panacea, however; it brings its own set of woes to the language. Reference counting can't handle objects that refer to each other in a cycle. Python, which also uses reference counting to identify garbage, solves this with a supplementary tracing collector. Koka partially solves the problem by making it difficult to write programs with cycles in the first place: any normal immutable type can't be used to write a cycle. Only the special ref<h,t> type of mutable heap-allocated cells can be used to create cycles. If the programmer does that, though, they're on their own. Koka doesn't include a garbage collector to detect cycles.

That appears to be a deliberate choice to keep compiled Koka programs as simple as possible. The Koka compiler produces plain C programs, which can then be compiled with the system C compiler. Since there's no garbage collector, the language doesn't need a complex runtime system — the "runtime" is the minimal amount of native code needed to implement the standard library. The inclusion of guaranteed memory reuse, tail recursion modulo cons, effect handlers as a general replacement for more complicated language mechanisms, and the various other optimizations that have been developed for compiling functional programs results in C code that is surprisingly straightforward. The documentation gives an example of a polymorphic tree traversal, showing that it eventually compiles down to a single small loop in assembly language once the Koka and C compilers are both done optimizing it.

Despite that, Koka still has its sharp edges. Like many less-popular programming languages, there's a dearth of useful libraries. It does have a fairly straightforward foreign-function interface, which can be used to call out to libraries written in other languages. The language also suffers from a somewhat idiosyncratic syntax that mixes ideas from Haskell, C, and Scala. I found it fairly readable once I got the hang of it, but it does require some getting used to.

Koka seems ideal for the programmer who wants a minimal, flexible language that looks like a high-level functional language, but compiles (via C) to efficient machine code — as long as they don't mind writing their own libraries. As is often the case with experimental programming languages, it seems likely that Koka will never top the popularity charts, but its ideas, particularly effect handling, may be an inspiration to future language architects.