[darcs-devel] Semantics of witnesses

[Ben Franksen]

Rather belated addition on an interesting discussion:

Am 12.08.19 um 23:26 schrieb Ben Franksen:
> Am 12.08.19 um 22:54 schrieb Ganesh Sittampalam:
>> On 12/08/2019 13:27, Ben Franksen wrote:
>>> your last remark may point a way to reconcile our two views. Indeed it
>>> is true that every patch has a unique minimal context and that this
>>> minimal context is an invariant property. (I am using the traditional
>>> definition of context here: the set of patches preceding a patch in a
>>> repo.) This in turn gives us a /canonical/ initial state for each patch
>>> (apply the minimal context to the empty state), which is then also an
>>> invariant property of the patch.
>>
>> The minimal context is definitely an invariant property of the patch
>> (i.e. the thing that can be commuted into lots of different contexts,
>> possibly changing representation). I don't think it helps us with
>> invariant properties of patch representations though.
> 
> Oops. You are right, of course: the minimal context rather corresponds
> to set (4) than set (2).

I wonder if the minimal context idea could be adapted to set (2). All we
need to do is check that, after commuting, our patches are structurally
equal to the input patches.

This is currently just a theoretical consideration.

To avoid ambiguities about what exactly structural equality means for
compound patches we could define new operations that are like commute
but fail if the commute isn't trivial. We need to distinguish whether we
want this property for the left or the right patch, so we'd add two new
methods:

  trivialCommuteL :: CommuteFn p p
  trivialCommuteR :: CommuteFn p p

Building on these, and the regular commute, define

  trivialCommuteWhatWeCanRL :: <same type as commuteWhatWeCanRL>

to minimize any concrete given contex.

However, for this to be useful we'd have to know if trivialCommuteR
satisfies enough patch laws; in particular, we'd need permutivity for
trivialCommuteR and I am not sure it holds even for Prim.V1.

Cheers
Ben