[darcs-devel] toy patch code

[Ben Franksen]

Good idea to take this off the tracker.

Am 31.08.19 um 18:02 schrieb Ganesh Sittampalam:
> On 31/08/2019 16:13, Ben Franksen wrote:
>> Ben Franksen <ben.franksen at online.de> added the comment:
>>>> This could be used for far more than just examining a few concrete
>>>> examples we find interesting. For instance, I find it interesting to
>>>> investigate which definitions of 'conflicts' / 'dependencies' satisfy
>>>> our patch laws. E.g. does permutivity hold for the example type you
>>>> defined? How large is the (finite!) set of possible 'dependencies' such
>>>> that all your patch laws hold? Can we combine conflicts and dependencies
>>>> into a single data structure, something like a matrix?
>>>
>>> I've been doing more with it off and on to try to get a better handle on
>>> some underlying model for conflictors, in particular looking at things
>>> like minimal contexts and how those relate to the patches actually
>>> mentioned in the conflictor. I'd like to get some higher-level
>>> understanding of the rules for commuting conflictors, not just the
>>> operational description we have at the moment. I haven't really figured
>>> out anything illuminating yet though.
>>
>> And ultimately it all comes down to establishing general permutivity
>> (for all n>=2 and including consistency of failure). I am convinced it
>> should be possible to formally derive the commute rules from that
>> requirement.
> 
> Plus satisfying the high-level properties we expect about when a patch
> is in conflict or not. The thing that makes it quite awkward, at least
> each time I think about it, is that you need 2 patches to be a conflict
> (and hence have their effects nullified). So there's this weird
> discontinuity when a conflicting set changes size from 2 to 1.

Yes. I would be interested in your considerations where this
'discontinuity' comes up.

>> I have also come to see merging as the more fundamental operation
>> compared to commuting. The direct definition of cleanMerge is nicely
>> symmetric and easy to understand. I really should rebase the patches and
>> send them.
> 
> But does it really cover the harder cases in commute?

Well, I don't know which cases you see a the hard ones. I always found
the non-conflicting commute more difficult to understand, and in
particular the ones involving inverse conflictors.

> As I've been
> playing with the examples, my feeling is that what's complicated is not
> "do these things merge" (whether cleanly or not), but "can we undo a
> merge" that might have happened in the past (or never actually happened,
> but could have done).

You mean the conflicted commute? I always found them quite
straight-forward: just look at what a conflicted merge produces and undo
that.

>>>> Furthermore: your ApplyState is trivial, which is okay for the purpose
>>>> you had in mind. But I wonder: is it possible to construct, for every
>>>> finite PrimCore-like type and each set of conflicts and dependencies
>>>> such that the patch laws hold, a suitable "model" of a state, such that
>>>> sequences of the corresponding Prim type map to (all) partial bijections
>>>> on that state?
>>>
>>> A state could just be a set recording the PrimCores already applied.
>>
>> Yes, I guess this is how one would abstractly construct one concrete
>> ApplyState. However, the set (or type) of all ApplyStates has a bit more
>> stucture, as not all such sets are valid states. I was curious about a
>> more declarative way to characterize the states i.e. the allowed sets.
>>
>>> But I'm not sure what use it would be at the moment.
>>
>> Just pure fun mathematics :-) It would shed light on the algebraic
>> structure of patch algebras. For instance, as these are prim patches, no
>> two elements may be in the set that are conflicting. And for each
>> element, it must also contain its dependencies. Note how the first
>> condition limts what we may add to an existing (valid) set, and how the
>> latter limits what we can remove from it.
> 
> Yeah, and I think that's really all the structure there is.

Yes, perhaps.

> But the structure of states for conflictors is much less clear to me.

Yes, this is interesting indeed.

> First I thought that you just need two sets of PrimCores, one that's
> active and one that's inactive, and that you could uniquely determine
> what should be in the active set and the inactive set just from the full
> set of PrimCores - just put all the ones that have a conflict with any
> other one in the inactive set, and the rest in the active set.
> 
> But then I realised that the contexts are more complicated. Let's make
> our notation be
> 
>   <active PrimCores|inactive PrimCores>.
> 
> If you have S, T and U which all conflict, then you can construct the
> state <|S,T,U> simply by constructing three repos each with one of them
> in and merging them.
> 
> But you can also construct <U|S,T> by first merging S and T and then
> recording U as the resolution of S and T.

Isn't that a completely different U than the one we had before?

> So the full context in which a patch is recorded matters, not just the
> context of active primitives.

This doesn't surprise me at all. If it were indeed as simple as you
thought then we wouldn't need the set of conflicts in a conflictor,
wouldn't we? There is more to a conflictor then just what it reverts.
This is obvious if you think of conflicting conflictors, where the set
of prims that the second one reverts is usually empty, at least doesn't
contain the patch it conflicts with... because that is already inactive.

> So then I started playing with the minimal
> contexts of each patch in all possible repos. But I haven't learnt
> anything interesting. (Latest code attached, anyway, completely
> undocumented).

Thanks, may take me some time to look at that. I am still not sure what
you wnated to achieve with these experiments, I'd be interested in
further explanations.

Cheers
Ben