一句话：提出用顺序维护数据结构实现增量双向类型检查，细粒度编辑后快速传播类型更新，性能较从头重分析快多个数量级。
实时编程环境需要随用户编辑持续提供类型检查等语义服务，但大程序的反复全量分析开销巨大。本文提出一种可高效增量更新类型信息的系统，更新内容包括类型错误标记以及每个表达式的期望类型与实际类型。系统在类型论层面被刻画为一个小步动态语义，在带标记和注解的程序上传播更新：大部分更新遵循基础双向类型系统，同时维护从绑定变量到其绑定位置的指针，类型更新可直接沿这些指针遍历；系统采用顺序维护数据结构来高效维护指针并确定更新传播的优先级。作者在 Agda 中机器化证明了该系统与朴素重分析等价，并证明其他重要元理论性质。随后给出经过多项优化的 OCaml 实现，并通过大规模压力测试评估，相比从头重分析取得多个数量级加速。
Live programming environments provide various semantic services, including type checking and evaluation, continuously as the user is editing the program. The live paradigm promises to improve the developer experience, but liveness is an implementation challenge, particularly when working with large programs. This paper specifies and efficiently implements a system that is able to incrementally update type information for a live program in response to fine-grained program edits. This information includes type error marks and information about the expected and actual type of every expression. The system is specified type-theoretically as a small-step dynamics that propagates updates through the marked and annotated program. Most updates flow according to a base bidirectional type system. Additional pointers are maintained to connect bound variables to their binding locations, with type updates traversing these pointers directly. Order maintenance data structures are employed to efficiently maintain these pointers and to prioritize the order of update propagation. We prove this system is equivalent to naive reanalysis in the Agda theorem prover, along with other important metatheoretic properties. We then provide an efficient OCaml implementation, detailing a number of impactful optimizations. We evaluate this implementation’s performance with a large stress-test and find that it is able to achieve multiple orders of magnitude speed-up compared to from-scratch reanalysis.
@article{paperbot2966,
title = {Incremental Bidirectional Typing via Order Maintenance},
author = {Thomas J. Porter and Marisa Kirisame and Ivan Wei and Pavel Panchekha and Cyrus Omar},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763117}
}