一句话：提出 Grove 协作结构编辑器演算，消除 patch 合成与三方合并，使编辑可交换并显式表示冲突，同时提供双向类型化支持。
传统版本控制依赖 patch 语言、diff 与三方合并，面对一行多编辑或代码迁移常误判冲突。Grove 是一种协作结构编辑器演算：patch 直接从编辑动作日志导出，所有编辑可交换，仓库状态构成交换复制数据类型（CmRDT）。其核心是带唯一标识顶点和边的有标有向多重图，编辑仅为边的插入与永久删除；通过 grove 分解，将局部、迁移和单环迁移冲突用洞与树间引用显式表示。Grove 还为 grove 设计类型错误定位系统并证明全性，使所有编辑状态静态有意义；静态语义是双向标记系统，结合渐进类型与合一推断来填充类型洞。作者用 Agda 机化元理论，并实现可由语法树规格生成 OCaml 代码的 Grove Workbench。
Version control systems typically rely on a patch language , heuristic patch synthesis algorithms like diff , and three-way merge algorithms . Standard patch languages and merge algorithms often fail to identify conflicts correctly when there are multiple edits to one line of code or code is relocated. This paper introduces Grove, a collaborative structure editor calculus that eliminates patch synthesis and three-way merge algorithms entirely. Instead, patches are derived directly from the log of the developer’s edit actions and all edits commute, i.e. the repository state forms a commutative replicated data type (CmRDT). To handle conflicts that can arise due to code relocation, the core datatype in Grove is a labeled directed multi-graph with uniquely identified vertices and edges. All edits amount to edge insertion and deletion, with deletion being permanent. To support tree-based editing, we define a decomposition from graphs into groves , which are a set of syntax trees with conflicts–including local, relocation, and unicyclic relocation conflicts–represented explicitly using holes and references between trees. Finally, we define a type error localization system for groves that enjoys a totality property, i.e. all editor states in Grove are statically meaningful, so developers can use standard editor services while working to resolve these explicitly represented conflicts. The static semantics is defined as a bidirectional marking system in line with recent work, with gradual typing employed to handle situations where errors and conflicts prevent type determination. We then layer on a unification-based type inference system to opportunistically fill type holes and fail gracefully when no solution exists. We mechanize the metatheory of Grove using the Agda theorem prover. We implement these ideas as the Grove Workbench , which generates the necessary data structures and algorithms in OCaml given a syntax tree specification.
@article{AdamsGPSZO25,
title = {Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus},
author = {Michael D. Adams and Eric Griffis and Thomas J. Porter and Sundara Vishnu Satish and Eric Zhao and Cyrus Omar},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704909}
}