Re: How to extend a patch theory to fully commute

Am 19.08.20 um 11:44 schrieb Ben Franksen:
> The fact that your patches have no "content" is of of course a result of
> starting out with "enriched" contexts. As you note in 2.2
> Interpretation, your contexts can *not* in general be understood simply
> as "working tree states": the mapping from contexts to states is not
> injective. It is not yet clear to me if that will have consequences when
> it comes to implementing your theory.

Let me elaborate this point a bit.

Your theory assume the existence of contexts as a "set". That doesn't
give us any hint as to how these contexts should be represented in a
concrete implementation. If we start out with some notion of prim patch
(such as the one in Darcs), then these exist as concrete representations
of state changes as data. But we know that states do not correspond 1:1
to contexts. The simplest example involves duplicate prim patches p, q,
such that name(p)/=name(q), but repr(p)==repr(q). Assuming a starting
context X for both p and q, the ending context is different, even though
the end state is the same. More interesting examples involve things like
(remove f; add g) versus (move f g).

The question now is: how can we arrive at a suitable definition (i.e.
representation) of context, given such a concrete definition of prim
patches and states?

The answer, in Darcs at least, is to not define contexts. Contexts
aren't represented at runtime at all. Instead, in our code contexts
exist only formally at the type level.

Your definition of context address may require that we have a way to
reify contexts as data. A natural way of arriving at a suitable
definition is to go backwards from patches: identify a context with the
set of all patch sequences that start at the empty state and that differ
only by commutation. At this point I am always tempted to say "and
elimination of inverses"; indeed your definition of a patch universe
implies that a sequence [a;b;b^] really has the same start and end
context as the plain [a]. But with respect to commutation this doesn't
seem right: [a;c] may commute to some [c';a'], but [a;b;b^;c] may not,
because e.g. [a;b] may not commute. Every time I think about this I am
getting head-aches. I cannot reconcile these two points of view.

Anyway, assuming we have sorted this out somehow, I am still having
doubts about reifying contexts, because the definition as an equivalence
class of sequences does not easily map to an efficient representation.

Cheers
Ben