Here is the promised Theory module.
Note that this is work in progress. In particular, regarding sequences of
patches as a groupoid, and the apply functor as a functor between groupoids,
requires that we can cancel inverses from a sequence of patches. I have some
doubts that this correctly models how patches behave in Darcs, since
presence or absence of a pair of inverse patches does have an influence on
commutation behavior. In particular, if it were true, then
commute(q:>[p;p^]) would always have to succeed, for arbitrary (welltyped)
p and q.
This is something that really vexes me. We /do/ cancel out inverses when
constructing (minimal) contexts for named prims in the RepoPatchV3
implementation. So there must be conditions under which this is sound. My
current thinking is that it works because the prims in question have
explicit identities. This means that when we have [p;p^] we /know/ that one
of them is an "original" patch (i.e. coming from some named patch in our
repo) and the other is /not/ and merely a result of some internal
manipulation. It also means we know we can always commute p and p^ into
proximity. None of this is true for unnamed prims, where being inverses is a
matter of accident i.e. the p^ could be a completely unrelated "inverse
duplicate" of p. Indeed, for patches with an explicit identity inversion is
a much more restricted (and thus more wellbehaved) operation. I guess this
means the formulation in terms of groupoids can be saved if we require patch
identities from the start.
Fortunately the proof of npermutivity from 2 and 3permutivity doesn't
depend on that, so it should go through even for unnamed prims.
1 patch for repository http://darcs.net/screened:
patch 0fec6ddeafa61241cfe33d7c6e03187d0e57b5d3
Author: Ben Franksen <ben.franksen@online.de>
Date: Fri Mar 15 18:23:52 CET 2019
* WIP add module Darcs.Patch.Theory
Attachments
