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 (well-typed)
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 well-behaved) 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 n-permutivity from 2- and 3-permutivity 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

• patch-preview.txt
• unnamed
• wip-add-module-darcs_patch_theory.dpatch

Would the darcs code or tests end up depending on this module? If not,
does it belong in the darcs codebase proper? Perhaps there's still
value in the haddock appearing alongside the rest of darcs.

> Would the darcs code or tests end up depending on this module?

I am not sure but I don't think so. My original plan was to gather all
the class properties there instead of them being scattered among all the
classes/modules. It would be perfect if in the documentation for the
classes we could refer to the Theory module but I guess this would
result in cyclic dependencies...

> If not, does it belong in the darcs codebase proper? Perhaps there's still
> value in the haddock appearing alongside the rest of darcs.

The generated docs are (currently) the only reason the module exists at
all. If you want to read it you should definitely look at that and not
the sources. (The reason I sent the patch is so you can apply, run cabal
(new-) haddock and read it! I wasn't planning to screen it any time soon.)

What I like about having it in haddock format inside the code base is
that we can reference code items. The kept the theory pretty close to
the actual source code; the only major deviation is the Apply class: I
treat ApplyState as tagged with a witness and regard apply as a pure
function (which is now also total, due to the witnesses). You can always
jump directly to the docs for the actual definitions; and I don't have
to repeat every detail, for instance most of the data types defined in
Darcs.Patch.Witnesses are only informally described in the theory.