Koka: Programming with Row-Polymorphic Effect Types

Note: This is an updated article: a previous version of this article contained a wrong lemma and corresponding mistakes in various proofs of Section 5.

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.