[darcs-devel] conflict resolution

[Ben Franksen]

I just found this email in my drafts folder and I think it would be a
waste not to send it, so...

Am 20.07.19 um 20:21 schrieb Ganesh Sittampalam:
> On 20/07/2019 09:53, Ben Franksen wrote:
>> In Darcs, a conflict count as "resolved" if some other change depends on
>> it. Whether this is a good user interface or not is a different
>> question, more on that below. For the moment, let us just consider the
>> internal logic and accept the UI as is.
> 
> I've also had my doubts about that piece of logic, given it has the flaw
> you identified.
> 
> Doing something at the Named level makes some sense, but would we then
> keep the existing logic too?

That was the plan.

> We end up with a hybrid story where you can
> resolve a conflict either by an implicit dependency at the Prim level or
> an explicit dependency at the Named level.

You can already declare it resolved by recording a tag. My proposal only
generalises this to other explicit dependencies.

The main disadvantage of resolving conflicts in this way is that it is
rather coarse-grained.

> Maybe that's ok as long as "this conflict is resolved" is purely a UI
> issue in the sense that it stops darcs mark-conflicts from presenting
> the conflict again. But if we ever wanted the concept to have a deeper
> meaning, e.g. in patch semantics, I think we should look for something
> simpler.

I am not sure I get what you mean here. Isn't the rule:

  * A conflict is resolved if another patch depends on it.

doing exactly that i.e. give conflict resolution a meaning in patch
semantics? I don't think we can devise anything simpler (that still
gives a good approximation of what it means intuitively).

To make this absolutely precise, let me give two more definitions:

  * A (direct) conflict is an (unordered) pair of patches in a repo that
    can be commuted to a common context, such that (in this context)
    they cannot be merged cleanly.

  * A patch depends on a conflict if it depends on either one of its
   (two) elements.

These definitions make it quite clear that this is not a concept that
makes sense for prim patches: any two prims in a sequence that can be
commuted to a common context cleanly merge. Thus talking about resolving
conflicts at the prim level is vacuous.

Which leads me to:

> Another idea that occurs to me while writing this is that you can 
> resolve a conflict between the deletion of the same hunk twice by 
> recording an empty hunk at the specific line in question. This isn't a 
> sensible idea right now because I think darcs assumes hunks are 
> non-empty (and I have a vague feeling it might even treat them as 
> identities in some cases). But it could give us a more principled 
> approach for resolving conflicts purely at the Prim level, if we can 
> always find a similar "null patch" for non-hunk cases, e.g. moving a 
> file to itself.

In light of my above attempts to make precise what we mean with
"conflict" and "resolved", this is only related to conflicts insofar as
it is about dependency.

What you propose here is to allow the higher patch levels to delegate
the addition of "semantic" dependencies to the prim patch layer by
adding new sorts of prim patches that have no effect but cause extra
dependencies. I agree that this has a certain charm in that these extra
dependencies are now defined without recourse to patch identities. And
it allows dependencies to be added (and thus declare conflicts to be
resolved) in a more fine-grained manner.

I also got an idea, now that I wrote all this ;-)

Allowing null patches at the prim level is problematic, as you noted,
because a null patch naturally commutes with everything. Indeed this is
the case when we consider sequences of prims, where we do have "null
patches": NilFL and NilRL. So adding specific null patches that don't
behave like that requires an incompatible change to prim patch semantics.

Instead, we could create these null patches as /sequences/ of prim
patches. Specifically: to depend on a prim p without causing an effect,
we add [p^;p]. This is /precisely/ what we want, as p^;p represents (via
the apply functor) the /partial/ identity function on repo states,
namely the one that is defined only on the range of p.

As an optimization, we can lift the idea to the RepoPatch layer.
Concretely, I am thinking of adding a new constructor to RepoPatchV3:

  Dependor :: Contexted (NamedPrim prim) wX -> RepoPatchV3 prim wX wX

A Dependor consists of a single contexted prim patch (ps;p) (as usual
the context is kept minimal) and semantically behaves exactly like
(ps;p;p^;ps^). It is self-inverse (so fortunately we don't need to add
Rodneped), its effect is NilFL, and the commute and merge rules follow
directly from the semantics. But they can be optimized e.g. commuting a
prim past a Dependor means we have to commute the Prim (only) past
(ps;p) i.e. the context and the prim itself. (Side note: a Dependor has
the same internal representation as a Duplicate in V2, modulo prim patch
identities. Can we learn something from that?)

Cheers
Ben