一句话：提出词法作用域效应处理器的编译策略，将高层效应处理翻译为底层栈切换，并在 Lexa 中实现与验证。
词法作用域效应处理器为代数效应提供模块化语义，支持局部推理，同时保留效应处理器强大的控制流表达能力。然而现有实现可能付出类似动态作用域处理器运行时搜索的代价。本文提出一种面向词法作用域效应处理器的编译策略，遵循词法作用域原则，并以可低层控制栈布局的语言为目标；方法的关键部分被形式化并证明正确。作者在名为 Lexa 的语言中实现这些思想，其编译器将高层效应处理翻译为底层栈切换。基于一组基准的评估表明，Lexa 生成的代码高效，在某些情况下将运行时间复杂度从二次降为线性。
Lexically scoping effect handlers is a language-design idea that equips algebraic effects with a modular semantics: it enables local-reasoning principles without giving up on the control-flow expressiveness that makes effect handlers powerful. However, we observe that existing implementations risk incurring costs akin to the run-time search for dynamically scoped handlers. This paper presents a compilation strategy for lexical effect handlers, adhering to the lexical scoping principle and targeting a language with low-level control over stack layout. Key aspects of this approach are formalized and proven correct. We embody the ideas in a language called L exa : the L exa compiler translates high-level effect handling to low-level stack switching. We evaluate the L exa compiler on a set of benchmarks; the results suggest that it generates efficient code, reducing running-time complexity from quadratic to linear in some cases.
@article{MaGLZ24,
title = {Lexical Effect Handlers, Directly},
author = {Cong Ma and Zhaoyi Ge and Edward Lee and Yizhou Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689770}
}