My understanding of Pijul’s patch theory is that it is based on Mimram and Giusto’s paper “A Categorical Theory of Patches” where they model a merge as a pushout and describe a syntactic construction of the free (conservative) finite cocompletion of a category. The idea that a merge should be a pushout seems well-motivated to me, but their specific model of the category of patches seems wrong.
Their model of “increasing” patches seems fine, but their model of patches with deletion forms a (connected) groupoid: every object is equivalent because you can just delete all the lines of the file and then add the lines in the other version. This would mean that any file state could be a valid merge, including always producing the empty file. I have searched for mention of this problem and only found this comment on reddit which is probably where I first heard about this problem.
How is this problem addressed in pijul? It seems to me that the objects of the category should incorporate some amount of the “history” of the object that does monotonically increase, in order to make deleting and restoring not an isomorphism, but I haven’t worked out any details. This blog post describes “ghost lines” but not very formally. Is there something more formal in the pijul repo?
I don’t think anything formal has been written (either within the pijul repo or not), but the extension isn’t too complicated. You just extend the model in the paper by adding a boolean “deleted” flag to each edge. (That is, an object in the category of files is an equivalence class of directed graphs, in which each node of the graph has some text and a boolean flag.) Then you allow patches to delete lines (meaning, set the flag to true) but not undelete them. The result isn’t a groupoid because a patch which deletes a line has no inverse.
In the paper, two directed graphs are equivalent if they have the same path-connectedness relation. I think pijul actually uses directed graphs themselves as the objects (rather than equivalence classes) because computing the equivalence relationship is a bit slow.
I’d guess that it arises as the co-completion of the smaller category containing only totally ordered files (and including the deleted flags), but admittedly I haven’t checked.
The current underlying category exits, is cocomplete, and merges are indeed pushouts. However, it is not constructed as a free cocompletion, although I don’t see any obvious obstruction to finding a basic category C including deletions where patches have pushouts if and only if their merge is a line graph.