Type Directed Compilation of Row-Typed Algebraic Effects
Proceedings of Principles of Programming Languages (POPL'17), Paris, France |
Algebraic effect handlers, are recently gaining in popularity as a
purely functional approach to modeling effects. In this article, we
give an end-to-end overview of practical algebraic effects in the
context of a compiled implementation in the Koka language. In
particular, we show how algebraic effects generalize over common
constructs like exception handling, state, iterators and async-await.
We give an effective type inference algorithm based on extensible
effect rows using scoped labels, and a direct operational semantics.
Finally, we show an efficient compilation scheme to common runtime
platforms (such as JavaScript, the JVM, or .NET) using a type
directed selective CPS translation.