一句话：提出将效应处理器名称作为一等值，并借助 scoped effects 与 rank-2 多态防止名称逃逸的命名处理器设计。
代数效应与处理器能让函数式语言组合地表达计算效应，但难以区分同一效应的多个实例。已有的命名效应处理器虽可区分实例，却依赖非标准机制防止处理器名逃逸，形式化复杂且限制较强。本文提出一种简单灵活的命名处理器设计：将处理器名作为一等值，并与通过 rank-2 多态维护作用域的 scoped effects 结合，从而在普通 λ 演算中防止名称逃逸。作者形式化了命名处理器与 scoped effects 的两种组合，并在 Koka 语言中实现，还给出神经网络与合一算法等应用。
Algebraic effects and handlers are a promising technique for incorporating composable computational effects into functional programming languages. Effect handlers enable concisely programming with different effects, but they do not offer a convenient way to program with different instances of the same effect. As a solution to this inconvenience, previous studies have introduced _named effect handlers_, which allow the programmer to distinguish among different effect instances. However, existing formalizations of named handlers are both involved and restrictive, as they employ non-standard mechanisms to prevent the escaping of handler names. In this paper, we propose a simple and flexible design of named handlers. Specifically, we treat handler names as first-class values, and prevent their escaping while staying within the ordinary λ-calculus. Such a design is enabled by combining named handlers with _scoped effects_, a novel variation of effects that maintain a scope via rank-2 polymorphism. We formalize two combinations of named handlers and scoped effects, and implement them in the Koka programming language. We also present practical applications of named handlers, including a neural network and a unification algorithm.
@article{paperbot1460,
title = {First-class names for effect handlers},
author = {Ningning Xie and Youyou Cong and Kazuki Ikemori and Daan Leijen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563289}
}