On Wed, Aug 06, 2008 at 06:40:34PM +0200, [EMAIL PROTECTED] wrote:
> Jason Dagit wrote:
> >apfelmus wrote:
> >
> >> It seems to me that the core of darcs is not well-understood. I
> >> mean, the darcs developer have come amazingly far with the
> >> informal model you described in [1] (for darcs 1, what about
> >> darcs 2 ?), but ultimately, it's lacking a well-defined
> >> semantics. For instance, in a commutation X Y <-> Y1 X1 , what
> >> exactly does it mean for Y1 and X1 "to perform the same change as
> >> Y and X"? Why exactly is the trivial choice Y1:=X and X1:=Y
> >> wrong? What about "meaningless" changes? For instance, given the
> >> file
The choice Y1:=X and X1:=Y is wrong because it violates permutivity.
Permutivity is a property that hadn't been formalized when the darcs
manual was written, but is discussed in various talks I've given, for
which the slides are on the web.
> >In an explanation of patch theory that I'm still writing up and
> >refining,
>
> I remember an initial version in the Monad.Reader but haven't heard
> anything since then :)
>
> >I start from the changes and work towards the patches. I think this
> >will help your understanding. Let me give a short treatment here
> >of some of those ideas.
> >
> >I'm going to work with invertible functions on the integers instead
> >of patches because I think it makes the examples easier.
> >
> >Let repository states be the integers and let changes be invertible
> >functions on repository states.
> >
> >Suppose we have a repository in state 1, and we record a change
> >that increments that repository state. Let's call this change
> >Increment and represent it with (+1), like the Haskell increment
> >function. This change would then be defined for all repository
> >states, and we understand what the resulting state would be. But,
> >when you're working with darcs all it would see is something like
> >this:
> >
> >Old State: 1
> >New State: 2
> >
> >So, darcs would represent the more general change with a function
> >that is restricted to work in exactly Old State, so it would record
> >this patch:
> >1 (+ 1) = 2
> >
> >The parens are there to emphasize the existence of the Increment
> >change. Now, suppose we have another change, Increment2, that is
> >defined as (+2), and a patch version of it is recorded right after
> >Increment. So we might have this repository, if we let the empty
> >repository start at state 1:
> >
> >Changes: {Increment2, Increment}
> >Patches: [1 (+ 1) = 2, 2 (+ 2) = 4]
> >Current State: 4
> >
> >With my notation above, I mean that we are holding the changes
> >Increment and Increment2 in a mathematical set. In practice we're
> >really storing the sequence of patches, which is what I represent
> >on the second line.
> >
> >Now, suppose we want to reorder the patches. Notationally we use
> >(.) for function composition. Since both changes are defined for
> >all integers we know that,
> >Increment2 . Increment = Increment . Increment2
> >
> >That is, these functions are commutative. So, it stands to reason
> >that we should also be able to commute their patch
> >representations. What would that look like notationally?
> >
> >Suppose we say the patch "1 (+ 1) = 2" is patch A, and "2 (+ 2) =
> >4" is the patch B. Currently their order is, B . A, but we want
> >patches C and D that correspond to Increment and Increment2 but
> >compose in the other order. The details of how to infer the new
> >patches is darcs' commute operation. It has to examine the patches
> >A and B and infer what their domain and range are and then "adjust"
> >them. Obviously with the example here you could figure it out
> >pretty easily. For example, let C be "1 (+ 2) = 3" and D be "3 (+
> >1) = 4". Then we can have the sequence D . C that has the same
> >effect as B . A but using different patches. The important isn't
> >that the patches are different it's that they are restrictions of
> >the same changes, Increment and Increment2.
> >
> >Do you have suggestions on how to further specify commute? I'm
> >increasingly of the mindset that the details of commute just
> >determine the specific semantics of darcs and are a natural
> >consequence of looking at what it means to apply the different
> >patch types in different orders. Which is to say, it's a very case
> >by case development that you do by inspection.
>
>
> I have no problem with the need for a commute operation (ignoring the
> question whether there might be a different representation of changes
> which eliminates the need for storing patches in sequence
> altogether); what I want to say is that the commute operation itself
> is still under-specified. It is exactly these details of commute that
> I feel need specification, i.e. how to "adjust" domain and range
> "pretty easily". What are these specific semantics of darcs?
>
> One problem is the generalization from patch to change . For
> instance, in your example, we have two patches
>
> A=(1 -> 2) and B=(2 -> 4)
>
> My first edit turns 1 into 2 and my second edit turns 2 into 4. How
> do you know that the first one was the change (+1) and the second one
> was the change (+2)? Why not (*2) in both cases? What about the
> change (\x -> if x<42 then x+1 else x-1)? In other words, there are
> many functions that can turn 1 into 2. However, in this case,
> uniqueness can be restored by restricting the class of functions to
> increments. (The non-uniqueness problem is what I meant with
> "meaningless changes".)
>
> So, your example of integers is simple enough, but what does the
> specification of "change" look like in the case of darcs, or more
> specifically in the case of editing the lines of a text file?
>
> If I understand it correctly, an a priori definition of "change"
> similar to your example Integer -> Integer does not even exist for
> darcs, or more specifically for the problem of editing files with
> Levenshtein's edit operations. (If you had one, you could always
> apply the changes in any order, for they always "do the right thing";
> just like you can apply (+1) and (+2) in any order.). Instead, the
> commute operation is used as a substitute for the non-existent notion
> of "change". (This is a nice trick and entirely fine.) But the
> problem of roughly saying what "change" is doesn't magically go away,
> the commute operation is still under-specified. For instance, what's
> the problem for two patches
>
> 1 apples == A ==> 1 pears == B ==> 1 pears
> 2 bananas 2 apples 2 kiwi
> 3 bananas 3 bananas
>
> to have a commute
>
> 1 apples == B' ==> 1 pears == A' ==> 1 pears
> 2 bananas 2 apples 2 kiwi
> 3 bananas 3 bananas
>
> ? (I know that this example is silly, I want a formal reason why it is.)
This specification isn't part of the "formalism" of darcs, since the
darcs formalism can handle multiple types of changes.
The details of how darcs handles primitive patches is only documented
in the code, simply because (to me) it's a trivial detail that isn't
very interesting. If you'd like to document this, you're welcome to
do so.
> PS: Should we archive this thread somewhere? And anyone please shout
> if you don't want to be CCed.
Yes, it should be on darcs-users.
--
David Roundy
Department of Physics
Oregon State University
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users
