[darcs-users] [patch19] Resolve issue1588: add --skip-conflicts option

Ganesh Sittampalam ganesh at earth.li
Fri Oct 30 21:39:25 UTC 2009


On Fri, 30 Oct 2009, Petr Rockai wrote:

> > +commuterIdRL :: CommuteFn p1 p2 -> CommuteFn p1 (RL p2)
> > +commuterIdRL _ (x :> NilRL) = return (NilRL :> x)
> > +commuterIdRL commuter (x :> (y :<: ys))
> > +  = do ys' :> x' <- commuterIdRL commuter (x :> ys)
> > +       y' :> x'' <- commuter (x' :> y)
> > +       return ((y' :<: ys') :> x'')

> I always mix up FL and RL (and more importantly their constructors), but
> anyway, this should lift a commuter on p1 and p2 to a commuter on p1 (RL p2)
> (the type signature says so much). I can't be trusted to understand in which
> order an RL is supposed to apply and on which side the end is written,

Neither can I!

> but as far as I can tell, the function should be correct if the
> witnesses match up.

...so I just work on that principle too :-)

Incidentally commuting a pair in the right order was one of the original 
motiviating examples for witnesses. When we were trying to find a way of 
expressing this kind of thing nicely in the type system, I came up with 
roughly what we have now, but just couldn't get it to typecheck on my 
sample code. Eventually I realised that I'd got my sample code backwards 
so they were behaving exactly as designed.

> It should be probably noted that "ys" is actually treated as an atomic entity,
> although its name suggests it is compound (which in practice it is, but that's
> probably irrelevant from the POV of this function).

Good point, the function originally explicitly took ys as some kind of 
list but at some point I realised I could generalise it.

> Now I just need to figure the inversions...

I often draw pictures, in my head or on paper. We have:

              ^
              |
              ys
              |
---common---> ---x---> ---y--->

and we want to push ys along to the end, i.e. we want (intermediately) ys'
from the following filled in square:

               ---x'-->
              ^        ^
              |        |
              ys       ys'
              |        |
---common---> ---x---> ---y--->

and since we only have ys and x initially and we need to use 
commute so that we are told about conflicts (for some patch types 
merge would just invent a conflictor), we need to turn the pair 
into a sequence somehow, and inverting x is one of ways we can do 
that: (invert x :> ys) <-> (ys' :> invert x')

> (This is a digression, but: I do think that we could benefit from
> clearer and more idiomatic terminology for the patch sequences -- I
> *think* it works to imagine an RL as a stack and and FL as a "normal"
> list... when I was toying around with these things, it also helped me to
> actually write RLs with their head to the right instead to the left as
> darcs does -- so that patches always apply from left to right as written
> in the code, but can be popped/pushed on different ends, depending on
> orientation of the list... but I guess this is all matter of different
> intuitions...)

I definitely agree about the left->right aspects of it, I have exactly the 
same problem. One issue is that the arrows in the constructors point 
towards the right (of the patch sequence), and if we swapped RL around 
we'd have to use something a bit longer for the constructor, or give up on 
that convention (which might be ok, since we'd now have visual order as a 
cue).

Re the names FL/RL, I agree that they are a barrier to comprehension, but
I'm not sure how we can improve on them - stack/list doesn't work well for 
me, partly because they aren't obviously symmetric, and partly because
neither really has a canonical "direction", at least to me.

Cheers,

Ganesh


More information about the darcs-users mailing list