Let’s take a journey through the foundational features that set Koka apart as a modern day functional language. Along the way we also take a detour into mimalloc, one of the world’s fastest industrial strength memory allocators (and a spin-off of the Koka project).

A core part of Koka is a sound type- and effect system that gives strong guarantees at compile time. The compiler in turn uses these guarantees in various novel ways to improve runtime performance – an intricate co-design of language and compiler.

For example, many functional languages use generational garbage collection for automatic memory management, which can lead to increased memory usage and/or unpredictable runtime pauses. In contrast, Koka uses compiler guided reference counting (Perceus) that uses standard malloc and free. This in turn allows Koka to compile many allocations into in-place updates at runtime instead, which can significantly increase performance for many functional style algorithms.

Particular topics that we hope to cover are:

  • Perceus: compiler guided reference counting as an alternative to garbage collection. This includes an overview of the core tricks in mimalloc, a fast scalable memory allocator which is widely used in the industry as a drop-in malloc/free replacement.
  • FBIP: functional-but-in-place programs which are guaranteed not to allocate.
  • First-class constructor contexts for efficient top-down algorithms.
  • Static Overloading with syntactic implicits as an alternative to type classes.
  • Algebraic effect handlers as an alternative to monads.

https://koka-lang.github.io/koka/doc/book.html

I am a member of the Research In Software Engineering (RISE) group at Microsoft Research, and interested in the design and application of strong type systems, declarative programming, and compiler technology. In particular, I work on the Koka language (and mimalloc) where I explore programming with algebraic effect handlers, effect typing, Perceus precise reference counting, and pure functional programming with high performance.