Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala. (31st March 2020)

• Record Type: Journal Article
• Authors: BRACHTHÄUSER, JONATHAN IMMANUEL; SCHUSTER, PHILIPP; OSTERMANN, KLAUS
• Is Part Of: Journal of functional programming. Volume 30(2020)
• Publication Date: 2020-03-31
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796820000027
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: 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 using intersection types and path-dependent types. The effect system of our library design fits well into the programming paradigm of capability passing and is inspired by the effect system of Zhang & Myers (2019, Proc. ACM Program. Lang. 3 (POPL), 5:1-5:29). Capabilities carry an abstract type member, which represents an individual effect type and reflects the use of the capability on the type level. We represent effect rows as the contravariant intersection of effect types. Handlers introduce capabilities and remove components of the intersection type. Reusing the existing type system of Scala, we get effect subtyping and effect polymorphism for free.