# Koka: Programming with Row Polymorphic Effect Types

arXiv: https://arxiv.org/abs/1406.2061 · HTML: https://mlsanity.com/paper/1406.2061/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Jun 2014.

## Built on by (most cited first, 3 of 3)

- [Coop: Memory is not a Commodity](https://mlsanity.com/paper/2311.00591/) (2023)
- [Towards Automated Formal Verification of Backend Systems with LLMs](https://mlsanity.com/paper/2506.10998/) (2025)
- [ETAS: An Effect-Typed Language for Agent Systems](https://mlsanity.com/paper/2607.17780/) (2026)

## Abstract (arXiv)

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.