Log in

No account? Create an account




July 1st, 2019

Handlers in Action

Effect Handlers, Monadic Reflection, Delimited Control



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.
Powered by LiveJournal.com