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

Ben Franksen ben.franksen at online.de
Mon Dec 14 14:30:50 UTC 2020


Am 13.12.20 um 11:16 schrieb Ben Franksen:
> However, remember your counter example of a patch universe with only two
> paths with names abc and cba. From the presence of both {a} and {c} we
> can deduce that of {a,c}, but it seems impossible to prove that {b} is
> present. For that we need a fifth axiom (e) analogous to (d) but with
> intersections instead of unions:
> 
> e) If nodes c1 and c2 are present, then c1 ∩ c2 is also present.

This is still not quite insufficient. With the natural numbers as the
set of names, b={}, and t={1,2}, the set C={b,t} would be a valid set of
contexts. But then there is no path from b to t (in fact we have no
patches at all). In general I think we want the patch graph to be
connected. A possible characterization in terms of contexts could be:

(f) For every non-empty context c there is at least one element n of c,
    such that c\\{n} is also a context.

It is then easy to show that a path p:s->t exists if and only if s is a
subset of t.

This variant of abstract patch theory has clean merge and unmerge (of
contexts) already built-in, so to speak, since merging is just taking
the union and unmerging is taking the intersection. I find it
interesting to note that adding conflictors a la Darcs means that we
enlarge the set of contexts by adding /conflicted states/, which are
those corners that we get (in addition to the normal unconflicted
contexts) if we allow arbitrary unions of contexts. Seen in this way,
conflictors appear quite natural and simple, conceptually at least.

Another interesting observation is that we can regard a name as a
partial bijection between contexts. The action of the function is to add
the name to the context and its inverse is to remove it. Its domain and
range are given by

  domain(n)={c∈C|n∉c and c∪{n}∈C}, range(n)={c∈C|n∈c and c\{n}∈C}

The reason I find this interesting is that it hints at a possibility to
re-introduce /concrete/ patches (that is, /patch content/) into the
picture. Concrete (primitive) patches can be seen as partial bijections
on a set S of states, represented as data. Here, too, we can generalize
to finite sequences of patches, which then naturally form a category,
and there is a (non-injective) functor (the "apply" functor) from that
category to the groupoid of partial bijections on states that maps
concatenation to function composition.

We may want to study functors from an abstract patch theory to a
concrete one. A functor maps both objects and arrows. For objects,
F:C->S associates a concrete state to each context (this mapping is also
not necessarily injective). For arrows it associates to each path p:s->t
a concrete patch F(p):F(s)->F(t). The functor laws say that
F(id_c)=id_F(c) and that F(p;q)=F(p);F(q).

This does not a priori mean that each abstract /patch/ (singleton path)
maps to a concrete patch, so I guess we have to require that, in
addition to the usual functor laws. There may be a few more extra
requirements that we want to impose. For instance, I guess we need some
sort of consistency requirement that relates commutation in the abstract
setting to that in the concrete setting. Needless to say, I haven't
thought these things through to the end, so I can't tell yet if it has
any practical relevance.

Cheers
Ben



More information about the darcs-users mailing list