一句话：为词法效应处理器设计并形式化了一种 dynamic wind，在任意控制效应下保持良定义语义与资源括约。
效应处理器以词法方式局部定义效应行为，并支持恢复续延，因此与 Scheme 的 dynamic-wind 所依赖的「进入/退出严格配对」假设相冲突：续延可能被延后恢复甚至恢复多次，导致资源括约失效。本文提出一种与词法效应处理器集成的 dynamic wind 变体，给出其设计、形式化语义与实现。该语义在任意位置出现任意控制效应时仍然良定义，尤其规定了在 prelude/postlude 中捕获与恢复续延的行为，并保证资源括约不被破坏。作者通过两个用例说明其表达力：外部状态的回溯（backtracking）与外部资源的终结（finalization）。
Effect handlers offer an attractive way of abstracting over effectful computation. Moreover, languages with effect handlers usually statically track effects, which ensures the user is aware of all side effects different parts of a program might have. Similarly to exception handlers, effect handlers discharge effects by locally defining their behavior. In contrast to exception handlers, they allow for resuming computation, possibly later and possibly multiple times. In this paper we present a design, formalization, and implementation for a variant of dynamic wind that integrates well with lexical effect handlers. It has well-defined semantics in the presence of arbitrary control effects in arbitrary places. Specifically, the behavior of capturing and resuming continuations in the pre- or postlude is well-defined and respects resource bracketing. We demonstrate how these features can be used to express backtracking of external state and finalization of external resources.
@article{paperbot2958,
title = {Dynamic Wind for Effect Handlers},
author = {David Voigt and Philipp Schuster and Jonathan Immanuel Brachthäuser},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763155}
}