Algebraic effect handlers, introduced by Plotkin and Power in 2002, are recently gaining in popularity as a purely functional approach to modeling effects. In this article, we give a full 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 (like JavaScript) using a type directed selective CPS translation.
I am a member of the Research In Software Engineering (RISE) group and chair of the Programming Languages working group (PLX). Currently, I am interested in the design and application of strong type systems and declarative programming languages, like Haskell. In particular, I am interested in programming with Effect inference in the Koka project. Furthermore, I work on domain specific embedded languages, language design, and compiler technology.
Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:20 - 16:00 | |||
14:20 25mTalk | Type Directed Compilation of Row-Typed Algebraic Effects POPL Daan Leijen Microsoft Research | ||
14:45 25mTalk | Do be do be do POPL | ||
15:10 25mTalk | Dijkstra Monads for Free POPL Danel Ahman University of Edinburgh, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris, ENS Paris, and Microsoft Research, Guido Martínez CIFASIS-CONICET, Argentina, Gordon Plotkin , Jonathan Protzenko Microsoft Research, Aseem Rastogi Microsoft Research India, Nikhil Swamy Microsoft Research Pre-print | ||
15:35 25mTalk | Stateful Manifest Contracts POPL |