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
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users
