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 practical implementation of effect handlers that supports effect safety, effect polymorphism, effect parametricity, and effect encapsulation which means that all effects are handled and effects cannot be accidentally handled by the wrong handler. Other existing languages and libraries break effect encapsulation by leaking implementation details in the effect type unless the user manually adds lifting annotations. We describe a novel way of achieving effect-safety using intersection types and path dependent types. We represent effect rows as the contravariant intersection of effect types, where an individual effect is represented by the singleton type of its capability. Handlers remove components of the intersection type. By reusing the existing type system we get subtyping and polymorphism of effects for free. The effect system not only guarantees safety, but also guarantees modular reasoning about higher-order effectful programs.