[darcs-devel] type of unravel in V1

Mon Feb 17 23:24:59 UTC 2020

Am 17.02.20 um 13:29 schrieb Ganesh Sittampalam:
> On 16/02/2020 23:01, Ben Franksen wrote:
>> Am 16.02.20 um 22:53 schrieb Ganesh Sittampalam:
>>> I also clarified the witnesses, which I am fairly sure were wrong, and
>>> removed a bunch of unsafeCoerces in the process.
>>
>> I have been at this point a number of times. In fact a while ago I
>> created a long sequence of patches doing exactly this (and some more).
>>
>> I have just uploaded these patches to
>> https://hub.darcs.net/bf/darcs-refactor-v1 . This is raw work in
>> progress and ugly, but for some changes I have written detailed patch
>> descriptions to explain what is going on.
>>
>> The main reason I gave up on this branch was that I think V1 is
>> unfixable. Yes we can clean up the code, but it will always remain
>> either buggy (as it is now) or will be /extremely/ slow
> Given we can't change the existing behaviour, I agree we're very limited
> in what we can do. I think it's still useful to clean up the witnesses,
> and to refactor "unwinding" along the lines you and I have both found
> possible.
> 
> For example, you made exactly the same cleanup to the witnesses for the
> conflicting patch as I've needed to make to get 'fullUnwind' to work.

I didn't mean to discourage you, just wanted to explain why I did not
pursue this further and never published it. By all means, if you can
clean up the code w/o introducing other bugs or getting side-tracked
with trying to fix "everything", go ahead.

>>> However, I did have to introduce a new one, in 'unravel'. There's a bit
>>> of discussion in the code comments about whether the witnesses on
>>> 'publicUnravel' or 'unravel' are correct, with the current conclusion
>>> being that 'publicUnravel' is right, saying that for RepoPatchV1 prim wX
>>> wY, the unravellings should start with wY (whereas unravel says wX).
>>
>> I am certain that the publicUnravel has the correct witnesses.
>> See
>> https://hub.darcs.net/bf/darcs-refactor-v1/patch/3b15dfdcc9c212bd50bc1bd51f70346a42292a4c
>> and especially the patch comment. IIRC  I had eliminated more or less
>> all the unsafe coercions at that point.
> 
> You actually still have a coercion here:
> 
> https://hub.darcs.net/bf/darcs-refactor-v1/browse/src/Darcs/Patch/V1/Commute.hs#396
> 
> which is roughly the same place I'm stuck too - if I change the return
> type of unravel to wY I need the same coercion as you.

Um, yes. I remember now that I succeeded in decoupling the core (merge,
commute) algorithms from unwind; after which this part of the code
became a bit less important to me.

> [Though it seems that pattern-matching on FlippedSeal is better than
> unsealFlipped and eliminates the need for another coercion, not sure why.]
> 
> The fundamental problem is if we start with
> 
>   p :: RepoPatchV1 prim wX wY
> 
> Then unwind, if it includes p, produces:
> 
>   FlippedSeal (RL (RepoPatchV1 prim)) wY
> 
> and after unsealing, we have a new witness wRandom:
> 
>   RL (RepoPatchV1 prim) wRandom wY
> 
> and then newUr produces
> 
>   [Sealed (RL (RepoPatchV1 prim)) wRandom]
> 
> and with two unanchored witnesses of course all hope is lost.

You nailed it.

> I think we end up coercing wRandom to wY, which makes sense in that we
> would expect a conflict resolution to start from the patch type result
> type. But I don't actually understand how the code guarantees that the
> resolution does start there.

I think the deeper reason is that we have no way to express, in the
types, that for a conflicted square @merge (p:\/:q) = q':/\:p'@ the
hidden witnesses for the common start state of the forking and the
common end state of the joining pair are actually the same, at least
effect-wise. When we construct the unwinding i.e. a common history for a
Merger, we unmerge the unwindings of both conflicting patches,
arbitrarily choose one of the branches, and prepend that to one of the
given unwindings; see my implementation of unwind and
reconcileUnwindings. The start state is thus hidden, but in reality we
know that the effects of the original patches (reconstructed via
unmerge) are all reversed in the upper half of the merge.

After we do that, we have one possible history that contains all patches
that are relevant to this particular conflict. We then use newUr to
reconstruct the original tree of patches, at least as far as that is
possible, i.e. unless there is an actual conflict resolution patch in
the way. The loose upper ends (leaves) of this patch tree now correspond
to lots of different states, but the common start state is the same as
the end state before we called unwind; which is why I think the
unsafeCoerce is justified here. Whether we can find a suitable place for
it that reflects the above considerations is another matter.

BTW, now that I write this I think that the unwind code can be
completely scrapped. Because nowadays resolveConflicts no longer has to
be self-contained: we pass a suitable history of patches to it, so there
is no need to reconstruct that.

> Given that understanding, the question is if we could possibly deduce
> that is what is actually happening in the types, or if we just need to
> put the unsafeCoercePStart somewhere strategic. My vote would be for
> either unwind or newUr, depending on what is actually correct.
> 
>> I urge you to take a look at my attempts. I think there is a lot of
>> information there.
> 
> Yep, thanks! It was interesting that you think we can get rid of
> unwindings completely by merging the undos of the underlying mergers
> instead of using the unwindings.

I am pretty sure that the merged undos are exactly the effect of the
unwindings and therefore that this refactor does not change behavior. I
think that I have a patch where I added an assertion that effect (which
I later removed).

> I also thought about removing it but
> had no clue what to do for that case. Still, I'd be quite worried about
> whether we really preserved existing behaviour in doing so.

I believe that at some intermediate state after this particular refactor
I ran all test successfully. Given that we deliberately use a crippled
legacy test case generator so as not to be drowned in failing tests,
this may not mean much.

Cheers
Ben
-------------- next part --------------
A non-text attachment was scrubbed...
Name: pEpkey.asc
Type: application/pgp-keys
Size: 4211 bytes
Desc: not available
URL: <http://lists.osuosl.org/pipermail/darcs-devel/attachments/20200218/862e59a2/attachment.key>