通过顺序维护实现增量双向输入

《Proceedings of the ACM on Programming Languages》：Incremental Bidirectional Typing via Order Maintenance

实时编程环境中的类型信息增量更新系统设计及优化

　　

摘要

实时编程环境在用户编辑程序的过程中，持续提供各种语义服务，包括类型检查和计算。实时编程范式有望提升开发者的体验，但实现实时性是一个挑战，尤其是在处理大型程序时。本文设计并实现了一个系统，该系统能够根据细粒度的程序修改逐步更新程序的类型信息。这些信息包括类型错误标记以及每个表达式的预期类型和实际类型。从类型理论的角度来看，该系统被描述为一个“小步动态系统”，它通过被标记和注释的程序传播类型更新。大多数更新遵循一个基本的双向类型系统进行。系统还维护了一些指针，用于将绑定变量与其绑定位置关联起来，类型更新直接通过这些指针进行传播。为了高效管理这些指针并确定更新传播的顺序，采用了顺序维护数据结构。我们证明了该系统在Agda定理证明器中等同于朴素的重分析方法，并展示了其他重要的元理论特性。随后，我们提供了一个高效的OCaml实现版本，并详细介绍了多项优化措施。通过对该实现进行大规模压力测试，我们发现其性能相比从头开始进行重分析提升了多个数量级。