发表机构
University of Tsukuba(筑波大学)
机构由 AI 辅助整理,请以论文原文为准。AI 中文总结
本研究严格比较一次性控制运算符与协程的表达能力,证明效应处理器和定界续延可被非对称协程宏表达,反之则不行,并修正了先前非正式论证的缺陷。
AI 中文摘要
控制运算符,如异常和效应处理器,提供了一种在程序中抽象且模块化地表示计算效应的手段。虽然大多数理论研究集中在多次性控制运算符上,但一次性控制运算符——它将捕获的续延的使用限制在至多一次——因其在表达能力和效率之间的平衡而受到关注。本研究旨在填补这一空白。我们对一次性控制运算符(包括效应处理器、定界续延,甚至非对称协程)之间的表达能力进行了数学上严格的比较。遵循先前关于多次性控制运算符的研究,我们采用Felleisen的宏表达能力作为我们的表达能力度量。我们验证了一个民间传说:一次性效应处理器和一次性定界控制运算符可以被非对称协程宏表达,但反之则不然。我们解释了为什么先前的一个非正式论证失败,以及如何修改它以得到一个有效的宏翻译。这是发表于APLAS 2025的一篇论文的扩展版本。
英文摘要
Control operators, such as exceptions and effect handlers, provide a means of representing computational effects in programs abstractly and modularly. While most theoretical studies have focused on multi-shot control operators, one-shot control operators---which restrict the use of captured continuations to at most once---are gaining attention for their balance between expressiveness and efficiency. This study aims to fill the gap. We present a mathematically rigorous comparison of the expressive power among one-shot control operators, including effect handlers, delimited continuations, and even asymmetric coroutines. Following previous studies on multi-shot control operators, we adopt Felleisen's macro-expressiveness as our measure of expressiveness. We verify the folklore that one-shot effect handlers and one-shot delimited-control operators can be macro-expressed by asymmetric coroutines, but not vice versa. We explain why a previous informal argument fails, and how to revise it to make a valid macro-translation.
Comments82 pages, 17 figures. Extended version of a paper presented at APLAS 2025 (LNCS 16201, pp. 88-106, https://doi.org/10.1007/978-981-95-3585-9_5, full version: arXiv:2509.11901)