Reference. Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
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.
Cite
Cites 44 works (5 here)
With notes (5)
Total Type Error Localization and Recovery with Holes zhao-2024-total
Type systems typically only define the conditions under which an expression is well-typed, leaving ill-typed expressions formally meaningless. This approach is insufficient as the basis for language servers driving modern programming environments, which are expected to recover from simultaneously localized errors and continue to provide a variety of downstream semantic services. This paper addresses this problem, contributing the first comprehensive formal account of total type error localization and recovery: the marked lambda calculus. In particular, we define a gradual type system for expressions with marked errors, which operate as non-empty holes, together with a total procedure for marking arbitrary unmarked expressions. We mechanize the metatheory of the marked lambda calculus in Agda and implement it, scaled up, as the new basis for Hazel, a full-scale live functional programming environment with, uniquely, no meaningless editor states. The marked lambda calculus is bidirectionally typed, so localization decisions are systematically predictable based on a local flow of typing information. Constraint-based type inference can bring more distant information to bear in discovering inconsistencies but this notoriously complicates error localization. We approach this problem by deploying constraint solving as a type-hole-filling layer atop this gradual bidirectionally typed core. Errors arising from inconsistent unification constraints are localized exclusively to type and expression holes, i.e., the system identifies unfillable holes using a system of traced provenances, rather than localized in an ad hoc manner to particular expressions. The user can then interactively shift these errors to particular downstream expressions by selecting from suggested partially consistent type hole fillings, which returns control back to the bidirectional system. We implement this type hole inference system in Hazel.
Peritext: A CRDT for Collaborative Rich Text Editing litt-2022-peritext
Conflict-Free Replicated Data Types (CRDTs) support decentralized collaborative editing of shared data, enabling peer-to-peer sharing and flexible branching and merging workflows. While there is extensive work on CRDTs for plain text, much less is known about CRDTs for rich text with formatting. No algorithms have been published, and existing open-source implementations do not always preserve user intent. In this paper, we describe a model of intent preservation in rich text editing, developed through a series of concurrent editing scenarios. We then describe Peritext, a CRDT algorithm for rich text that satisfies the criteria of our model. The key idea is to store formatting spans alongside the plaintext character sequence, linked to a stable identifier for the first and last character of each span, and then to derive the final formatted text from these spans in a deterministic way that ensures concurrent operations commute. We have prototyped our algorithm in TypeScript, validated it using randomized property-based testing, and integrated it with an editor UI. We also prove that our algorithm ensures convergence, and demonstrate its causality preservation and intention preservation properties.
Bidirectional Typing dunfield-2021-bidirectional
Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to support features for which inference is undecidable; using synthesis enables bidirectional typing to avoid the large annotation burden of explicitly typed languages. In addition, bidirectional typing improves error locality. We highlight the design principles that underlie bidirectional type systems, survey the development of bidirectional typing from the prehistoric period before Pierce and Turner’s local type inference to the present day, and provide guidance for future investigations.
Hazelnut: a bidirectionally typed structure editor calculus omar-2017-hazelnut
Homotopical patch theory angiuli-2016-homotopical
Homotopy type theory is an extension of Martin-Löf type theory, based on a correspondence with homotopy theory and higher category theory. In homotopy type theory, the propositional equality type is proof-relevant, and corresponds to paths in a space. This allows for a new class of datatypes, called higher inductive types, which are specified by constructors not only for points but also for paths. In this paper, we consider a programming application of higher inductive types. Version control systems such as Darcs are based on the notion of patches—syntactic representations of edits to a repository. We show how patch theory can be developed in homotopy type theory. Our formulation separates formal theories of patches from their interpretation as edits to repositories. A patch theory is presented as a higher inductive type. Models of a patch theory are given by maps out of that type, which, being functors, automatically preserve the structure of patches. Several standard tools of homotopy theory come into play, demonstrating the use of these methods in a practical programming context.
External (39)
- Artifact for Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus (2024)
- Version control post-Git (FOSDEM 2024 talk) (2024)
- How CRDTs make multiplayer text editing part of Zed's DNA (2022)
- A Highly-Available Move Operation for Replicated Trees (2021)
- Moving elements in list CRDTs (2020)
- Conflict-free replicated data types (CRDTs) (2018)
- Enhancing rich content wikis with real‐time collaboration (2017)
- Toward Semantic Foundations for Program Editors (2017)
- Near Real-Time Peer-to-Peer Shared Editing on Extensible Data Types (2016)
- A graph-based algorithm for three-way merging of ordered collections in EMF models (2015)
- Refined Criteria for Gradual Typing (2015)
- Fine-grained and accurate source code differencing (2014)
- LSEQ: an adaptive structure for sequences in distributed collaborative editing (2013)
- From bytecode to JavaScript: the Js_of_ocaml compiler (2013)
- Evaluating CRDTs for real-time document editing (2011)
- Conflict-Free Replicated Data Types (2011)
- Language and IDE Modularization and Composition with MPS (2011)
- Approximating Tree Edit Distance through String Edit Distance for Binary Tree Codes (2010)
- Deep hypertext with embedded revision control implemented in regular expressions (2010)
- The Scratch Programming Language and Environment (2010)
- Operation-Based, Fine-Grained Version Control Model for Tree-Based Representation (2010)
- Replicated abstract data types: Building blocks for collaborative applications (2010)
- An optimal decomposition algorithm for tree edit distance (2009)
- A Commutative Replicated Data Type for Cooperative Editing (2009)
- The Sketching Approach to Program Synthesis (2009)
- Logoot: A Scalable Optimistic Replication Algorithm for Collaborative Editing on P2P Networks (2009)
- Darcs 2.1.0.1 Appendix A: Theory of patches (2009)
- Change Distilling:Tree Differencing for Fine-Grained Source Code Change Extraction (2007)
- Data consistency for P2P collaborative editing (2006)
- A survey on tree edit distance and related problems (2005)
- Darcs: distributed version management in Haskell (2005)
- A three-way merge for XML documents (2004)
- Toward unique identifiers (1999)
- Computing the Edit-Distance Between Unrooted Ordered Trees (1998)
- Meaningful change detection in structured data (1997)
- The Zipper (1997)
- Concurrency control in groupware systems (1989)
- The Cornell program synthesizer (1981)
- An Algorithm for Differential File Comparison (1976)