Efficient strong functional programming with effects and compiler guided reference counting
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.
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.