Patch theory in Darcs and Pijul, and the categorical theory of patches

Document status: reviewed. Canonical source.

Summary

Darcs treats a repository as a set of patches and defines merge through commutation: two sequential patches A B may be rewritten as B' A' with the same effect, and a patch has an inverse. Conflicts in Darcs 2 are encoded by a special patch type, the conflictor, which stores the conflicting primitive and the closure of what it conflicts with; the Darcs wiki reports that commutation with conflictors is not always invertible and that duplicates are a major source of defects. Mimram and Di Giusto formalise files as objects and patches as morphisms of a category L, define merge as a pushout, observe that conflicting patches have no pushout, and construct the free finite conservative cocompletion P whose objects are finite sets of labelled lines with a transitive relation, so conflicts become ordinary objects and merging always exists. Pijul implements the same idea operationally: a repository is a directed graph of line vertices identified by the hash of the introducing change and an offset, edits are edge relabellings, independent changes commute, and conflicts (unordered alive vertices, cycles, zombie vertices) are stable graph states that later changes resolve. What generalises to semantic operations on identity-bearing trees is stated in the relevance section.

Evidence

Category of files and patches: a file is A : [n] → L; a patch is an injective increasing partial function f : [m] → [n] with B ∘ f = A where defined (Definition 1). L is the free monoidal category generated by insertion η_a : I → a and deletion ε_a : a → I with ε_a ∘ η_a = id_I (Proposition 2). Mimram and Di Giusto, arXiv 1311.3903 PDF, §2 (retrieved 2026-08-29).
Merge as pushout: the merged file of two coinitial patches “should be a pushout of the diagram (2)”; diagram (3) “does not admit a pushout in L. In this case, the two patches f1 and f2 are said to be conflicting.” §3.
Completion: P is the free finite conservative cocompletion of L (Definition 5); by Theorem 6 it is the subcategory of presheaves preserving finite limits; concretely P is equivalent to finite sets with a transitive relation and relation-preserving functions (Theorem 15); the pushout in P is B ⊎ C / ~ with the transitive closure of the inherited relations (Proposition 16); cycles arise in P (Example 18); a morphism G1 + G1 → G1 merges two independent lines, modelling conflict resolution (Example 19); deletions are handled in §6 (Theorem 20). §3-6.
Related-work statement: “The Darcs community has investigated a formalization of patches based on commutation properties [10]” and the residual-as-pushout condition is never stated in Darcs or OT work. §1.
Darcs theory index: three phases, Darcs 1 “Mergers”, Darcs 2 “Conflictors” described as the current state of the art, Darcs 3 formalisation work; links to Jacobson’s inverse-semigroup formalisation (UCLA CAM report 09-83), Camp, Angiuli et al. ICFP 2014, Mimram and Di Giusto, Pijul. http://darcs.net/Theory (retrieved 2026-08-29). The Darcs manual chapter on patch theory returned HTTP 500 on retrieval; commutation notation below is taken from the wiki pages and the Mimram related-work section, not from the manual.
Conflictors: “a special patch type that represents a conflict between primitive patches (used for Darcs2 repositories)”; a conflictor stores the original primitive, the transitive closure of the changes it conflicts with, and the tracking “apparently has bugs”; commuting a conflictor with a duplicate “is not guaranteed to be invertible”. http://darcs.net/Theory/Conflictors (retrieved 2026-08-29).
Pijul commutation and conflicts: “for any two changes A and B, either A and B can be applied in any order, or A depends on B, or B depends on A”; “Conflicting changes always commute in Pijul and never commute in Darcs”; Darcs suffers “the exponential merge problem”; conflicting edits are applied without resolution so no information is lost. https://pijul.org/manual/why_pijul.html (retrieved 2026-08-29).
Pijul model: a repository is a directed graph G = (V, E) whose vertices are lines identified by the hash of the introducing change and a position within it; edges carry a status label (alive, deleted) and the introducing change; deletion relabels an edge from alive to dead, so the structure is append-only; an insertion depends on the changes that introduced its context, a deletion on the change that created the edge; three conflict kinds: two alive vertices with no directed path between them, alive vertices with paths in both directions (cycle), and zombie vertices with both alive and dead incoming edges; pseudo-edges connect across deleted regions so alive-subgraph traversal does not become linear in history; files use a name vertex and an inode vertex so renames commute with content edits. https://pijul.org/manual/theory.html (retrieved 2026-08-29).
Pijul conflict handling: insertion conflicts (same position, order undecidable), deletion conflicts (edit inside a deleted block), name and rename conflicts; conflicts persist as repository state, further changes apply on top, resolution is itself a change; pijul unrecord removes a change. https://pijul.org/manual/conflicts.html (retrieved 2026-08-29).

Mechanism

Darcs (commutation calculus, notation as used in the Darcs theory pages and the Mimram related-work summary):

sequential composition   A ; B         (B is written in the context after A)
commutation              A ; B  <->  B' ; A'      when the pair commutes
inverse                  A ; A⁻¹ = id
merge of parallel A, B  = find B' with  A ; B' having the effect of both
conflict                 = commutation fails for a required pair; Darcs 2 records a conflictor

Categorical form (Mimram and Di Giusto):

objects: files  A : [n] → L        morphisms: patches (injective, increasing, partial, label-preserving)
merge(f1 : A → A1, f2 : A → A2) = pushout  A1 → M ← A2      (exists only when f1, f2 compatible)
P = free finite conservative cocompletion of L
objects of P: (S, <) finite labelled set with transitive relation   (lines partially ordered; cycles allowed)
pushout in P: B ⊎ C / (f(a) ~ g(a)), relation = transitive closure of <_B ∪ <_C

Pijul (graph of lines):

vertex id   = (hash(change), offset)
edge label  = (status ∈ {alive, deleted, ...}, change)
insert(line) : add vertex, add alive edges to context vertices; depends on context-introducing changes
delete(line) : relabel incoming edge alive → deleted; depends on edge-introducing change
apply(c1); apply(c0) = apply(c0); apply(c1)  when neither depends on the other
conflict states: unordered alive siblings | cycle | zombie (alive + deleted edges)
resolution: a new change that adds ordering edges or kills vertices

Cost model as stated by the sources: Darcs merges can be exponential in the presence of conflicts (Pijul manual); Pijul’s pseudo-edges keep alive-subgraph traversal from scaling with history; Pijul’s apply depends on the change and its dependencies, not on the full history, but the manual gives no formal bound.

NUIF relevance

Borrow

Conflict as a first-class state (Pijul zombie and unordered states; objects of P) so a NUIF three-way merge can produce a document containing typed conflict objects rather than failing, matching spec/06’s requirement to surface typed conflicts.
Commutation of independent operations as the definition of independence: two NUIF operations are independent when neither’s preconditions mention the other’s effects, and the merge is their commuted composition.
Content-derived identity for inserted lines (hash of change plus offset) as the model for assigning entity IDs to elements created inside a patch before the patch has a revision hash.

Adapt

Pijul’s dependency rule (an edit depends on the changes that introduced its context) maps to NUIF preconditions: a SetProperty should depend on the create of its entity, a Move on the create of the destination parent; dependencies should be derived from preconditions rather than declared manually.
The categorical merge-as-pushout requirement is a correctness test for a NUIF merge function: for independent patches the merge must equal both compositions, otherwise the result must be a conflict object, never an arbitrary winner.
Pijul’s dual vertices (name vs. content) correspond to separating Rename from structural operations in nuif-protocol so renames commute with subtree edits.

Reject

Line-level graph representation for the canonical document: NUIF entities already have stable identity, so a graph of lines is unnecessary; only the conflict states and commutation discipline transfer.
Darcs-style conflictors that record transitive closures inside the patch stream; the Darcs wiki documents non-invertible commutation and duplicate-related defects.

Open questions

Whether NUIF’s operation set can be given a category with all pushouts (a completion analogous to P) or whether some operation pairs (delete versus move-into) must remain conflict objects by design.
What the complexity of merging two long NUIF patches is when conflicts are retained rather than resolved; Pijul provides no formal bound to compare against.
Whether identity-bearing entities remove the “insertion conflict” class entirely (two inserts under one parent are ordered by order keys) or merely convert it into an ordering conflict.