一句话：提出 Scala 库 Effekt，以能力传递与交叉/路径依赖类型实现支持效应安全和效应多态、无需类型级编程的效应处理器。
效应处理器为模块化组织效应程序提供了有前景的途径，但库实现常难以同时保证效应安全与效应多态，或需依赖类型级编程。本文提出 Scala 库 Effekt，其核心是能力传递，并基于多提示定界续延的 monad 实现。作者设计了一种利用交叉类型与路径依赖类型的新方法来实现效应安全：能力携带抽象类型成员，表示单个效应类型并在类型层面反映能力使用；效应行表示为效应类型的逆变交叉，处理器引入能力并移除交叉类型的组件。该设计受 Zhang & Myers（2019）效应系统启发，复用 Scala 现有类型系统自然获得效应子类型和效应多态。Effekt 是首个无需类型级编程即可支持效应安全与效应多态的效应处理器库实现。
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.
@article{BrachthauserSO20,
title = {Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala},
author = {JONATHAN IMMANUEL BRACHTHÄUSER and PHILIPP SCHUSTER and KLAUS OSTERMANN},
journal = {Journal of Functional Programming},
volume = {30},
year = {2020},
doi = {10.1017/s0956796820000027}
}