一句话：提出用词法作用域 handler 为代数效应实例命名并在类型中追踪，从而在同一上下文中组合同一效应的多次使用。
代数效应 handler 要成为实用构造，仍难在同一程序中组合同一效应的不同使用，尤其在静态类型-效应系统中：例如把可变内存单元定义为 put/get 及其 handler 后，难以在单一上下文中操作多个内存单元。本文提出词法作用域效应，每个效应实例由名字标识，由外层 handler 绑定并在表达式类型中追踪。该设定需处理效应、多态与 binder 下归约的复杂交互；作者为此发展了可处理开放项的 Kripke 风格逻辑关系，证明演算所需性质。核心结果在 Coq 中形式化，并实现实验性表层语言以展示实用性。
Handlers of algebraic effects aspire to be a practical and robust programming construct that allows one to define, use, and combine different computational effects. Interestingly, a critical problem that still bars the way to their popular adoption is how to combine different uses of the same effect in a program, particularly in a language with a static type-and-effect system. For example, it is rudimentary to define the “mutable memory cell” effect as a pair of operations, put and get , together with a handler, but it is far from obvious how to use this effect a number of times to operate a number of memory cells in a single context. In this paper, we propose a solution based on lexically scoped effects in which each use (an “instance”) of an effect can be singled out by name, bound by an enclosing handler and tracked in the type of the expression. Such a setting proves to be delicate with respect to the choice of semantics, as it depends on the explosive mixture of effects, polymorphism, and reduction under binders. Hence, we devise a novel approach to Kripke-style logical relations that can deal with open terms, which allows us to prove the desired properties of our calculus. We formalise our core results in Coq, and introduce an experimental surface-level programming language to show that our approach is applicable in practice.
@article{paperbot552,
title = {Binders by day, labels by night: effect instances via lexically scoped handlers},
author = {Dariusz Biernacki and Maciej Piróg and Piotr Polesiuk and Filip Sieczkowski},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371116}
}