Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
summary
Paper claims a version-control model that removes patch synthesis and three-way merge by making edits commute: edits become no diff or merge commutative operations so remote actions can be applied in any order. The core datatype is a labeled directed multigraph where all edits are edges-only edits (insert/delete, deletions are permanent), graphs decompose into groves that explicitly represent relocation and unicyclic conflicts, a bidirectional gradual typing/localization gives total static meaning for all states, the metatheory is mechanized in Agda, and a Grove Workbench generates OCaml artifacts (evaluated functional).
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:08Why version control is a programming languages problem
- 2:58Patch-based merging problems
- 5:26Eliminating diff with structure editing
- 7:54Merging in structure editors
- 8:59Commutative Replicated Data Types for merging
- 10:21Grove patch language
- 11:47Graph-based program state
- 15:14Collaborative structure editing
- 17:01Conflict representation in Grove
- 18:46Type error localization in Grove
- 19:50Live collaborative programming
- 20:31Q&A
related talks
01h 00mA Type-Safe Structure Editor Calculus + Strictly Capturing Non-Strict Closures
14mIncremental Bidirectional Typing via Order Maintenance
29mA type safe calculus for generating syntax-directed editors
28mDocument-oriented programming based on edit history
18mRestructuring Structure Editing
45mResidential Programming without Mutable State
34mIncremental Bidirectional Typing via Order Maintenance
11mDenicek: Computational Substrate for Document-Oriented End-User Programming