Effekt: Type- and Effect-safe, Extensible Effect Handlers in Scala
by Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann
Unpublished. Under consideration for publication in Journal of Functional Programming, 2019.
This publication is related to the Effekt: Algebraic Effect Handlers research project.
Effect handlers are a promising way to structure effectful programs in a modular way. We present the Scala library Effekt, which is centered around capability passing and implemented in terms of a monad for multi-prompt delimited continuations. Effekt is the first library implementation of effect handlers that supports effect safety and effect polymorphism without resorting to type-level programming. We describe a novel way of achieving effect safety by using intersection types and path-dependent types. The effect system of our library design fits fits well into the programming paradigm of capability passing and is inspired by the effect system of Zhang & Myers (2019). We represent effect rows as the contravariant intersection of effect types, where an individual effect is represented by the singleton type of the capability. Handlers remove components of the intersection type. By reusing the existing type system of Scala, we get effect subtyping and effect polymorphism for free.