[darcs-users] darcs patch: Haddock some simple functions in Darcs.P... (and 2 more)

[Jason Dagit]

On Wed, Apr 29, 2009 at 2:03 PM, Eric Kow <kowey at darcs.net> wrote:
> Hi,
>
> On Wed, Apr 29, 2009 at 22:40:53 +0200, Reinier Lamers wrote:
>> The patches are OK save for one apparently forgotten word (bottom comment).
>> See below for comments.
>
> Thanks!  I'll apply the ones that pass inspection and amend the next
> one.
>
>> This all seems OK. Though I'd really like to know what the consistency is that
>> the above function checks for.
>
>> >[Haddock Darcs.Patch.Prim.commute_no_conflicts.
>> >Eric Kow <kowey at darcs.net>**20090428192219
>> > Ignore-this: ceb409fe1f07a4329014fa4b4f2244e0
>> >] hunk ./src/Darcs/Patch/Prim.lhs 1012
>> >+    -- | If 'commute_no_conflicts' @x :> y@ succeeds, we know that that @x@
>> > commutes
>> >+    --   past @y@ without any conflicts.   This function is
>> > useful for patch types
>> >+    --   for which 'commute' is defined to always
>> > succeed; so we need some way to
>> >+    --   pick out the specific cases where
>> > commutation succeeds without any conflicts.
>> >+    --
>> >+    --   Consider the commute square with patch names written in capital
>> > letters and
>> >+    --   patch contexts written in small letters.
>> >+    --
>> >+    --   @
>> >+    --          X
>> >+    --       o-----a
>> >+    --       |     |
>> >+    --    Y' |     | Y
>> >+    --       |     |
>> >+    --       z-----b
>> >+    --          X'
>> >+    --   @
>> >+    --
>> >+    --   The default definition of this function that we can mirror the
>> > commutation
>>
>> Shouldn't there be an "assumes" or "states" before the "that"?
>
> I think I meant to say "checks".  Basically this function commutes X
> past Y, and then it commutes -X past Y' and then checks to see if
> we actually get this mirror-image square.
>
>> >+    --
>> >+    --   @
>> >+    --         -X     X
>> >+    --       a-----o-----a
>> >+    --       |     |     |
>> >+    --   Y'' |   Y'|     | Y
>> >+    --       |     |     |
>> >+    --       b-----z-----b
>> >+    --         (-X)'  X'
>> >+    --   @
>
> This idea took me a long time to grasp because I had some trouble
> seeing how I could apply a patch to -X, but then I remembered that
> -X just takes us from some ending state of X to its starting state,
> which is exactly where Y' applies.
>
> Another thing which sort of concerns me is that I'm potentially mixing
> up the notion of context as "set of patches" with that of "state we're
> in" in the sense there could be more than one way to get to the same
> place.  Anyway, I'll sit on this and amend later :-)

Then let me just reiterate one important difference:

Each context corresponds to exactly one specific state[1].  Each state
could be generated by any number of contexts.  That is, there is a
*function* from context to state, but the converse, state to context
is not a function.  State does not uniquely determine the context.
Some contexts (sequences of patches) are not identical, but generate
the same state.  If the contexts are related by commutation of their
sequences then they are equivalent contexts (and also generate the
same state).

[1] This is an important property that no one has rigorously proven,
but it seems to be true.  Future work in this area would be greatly
appreciated.  For example, if we know the exact things that cause this
property to be true or false then we could more easily talk about new
patch types, new commutation rules, and so on.

I expected none of this to be new, but maybe it helps to hear it again.

Jason