Koka: Programming with Row Polymorphic Effect Types

TL;DR

Koka introduces a type system that explicitly models effects with row polymorphism, enabling automatic inference, safe encapsulation of state, and clear effect signatures, demonstrated through a new language implementation.

Contribution

The paper presents a novel effect system with row polymorphism supporting polymorphic effects and deep semantic connections, implemented in the Koka language.

Findings

Effect types are automatically inferred and semantically meaningful.

Safe encapsulation of stateful operations without traditional restrictions.

Successful application of the system in various practical programs.

Abstract

We propose a programming model where effects are treated in a disciplined way, and where the potential side-effects of a function are apparent in its type signature. The type and effect of expressions can also be inferred automatically, and we describe a polymorphic type inference system based on Hindley-Milner style inference. A novel feature is that we support polymorphic effects through row-polymorphism using duplicate labels. Moreover, we show that our effects are not just syntactic labels but have a deep semantic connection to the program. For example, if an expression can be typed without an exn effect, then it will never throw an unhandled exception. Similar to Haskell's `runST` we show how we can safely encapsulate stateful operations. Through the state effect, we can also safely combine state with let-polymorphism without needing either imperative type variables or a syntactic value restriction. Finally, our system is implemented fully in a new language called Koka and has been used successfully on various small to medium-sized sample programs ranging from a Markdown processor to a tier-splitted chat application. You can try out Koka live at www.rise4fun.com/koka/tutorial.