On Sun, Jun 17, 2007 at 12:50:28PM +0200, Eric Y. Kow wrote: > Argh... Sorry, here is perhaps a more readable version. > > General comments and questions > ------------------------------ > 1) This does not compile with GHC 6.4.1, even without type witnesses. > It complains about the constructors :/\: (and friends). Unless we > can issue a fix rather quickly, we will have to require GHC 6.6 for > the next release. Is that ok with you?
I think that's okay with me. Particularly if Tommy doesn't pull these patches straight in, so if a bugfix release is needed that could be done without requiring 6.6. The infix types are somewhat gratuitous, but I like them: we avoid having to invent a new name for each of these patch relationships. And anyone who wants to learn the code is going to have to learn the visual mnemonics anyhow. > 2) The new code will not parse/understand/ commute mergers. Is > this correct? If so, I'm guessing you are planning some sort > of repository conversion tool (à darcs optimize or upgrade). > How do you reckon that would work? That is, what do mergers > translate to? I don't expect that the next release of the code will be compiled with type witnesses, so we'll still have the merger code compiled in. My expectation is that the type witnesses will be used (for a while yet) as a development tool, to make sure our code is safe. Since we don't plan on modifying the merger code, and it's very, very complicated and ugly, it's easiest to leave it untouched. > 3) I was wondering if there really exists such a thing as an empty > composite or split patch (NilFL). Since we now have control > over our own list type, would it be worthwhile to have lists > that are guaranteed to have at least one element in them? You seem > to be using ComP NilFL to double as an 'identity patch' (is that used > just for internal purposes?). If this is the sole use of empty patch > lists, maybe have a constructor just for that? Split patches are going the way of the dodo, so it's really just empty composite patches. We are indeed using ComP NilFL as the identity patch. I don't see a real benefit to making composite patches be non-empty and having a separate type for an identity patch. Given that we don't have a separate primitive-non-empty-patch type, I think it'd just be awkward. It'd be nice to have such a type, but at the moment we're actually trying to not make *too* invasive changes to the code (although it might not seem like that). > unsafeCoerce# > ------------- > > - p1_modifies /= p2_modifies = Succeeded (p2 :< p1) > > + p1_modifies /= p2_modifies = Succeeded (unsafeCoerce# p2 :< > > unsafeCoerce# p1) > > As I understand it, the unsafeCoerce#s are used for forcing the type > witnesses. I wonder then if we could have a somewhat safer wrapper > like > unsafeCoercePatch :: Patch C(x,y) -> Patch C(a,b) > > Just to avoid, for example, unintentionally coercing something > completely unrelated because of a bracketing typo. Yeah, that'd be a reasonable idea. Except that we'd also need a separate unsafeCoercePatchFL. But I fervently hope to reduce the number of unsafeCoerce#s to the point where we can (and will) vigorously review each use. > MergeFunction > ------------- > > +new_merge :: (Patch :\/: Patch) C(x,y) -> Maybe ((Patch :/\: Patch) C(x,y)) > > +new_merge (p1:\/:p2) = do ip1' :< p2' <- commute (p2 :< invert p1) > > + return (p2' :/\: invert ip1') > > Would a MergeFunction type be useful? > > type MergeFunction = (Patch :\/: Patch) C(x,y) -> Maybe ((Patch :/\: Patch) > C(x,y)) Maybe, but I'm not sure how often it'll show up. Merging is the next thing on Jason's TODO list (merging sequences involving conflicting patches), so he'll be taking a look at how we want to structure things tomorrow. > Canonize > -------- > > - liftM2 (merger g) (canonize p1) (canonize p2) > > + (merger g) (canonize p1) (canonize p2) > > I am somewhat concerned about this. As I understand it, we replace the > Nothings with an identity patch (ComP NilFL). Fine. But in places like > this, does this mean we lose this idea of failures propagating in the > Maybe monad? For example, does the example above really behave the same > way (or does it really not matter?). > > I confess that I wasn't able to figure what returning Nothing means. > Does it mean that canonization "fails" in some way? It used to mean that canonization failed, but then switched to mean that canonization returned an identity patch. In this case, the canonization can't return Nothing for the subpatches, or we'd have serious trouble. In fact, we really should never be canonizing mergers at all. It changes the structure of a patch, and so it can't be done on a recorded patch, and we shouldn't have mergers except in recorded patches... > > -canonize p@(FP _ (Binary old new)) = if old /= new then Just p > > - else Just null_patch > > Another thing is that now Just null_patch and Nothing are collapsed into > a single type of result, the identity patch. Is that ok? Yeah, as mentioned above the meaning of the return result of canonization changed, which introduced this redundancy. There were also places that had multiple checks if the canonization returned Nothing or a null_patch. > Conflicted > ---------- > (with David's modifications) > > A Conflicted patch is (as I understand Jason's mail) a storage mechanism > on top of which the cancellation patches will be implemented. A > conflicted patch consists of a patch and a sequence of patches (a patch > context). I'm guessing that we call it this because it is something we > generate when there is a conflict. > > Jason, can you explain to me what the relationship is between the two? > For example, why don't we just have a list of patches? I know you asked Jason, but as long as I'm replying... Yes a Conflicted patch is a patch that has run into a conflict. It's going to serve as the placeholder for primitive patches that have no effect because of a conflict. Conflicts, in the new system, will have non-local effects, meaning that when you pull a patch it may modify the files describing patches already in your repository (if there's a conflict, or a cancellation patch involved). These scary non-local modifications will be implemented by replacing the affected primitive patches with Conflicted patches, which has the benefit of being a locally reversible process (i.e. if we were to lose the patch that caused the conflict, we could still reverse its effects, just by converting Conflicted patches into ordinary ones (which involves some commutation, obviously). > Conflicted patches always commute, although how they commute depends on > what they commute with. There are three cases that are looked at in > order > > 1. we are commuting with another Conflicted patch > trivial: just do it > 2. we try commuting with something that does not conflict with us > (Conflicted p1 cs) :> p2 > ok... > p1 p2' cs' > p2'' p1' cs' > and we return > p2'' :> (Conflicted p1' cs') > > Yeah, this is redundant, but it sometimes helps me to just > work through things Except that p2'' is the same as p2 (unless there's a bug) because a Conflicted patch has no efect. > 3. we try commuting with something that _does_ conflict with us > swallow it (black magic) Yes. > > -- If the confilcted patch or the context does not commute with the > typo :-) > > -- other patch then we need to add the other patch to the context of > > -- the conflicted patch. > > -- The hard case here, is doing the inverse commute. To work correctly > > -- we must make sure that the context has the correct patch at the end. > > -- Otherwise we cannot find it to remove it from the context. > > conflicted_commute_depends :: CommuteFunction > > conflicted_commute_depends (Conflicted p1 csp2 :< p2) | > > ((lastc:<:initcs):_) <- filter (\(lastc:<:_) -> isEq (p2 =/\= lastc)) $ > > last_permutations csp2 > > = case p2 =/\= lastc of > > IsEq -> Succeeded (p2 :< Conflicted p1 (reverseRL initcs)) > > _ -> impossible > > conflicted_commute_depends (Conflicted p1 cs :< ip2) = > > Succeeded (ip2 :< Conflicted p1 (cs+>+invert ip2:>:NilFL)) > > conflicted_commute_depends _ = Unknown > > I haven't really tried to understand this code. Sorry. > > By the way, could you explain what the Proof stuff is for? Just for > grabbing patches which don't modify context, for example, Conflicted > patches? I'm guessing filterE would still have a use even though it is > no longer in this code? I'm not sure. It seemed like a good idea at the time, but didn't work. We'll see if it's useful. The idea of a Proof was to have a data structure that encapsulated an IsEq and a data object, to simplify pattern matching. i.e. if we've proven that types x and y are the same, it'd allow us to avoid redundant runtime checks that this is the case. But I'm not certain that there really is a use for filterE. The use we designed it for wasn't possible, because one of the two types we wanted to prove were identical was unknown at the time we called filterE (an existential that we couldn't look at until we opened up the FL). > Sealed > ------ > > +data Sealed a where > > + Sealed :: !(a C(x,)) -> Sealed a > > Thanks to Ian and Ganesh's gracious help, I was able to make more sense > of this code. My stumbling block was forgetting that you could curry > type parameters, so I was mentally substituting > Sealed :: Patch x -> Sealed Patch > > which confused me. Maybe a little notational tweak might help lead > readers a bit, something like > Sealed :: !(px C(,y)) -> Sealed p you mean Sealed :: !(px C(,y)) -> Sealed px right? > > +unseal :: Sealed a -> (FORALL(x) a C(x,) -> b) -> b > > +unseal (Sealed a) f = f a > > Similarly, > unseal :: Sealed px -> (FORALL(y) px C(,y) -> b) -> b Yeah, that would be a good idea. I also want some day to get rid of that stupid comma in C, so it'll be C(y), and C(x,y) will become C(x y). It'll just make it prettier and more flexible, I think. -- David Roundy http://www.darcs.net
signature.asc
Description: Digital signature
_______________________________________________ darcs-devel mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-devel
