[darcs-users] Write-up on "tree repositories" as an alternative to conflictors

[Ben Franksen]

I would start the whole thing with a slightly different definition.

Let N and C be sets. Elements of N will be called names and elements of
C will be called contexts. Let G be a directed acyclic N-labelled
C-graph. In other words, an edge in the graph is an element of P:=C*C*N.
The edges are called patches. We refer to the first, second, and third
member of such a tuple using the functions source, target, and name:

  source :: P -> C    source (s,_,_) = s
  target :: P -> C    target (_,t,_) = t
  name   :: P -> N    name   (_,_,n) = n

The free category on G is defined as having C as its objects, and the
finite paths (sequences of edges) in the graph as arrows. The
composition is concatenation of paths, and the identity at context c is
the empty path starting and ending at c. We write composition as plain
juxtaposition, or,  when required for disambiguation, as p;q.

We extend the three functions above to paths. The source of a path is
the source of its first patch, the target is the target of its last
patch, and the name of a path is the set of names of its patches:

  name(p1,...,pn)={name(p1),...,name(pn)}

This is indeed an extension if we identfy a name with the singleton set
consisting of just that name.

As usual in category theory, we write p:s->t to indicate that
source(p)=s and target(p)=t. We also identify patches with one-element
sequences, so the same notation applies to single patches.

A set of paths S is called parallel if all members have the same start
and end i.e. there are s and t in C such that p:s->t for all p in S.

We call G=(N,C,P) a patch graph, and its free category a patch theory,
if the following holds: for any finite set of parallel paths, all its
members have the same name. (Remark: This is obviously equivalent to
requiring it only for two-element sets.)

The usual patch laws then all follow from that.

We can define the clean merge of two paths as follows. Let p and q be
paths with the same source. A clean merge of (p,q) is a then a pushout,
in other words, another pair of paths (q',p'), such that pq' and qp' are
parallel, and such that q',p' are minimal in the sense that for any
other such pair (q'', p'') there is a unique path r such that q'',p''
factors through r; that is, p''=p'r and q''=q'r. It follows from the
defining property of a patch theory that name(pq')=name(qp'), but I
think it should also be possible to deduce

  name(pq') = name(p) U name(q)

using the universal property (minimality) of the merge. Indeed I think
both definitions are equivalent. Note that any such merge must
necessarily be unique (because pushouts are unique).

Again, I think this immediately generalises to arbitrary finite sets of
forking paths, where a set of paths is called forking if all its members
have the same source, and joining if all its members have the same
target. A clean merge is thus a bijective function m from a forking set
S with source s to a joining set T with target t, such that

  p;m(p) : s -> t for all p in S

and such that for all p in S, name(m(p)) is a subset of Union {name(q)|q
in S}.

Cheers
Ben