一句话:提出将二等能力推断为区域/证据的提升推断翻译,使词法效应处理器高效编译且保持类型与语义。
效应处理器提供了结构化的效应抽象,但常带来显著运行时开销。已有工作用 CPS 翻译并结合处理器嵌套信息来决定效应穿过哪些处理器,但显式区域与子区域证据的演算过于冗长,不适合作为源语言。本文为源语言底层的演算推断这种提升信息:该演算使用二等能力安全使用效应;作者定义到带区域与证据演算的类型化翻译,并证明该提升推断翻译保持可类型性与语义,从而揭示二等能力与区域结构的关系,并补齐编译器流水线中的缺口。实现与基准测试表明该方法可行。
Effect handlers are a high-level abstraction that enables programmers to use effects in a structured way. They have gained a lot of popularity within academia and subsequently also in industry. However, the abstraction often comes with a significant runtime cost and there has been intensive research recently on how to reduce this price. A promising approach in this regard is to implement effect handlers using a CPS translation and to provide sufficient information about the nesting of handlers. With this information the CPS translation can decide how effects have to be lifted through handlers, i.e., which handlers need to be skipped, in order to handle the effect at the correct place. A structured way to make this information available is to use a calculus with a region system and explicit subregion evidence. Such calculi, however, are quite verbose, which makes them impractical to use as a source-level language. We present a method to infer the lifting information for a calculus underlying a source-level language. This calculus uses second-class capabilities for the safe use of effects. To do so, we define a typed translation to a calculus with regions and evidence and we show that this lift-inference translation is typability- and semantics-preserving. On the one hand, this exposes the precise relation between the second-class property and the structure given by regions. On the other hand, it closes a gap in a compiler pipeline enabling efficient compilation of the source-level language. We have implemented lift inference in this compiler pipeline and conducted benchmarks which indicate that the approach is indeed working.
@article{paperbot1841,
title = {From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers},
author = {Marius Müller and Philipp Schuster and Jonathan Lindegaard Starup and Klaus Ostermann and Jonathan Immanuel Brachthäuser},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622831}
}