一句话:证明通用效应处理器使 generic count 获得渐近加速,差距源于单次与多次限定控制之别。
该论文研究限定控制(delimited control)所能带来的根本性效率收益。作者在纯函数基语言 λ_b 与加入通用效应处理器的扩展 λ_h 中考察 generic count 问题,证明 λ_h 能以渐近意义上优于 λ_b 中任何实现的方式求解该问题。作者进一步把 λ_b 扩展为带仿射效应处理器的语言 λ_a(其表达能力足以编码异常、局部状态、协程与单次续延),并证明这一效率差距依然存在。由此,效率差异被精确定位在“单次(single-shot)”与“多次(multi-shot)”限定控制之间的鸿沟上。据作者所知,这是控制算子方向上首类此类结果。
Abstract We study a fundamental efficiency benefit afforded by delimited control, showing that for certain higher-order functions, a language with advanced control features offers an asymptotic improvement in runtime over a language without them. Specifically, we consider the generic count problem in the context of a pure functional base language ${\lambda_{\textrm{b}}}$ and an extension ${\lambda_{\textrm{h}}}$ with general effect handlers . We prove that ${\lambda_{\textrm{h}}}$ admits an asymptotically more efficient implementation of generic count than any implementation in ${\lambda_{\textrm{b}}}$ . We also show that this gap remains even when ${\lambda_{\textrm{b}}}$ is extended to a language ${{{{{{\lambda_{\textrm{a}}}}}}}}$ with affine effect handlers , which is strong enough to encode exceptions, local state, coroutines and single-shot continuations. This locates the efficiency difference in the gap between ‘single-shot’ and ‘multi-shot’ versions of delimited control. To our knowledge, these results are the first of their kind for control operators.