一句话：提出广义证据传递等精化技术，把代数效应处理器高效编译到 C，性能超越多个最佳实现。
本文研究代数效应处理器的编译技术。作者提出一系列逐步精化的中间形式：从代数效应出发，经过多提示定界控制、广义证据传递（generalized evidence passing）、yield bubbling，最终以单子翻译归约为纯 lambda 演算，从而可高效编译到多种目标平台。文中还探讨了该设计空间中的若干有趣设计点。作者给出两种实现：一个 Haskell 库，以及 Koka 语言的 C 后端。评估上将所提技术与另外三种同类最佳实现进行比较，包括多核 OCaml、Haskell 的 Ev.Eff 库与 C 的 libhandler 库，结果表明该技术十分有效。作者期望这项工作能为未来代数效应的设计与实现奠定基础。
This paper studies compilation techniques for algebraic effect handlers. In particular, we present a sequence of refinements of algebraic effects, going via multi-prompt delimited control, _generalized evidence passing_, yield bubbling, and finally a monadic translation into plain lambda calculus which can be compiled efficiently to many target platforms. Along the way we explore various interesting points in the design space. We provide two implementations of our techniques, one as a library in Haskell, and one as a C backend for the Koka programming language. We show that our techniques are effective, by comparing against three other best-in-class implementations of effect handlers: multi-core OCaml, the _Ev.Eff_ Haskell library, and the libhandler C library. We hope this work can serve as a basis for future designs and implementations of algebraic effects.
@article{paperbot1117,
title = {Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C},
author = {Ningning Xie and Daan Leijen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473576}
}