Patch Theory for Entities

Version control has been trying to acquire a theory for twenty years, and it keeps almost working. The attempts are real mathematics done by serious people, and each one runs into the same wall. This post is about that wall, why changing one thing about the data model walks straight through it, and what we can and cannot prove once you do.

The short version is that merge becomes provable when you stop treating a file as a sequence and start treating it as a map.

Why the theory kept failing

Darcs shipped in 2005 with an explicit "theory of patches", where patches were invertible operations and the important relation was commutation. It was the first serious attempt to say what a merge is rather than what an algorithm happens to do. It was also never proven sound, and it famously fell into merges that took exponential time.

Judah Jacobson later gave Darcs a real algebraic footing using inverse semigroups, and Samuel Mimram and Cinzia Di Giusto gave the whole idea a category-theoretic treatment where a merge is a pushout. Pijul is built directly on that second one, which is why it can claim a merge that Darcs could not. There is even a machine-checked version, the homotopical patch theory of Angiuli, Morehouse, Licata and Harper, which models a repository as a higher inductive type so that the group laws fall out of the type theory itself.

So the theory exists and it is good. The problem is what it has to be a theory of.

A patch to a sequence of lines is defined by position. Insert a line at index 12, and every subsequent patch that mentions index 12 now means something different. Two edits that a human would call obviously independent do not commute, because both are stated in coordinates the other one moved. Every line-based patch theory spends most of its machinery reconstructing intent that the representation destroyed, and conflicts appear wherever that reconstruction is ambiguous rather than wherever the changes actually disagree.

One change to the model

Let N be a set of stable entity names, meaning functions, classes and methods addressed by identity rather than by position. Let C be the set of possible contents for one of them. A repository state is a finite partial map.

s : N ⇀ C

A patch is a finite set of primitive operations, each targeting exactly one name.

add(n, c)        applicable when n ∉ dom(s)
del(n)           applicable when n ∈ dom(s)
mod(n, c → c')   applicable when s(n) = c

Each primitive is a partial invertible map on states, so patches form a groupoid, which is the same structure Jacobson found in Darcs. Nothing here is new mathematics. What is new is that the operations are keyed by name instead of position, and that single change does the work.

Two patches touching different names commute. Not usually, not after a normalization pass, but by definition, because a finite map has no ordering for them to disturb. The property that line-based patch theory spends all its effort trying to recover is now free.

Merge is a pushout, and conflicts become decidable

Given a base state b and two patches out of it, p₁ and p₂, the merge is the pushout of that span. In plain terms, the pushout is the smallest state that contains both changes and does not commit to anything neither side asked for.

Two things follow immediately.

The proof is one line, since disjoint keys commute and the union is therefore well defined. This is the common case in real repositories, and unlike "the changed line ranges do not overlap", disjointness of names is stable under formatting, reordering and unrelated edits elsewhere in the file.

That is the complete condition, it is decidable, and it is checkable in time linear in the size of the patches. There is no heuristic and no tunable threshold. Either two changes touch the same entity differently or they do not.

To make merge total rather than partial, extend contents with an explicit conflict value.

C^ = C ∪ { conflict(base, ours, theirs) }

Now the merge always exists and is computed key by key. If at most one side changed a name, take that side. If both changed it identically, take it. If both changed it differently, emit a conflict value at that key. This is Mimram's free cocompletion trick, and in an implementation it is exactly a per-entity conflict marker, except that it is derived from the model rather than asserted by the merge algorithm.

The laws come for free

Because the merge is computed independently at each key, the whole-state merge is a pointwise product of per-key merges, and each per-key merge is a bounded join relative to the base. Products of semilattices are semilattices, so the algebra you want falls out without separate proofs.

Writing ⋄ᵦ for merge against base b, you get idempotence, so s ⋄ᵦ s = s. You get commutativity, so s₁ ⋄ᵦ s₂ = s₂ ⋄ᵦ s₁ once conflict values are treated as unordered. You get a unit, so a side that changed nothing contributes nothing. And you get associativity on pairwise disjoint supports, which becomes full associativity once conflict values flatten.

These are the properties people usually assert about a merge tool in a README. Here they are consequences of the representation.

Many agents converge, and that is a different proof

There is a second thing the same structure buys, and it is worth separating because it is proven by a different community.

A finite map with a per-key join is a map-CRDT. That means Shapiro's strong eventual consistency result applies directly, so replicas that observe the same set of operations converge to the same state regardless of order or timing. Better still, there is already a machine-checked proof of exactly this shape, in Isabelle/HOL, by Gomes, Kleppmann, Mulligan and Beresford. You instantiate it rather than redo it.

So the two halves of a multi-agent merge story get two independent and established proofs. The pushout view says a single three-way merge is correct and says exactly when it conflicts. The semilattice view says that any number of agents editing concurrently will agree in the end. The entity model is the representation where both apply cleanly at once, and it is not obvious that anything else does.

The honest boundary

Everything above is about which entity wins and when a conflict exists. None of it proves that merging two edits inside the same function body is correct.

That residual is ordinary text merge, and it is not provable in general, because two people rewriting the same three lines can disagree in ways no algorithm can adjudicate. So the correct theorem is a reduction rather than a total result.

The whole-repository correctness theorem is parametric in that inner merge. This is a weaker claim than "we proved merge", and it is the one that is actually true. It is also more useful than it sounds, because it confines everything unprovable to a single function body instead of letting it range over a whole file. That confinement is the entire practical benefit, and it is why an entity-level tool produces fewer conflicts without being more reckless.

What we measured

Theory that never meets a benchmark is a hobby, so here is what happens when this model is implemented. weave is the merge driver, and everything below reproduces from its repository.

On 31 hand-written scenarios across seven languages, run with weave bench.

Two of those 31 scenarios must not merge, and that deserves explanation because it is the most interesting number in the table. When both sides add different decorators to the same Python or TypeScript function, decorator application is function composition, so the stacking order changes behaviour. Putting @cache outside @auth serves cached responses without ever running the authentication check. There is no correct order to pick, so weave refuses. A tool that merges those cleanly is wrong rather than better, and we changed our own benchmark to stop rewarding it, which cost us a headline 31/31 clean-merge number we had been quoting.

Annotations in Java, C# and Kotlin are unordered metadata, so those still merge by set union. The distinction is semantic, not syntactic.

Replayed across 300 real merge commits from flask, which yielded 37 files where a supported three-way merge actually happened, weave produced zero regressions against the human-authored merge and resolved two conflicts git could not. That is a small sample of contested files, and we would rather report it as such than round it into a percentage.

What went wrong

The reading side of this is a separate tool, sem, which answers structural questions from the same entity graph. Measured per operation on flask, asking sem for a function plus its callers and callees costs 96 to 98 percent fewer tokens than grepping and reading the files, and impact queries are near total reductions because a graph traversal returns callers where grep returns every textual mention.

Those numbers are real and they are also not the whole story, so here is the part that did not work.

First, sem's name resolution missed. Of fifteen entities we sampled from flask, sem context resolved nine and returned nothing for six, despite sem entities listing all fifteen. A 40 percent miss rate is disqualifying for a tool meant to replace grep, since grep does not silently fail to find things, and we excluded those six from the token comparison rather than let a failure masquerade as a zero-token win.

Second, and more uncomfortable, the per-operation savings did not survive contact with an agent loop. We ran a three-armed comparison on SWE-bench Lite instances, giving the same agent traditional file tools, then sem's structural tools, then sem plus entity-level editing. On one run the structural arm consumed roughly three times more tokens than the file-based arm, because verbose structural output accumulates in context and resolution misses make the agent retry until it hits the turn limit. On a later run with a stronger model, the file-based arm solved both tasks while the entity-editing arm solved neither.

Two instances is far too small to conclude anything, and we are not claiming the approach fails. We are saying that a large per-operation reduction is not the same as a session-level win, that we have measured one and not yet demonstrated the other, and that anyone who tells you otherwise about their own tooling has probably not run the second experiment.

What is open

The theory has a clear next step, which is to formalize the model and the two theorems in Lean or Isabelle so the core is machine-checked rather than argued in prose. The pieces are small, the CRDT half can be instantiated from existing work, and the inner merge stays abstract with stated obligations. That would make this the first entity-level merge with a mechanized soundness result, as far as we know.

The engineering has a clearer one. Fix the resolution misses, then re-run the agent comparison at a sample size that can actually support a claim.

The part we are most confident about is the smallest. Choosing names over positions as the unit of change turns merge from a heuristic into a structure where a conflict has a definition, and both a categorical proof and a CRDT convergence proof apply to the same object at once. Everything after that is implementation, and implementation is allowed to be wrong in ways the model is not.