Type Directed Compilation of Row-typed Algebraic Effects
Algebraic effect handlers are recently gaining in popularity as a purely functional approach to modeling effects. As a restriction on general monads, algebraic effects come with various advantages: they can be freely composed, and there is a natural separation between their interface (as a set of operations) and their semantics (as a handler).
In this talk, I give an end-to-end overview of practical algebraic effects in the context of a compiled implementation in the Koka language. I’ll present a language design for algebraic effects, and show how algebraic effects subsume many control-flow constructs that are specialized in other languages, e.g. exceptions, state, iterators, async-await, etc. In particular, iterators and async-await are complex constructs that can lead to subtle interactions with other features and require complex compilation mechanisms. Being able to generalize over them using a single well-founded abstraction is a huge win.
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.
Sun 18 SepDisplayed time zone: Osaka, Sapporo, Tokyo change
15:30 - 16:30
|Type Directed Compilation of Row-typed Algebraic Effects
Daan Leijen Microsoft ResearchLink to publication
|Administrative normal form, continued: Sharing control in direct style