一句话：提出 λ_HEL 演算及存在/局部代数效应，用类型化运行时强制转换保障效应抽象不被破坏。
代数效应与处理器是当前函数式语言中处理异常、可变状态、非确定性等计算效应的前沿方法，但要在大型模块化程序中推广，需要能隐藏或隔离效应的抽象机制。本文提出两种机制：存在效应（向用户隐藏特定效应细节）与局部效应（保证外部代码无法干扰给定效应）。技术难点在于执行期效应操作与正确处理器的动态耦合；作者设计了带局部与存在代数效应的 λ_HEL 演算，并用类型化运行时强制转换约束处理器的动态行为，使类型系统保证抽象不被破坏。作为概念验证，他们实现了基于该演算的实验语言，以 ML 风格模块系统提供强抽象机制。
Proposed originally by Plotkin and Pretnar, algebraic effects and their handlers are a leading-edge approach to computational effects: exceptions, mutable state, nondeterminism, and such. Appreciated for their elegance and expressiveness, they are now progressing into mainstream functional programming languages. In this paper, we introduce and examine programming language constructs that back adoption of programming with algebraic effects on a larger scale in a modular fashion by providing mechanisms for abstraction. We propose two such mechanisms: existential effects (which hide the details of a particular effect from the user) and local effects (which guarantee that no code coming from the outside can interfere with a given effect). The main technical difficulty arises from the dynamic nature of coupling an effectful operation with the right handler during execution, but, as we show in this paper, a carefully designed type system can ensure that this will not break the abstraction. Our main contribution is a novel calculus for algebraic effects and handlers, called λ HEL , equipped with local and existential algebraic effects, in which the dynamic nature of handlers is kept in check by typed runtime coercions. As a proof of concept, we present an experimental programming language based on our calculus, which provides strong abstraction mechanisms via an ML-style module system.
@article{paperbot678,
title = {Abstracting algebraic effects},
author = {Dariusz Biernacki and Maciej Piróg and Piotr Polesiuk and Filip Sieczkowski},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290319}
}