A Categorical Theory of Patches

Samuel Mimram, Cinzia Di Giusto

When working with distant collaborators on the same documents, one often uses
a version control system, which is a program tracking the history of files and
helping importing modifications brought by others as patches. The
implementation of such a system requires to handle lots of situations depending
on the operations performed by users on files, and it is thus difficult to
ensure that all the corner cases have been correctly addressed. Here, instead
of verifying the implementation of such a system, we adopt a complementary
approach: we introduce a theoretical model, which is defined abstractly by the
universal property that it should satisfy, and work out a concrete description
of it. We begin by defining a category of files and patches, where the
operation of merging the effect of two coinitial patches is defined by pushout.
Since two patches can be incompatible, such a pushout does not necessarily
exist in the category, which raises the question of which is the correct
category to represent and manipulate files in conflicting state. We provide an
answer by investigating the free completion of the category of files under
finite colimits, and give an explicit description of this category: its objects
are finite sets labeled by lines equipped with a transitive relation and
morphisms are partial functions respecting labeling and relations.