Koka: Programming with Row Polymorphic Effect Types

Daan Leijen


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 http://www.rise4fun.com/koka/tutorial.


Publication typeInproceedings
Published inMathematically Structured Functional Programming 2014

Previous versions

Daan Leijen. Koka: Programming with Row-Polymorphic Effect Types, 28 August 2013.

> Publications > Koka: Programming with Row Polymorphic Effect Types