AI 中文总结
本文提出响应式编程核心演算Willow，搭配时间感知类型与效果系统，可静态跟踪响应式程序的时间行为，检测导致非终止或性能下降的渲染级联与循环，其原型检查器经评估可支撑响应式程序时间正确性推理。
AI 中文摘要
React等响应式编程框架允许开发者通过声明式指定输出如何依赖变化的输入来构建交互式应用。尽管该模型便于推理应用的计算内容，但响应式程序的时间行为仍难以理解和验证。应用隐含依赖框架运行时中的时序假设，会导致过时读取、瞬时不一致、依赖顺序的行为、意外反馈循环等微妙错误。为应对这些挑战，本文提出受React启发的响应式编程核心演算Willow。Willow提供以渲染（组件生成用户界面描述的基本评估步骤）为单位建模计算的时间感知操作语义，并搭配新型类型与效果系统，将时间行为作为效果进行静态跟踪。“next”模态表示延迟，不仅以渲染为单位，还可使用宿主环境暴露的任何单位（如渲染、网络请求或毫秒）。一系列模态跟踪事件处理程序的生命周期：注册时、触发时、待处理事件取消时及处理程序移除时。核心见解是所得效果构成时间依赖图，使标准图算法能静态检测导致非终止或性能下降的渲染级联和渲染间循环。我们对Willow进行形式化，并证明其效果系统关于时间感知语义的保真性。我们还实现带自动效果推理的原型检查器，对去抖动、表单输入、API驱动更新等代表性响应式模式进行评估。结果表明，时间感知类型为推理响应式程序的时间正确性提供了实用基础。
英文摘要
Reactive programming frameworks such as React allow developers to build interactive applications by declaratively specifying how outputs depend on changing inputs. Although this model makes it easy to reason about what an application computes, the temporal behavior of reactive programs remains difficult to understand and verify. Applications implicitly rely on timing assumptions buried in framework runtimes, leading to subtle bugs such as stale reads, transient inconsistencies, order-dependent behavior, and unintended feedback cycles. To address these challenges, this paper presents Willow, a core calculus for reactive programming inspired by React. Willow gives a time-aware operational semantics that models computation in terms of renders, the fundamental evaluation step in which components produce user interface descriptions, and pairs it with a novel type-and-effect system that statically tracks timing behavior as effects. A "next" modality expresses delays measured not only in renders but in any unit the host environment exposes--renders, network requests, or milliseconds. A family of modalities tracks the lifecycle of event handlers: when they are registered, when they fire, when pending events are canceled and when handlers are removed. A key insight is that the resulting effects form a temporal dependency graph, letting standard graph algorithms statically detect render cascades and inter-render loops that cause non-termination or performance degradation. We formalize Willow and prove preservation of the effect system with respect to the time-aware semantics. We also implement a prototype checker with automatic effect inference and evaluate it on representative reactive patterns such as debouncing, form inputs, and API-driven updates. Our results demonstrate that time-aware typing provides a practical foundation for reasoning about the temporal correctness of reactive programs.
Comments56 pages, including appendix
