[darcs-users] darcs patch: partial type witnesses in Unrevert (and 44 more)
Jason Dagit
dagit at codersbase.com
Wed Aug 27 20:30:38 UTC 2008
On Wed, Aug 27, 2008 at 1:22 PM, David Roundy <droundy at darcs.net> wrote:
> On Wed, Aug 27, 2008 at 01:14:56PM -0700, Jason Dagit wrote:
>> On Wed, Aug 27, 2008 at 12:06 PM, David Roundy <droundy at darcs.net> wrote:
>> > On Wed, Aug 27, 2008 at 09:56:32AM -0700, Jason Dagit wrote:
>> >> David,
>> >>
>> >> This is the resend you requested.
>> >>
>> >> I can't be sure that the individal patches below will compile by themselves, but
>> >> I know they result in a working darcs when applied together. Hopefully,
>> >> sending like this will make it easier for you to review them!
>> >
>> > I've applied:
>> >
>> > Wed Aug 27 12:53:27 EDT 2008 Jason Dagit <dagit at codersbase.com>
>> > * updates to Repository.Internal to fix conflicts and support type witness refactor in commands
>> >
>> > Wed Aug 27 00:40:25 EDT 2008 Jason Dagit <dagit at codersbase.com>
>> > * fix error in Properties due to new commuteFL
>> >
>> > Wed Aug 27 00:13:44 EDT 2008 Jason Dagit <dagit at codersbase.com>
>> > * fix minor type witness compile error with new commuteFL
>> >
>> > Wed Aug 27 00:13:21 EDT 2008 Jason Dagit <dagit at codersbase.com>
>> > * fix conflicts with get_extra changes
>> >
>> > Sun Aug 24 21:18:10 EDT 2008 Jason Dagit <dagit at codersbase.com>
>> > * improve reporting for bug in get_extra
>> >
>> > Mon Aug 25 14:59:07 EDT 2008 Jason Dagit <dagit at codersbase.com>
>> > * Finish refactor of Unrevert as well as making it pass double-unrevert.sh
>> >
>> > Mon Aug 25 14:32:35 EDT 2008 Jason Dagit <dagit at codersbase.com>
>> > * add double-unrevert.sh test
>> >
>> > Wed Aug 13 01:38:37 EDT 2008 Jason Dagit <dagit at codersbase.com>
>> > * partial type witnesses in Unrevert
>> >
>> >
>> > but I've spent most of my time reviewing the changes in
>> > Repository.Internal, and ended up reverting many of those changes
>> > (which were wrong).
>> >
>> >> [updates to Repository.Internal to fix conflicts and support type witness refactor in commands
>> >> Jason Dagit <dagit at codersbase.com>**20080827165327] hunk ./src/Darcs/Repository/Internal.lhs 336
>> >> get_unrecorded :: RepoPatch p => Repository p C(r u t) -> IO (FL Prim C(r u))
>> >> get_unrecorded = get_unrecorded_private id
>> >>
>> >> +-- | The /unrecorded/ includes the pending and the working directory changes.
>> >> get_unrecorded_private :: RepoPatch p => ([DarcsFlag]->[DarcsFlag]) -> Repository p C(r u t) -> IO (FL Prim C(r y))
>> >> get_unrecorded_private _ (Repo _ opts _ _)
>> >> | NoUpdateWorking `elem` opts = return $ unsafeCoerceP NilFL
>> >> hunk ./src/Darcs/Repository/Internal.lhs 573
>> >> decideHashedOrNormal rf $ HvsO {hashed = HashedRepo.apply_to_tentative_pristine c opts p,
>> >> old = DarcsRepo.add_to_tentative_pristine p}
>> >
>> > It looks pretty clear to me that tentativelyAddToPending is still used
>> > in a buggy manner. It's only used three times, but two of those make
>> > differents assumptions (the third is in Get, where we know there are
>> > initially no local changes), so fixing a bug in Unrevert will be
>> > guaranteed to create a bug in Unrecord (but in the command
>> > obliterate).
>>
>> Well, the way I started thinking about tentativelyAddToPending is that
>> the pending has context C(r w), where w is the working copy context
>> (and thus the unrecorded changes are (pend +>+ working) :: C(r u). We
>> don't track the working copy context. That's why I changed it to x in
>> the type sig of tentatvelyAddToPending. Even if we add tr and tu to
>> the repository state below we're not tracking the working copy
>> context. Furthermore, as I understand it, even if we do track the
>> working copy context we'd still have the burden of proving that
>> sometimes w = r in some of the commands.
>>
>> >
>> >> -tentativelyAddToPending :: forall p C(r u t y). RepoPatch p
>> >> - => Repository p C(r u t) -> [DarcsFlag] -> FL Prim C(u y) -> IO ()
>> >> +-- | This fuction is unsafe because it accepts a patch that works on the tentative
>> >> +-- pending and we don't currently track the state of the tentative pending.
>> >> +tentativelyAddToPending :: forall p C(r u t x y). RepoPatch p
>> >> + => Repository p C(r u t) -> [DarcsFlag] -> FL Prim C(x y) -> IO ()
>> >> tentativelyAddToPending (Repo _ opts _ _) _ _
>> >> | NoUpdateWorking `elem` opts = return ()
>> >> | DryRun `elem` opts = bug "tentativelyAddToPending called when --dry-run is specified"
>> >> hunk ./src/Darcs/Repository/Internal.lhs 585
>> >> let pn = pendingName rt
>> >> tpn = pn ++ ".tentative"
>> >> Sealed pend <- readPrims `liftM` (gzReadFilePS tpn `catchall` (return nilPS))
>> >> - FlippedSeal newpend_ <- return $ newpend (unsafeCoerceP pend :: FL Prim C(r t)) patch
>> >> + FlippedSeal newpend_ <- return $ newpend (unsafeCoerceP pend :: FL Prim C(a x)) patch
>> >> writePatch tpn $ fromPrims_ newpend_
>> >> where newpend :: FL Prim C(a b) -> FL Prim C(b c) -> FlippedSeal (FL Prim) C(c)
>> >> newpend NilFL patch_ = flipSeal patch_
>> >
>> > ..
>> >
>> >> tentativelyRemovePatches :: RepoPatch p => Repository p C(r u t) -> [DarcsFlag]
>> >> - -> FL (Named p) C(x t) -> IO ()
>> >> + -> FL (Named p) C(x r) -> IO ()
>> >> tentativelyRemovePatches = tentativelyRemovePatches_ UpdatePristine
>> >
>> > The former definition is correct. A quick look at
>> > tentativelyRemovePatches_ shows that it is in fact the tentative
>> > inventory that is being modified, which requires that the patches be
>> > in the context of the tentative state.
>> >
>> > But it's a bit vague since with our current type witnesses 't' is
>> > always guaranteed to be the same as 'r', and there is no correct
>> > answer. Certainly with the type you've given this function, if it's
>> > called twice it will corrupt the repository. (It isn't called twice,
>> > but the type system can't check this, and there are reasonable reasons
>> > to call it twice, or to use some other repository-modifying command
>> > afterwards.)
>>
>> As you said in a different email, we don't have a way to track state
>> mutation with the type witnesses. As you said here, we don't separate
>> tentative recorded (tr) from tentative unrecorded (tu). Which, as I
>> tried to point out in a different email (off list) which you said you
>> didn't read in detail, would be required to solve this ambiguity. As
>> such, I've pretty much stopped using the 't' type and I was tempted to
>> just remove it for now but have trouble justifying that work when I
>> could probably replace it with tr and tu for a similar amount of
>> effort. Then once I'm done adding tr and tu I'd run head first into
>> the problem of tracking the mutations of state.
>>
>> We've rolled around ideas about tracking those mutations, but it seems
>> that doing it in a safe way requires formalizing something like Monad
>> but with either incompatible kinds or types (I forget which was the
>> bigger problem). Either way, it seems as though this would require a
>> new type or class similar to Monad (let's call it Monadish for this
>> discussion). Once we have that defined I imagine us lifting IO into
>> that new monadish. Now the inelegance of this solution rears it's
>> ugly head. We make very heavy use of the do-notation and we'd have to
>> revert all our monad code to use the monad primitives.
>>
>> We *might* be able to make heavy use of GHC specific hacks to take
>> over the do-notation but I'm not sure. And as I understand it you
>> can't use both means of do-notation in the same module. This has the
>> implication that we'd need to make new Monadish instances for the
>> places that we use do-notation currently, such as Maybe and Either.
>>
>> >> hunk ./src/Darcs/Repository/Internal.lhs 632
>> >> remove_from_unrevert_context repository ps
>> >> debugMessage "Removing changes from tentative inventory..."
>> >> if format_has HashedInventory rf
>> >> - then do HashedRepo.remove_from_tentative_inventory repository opts ps
>> >> + -- I believe this call to HashedRepo.remove_from_tentative_inventory is safe
>> >> + -- Because the above call to remove_from_unrevert_context ensures that
>> >> + -- none of the patches in pending depend on ps.
>> >> + then do HashedRepo.remove_from_tentative_inventory repository opts (unsafeCoerceP ps :: FL (Named p) C(x t))
>> >> when (up == UpdatePristine) $
>> >> HashedRepo.apply_to_tentative_pristine c opts $
>> >> progressFL "Applying inverse to pristine" $ invert ps
>> >
>> > The comment here is completely wrong. The call to
>> > remove_from_unrevert_context has no effect on pending, and no effect
>> > on the repository itself. Fortunately, fixing the bug in the type of
>> > this function removes the need for the unsafeCoerceP.
>>
>> Ah right, I forgot to revise that comment after realizing that Pending
>> != Tentative.
>>
>> Changing the type to t would still be the wrong thing though. As t is
>> not a well-defined context. The reason I made it r is because we
>> don't have tr. Also, tr would be equal to r until we do our first
>> tentative operation, which is probably quite problematic to explain to
>> the type checker also.
>>
>> >
>> >> hunk ./src/Darcs/Repository/Internal.lhs 642
>> >> -tentativelyReplacePatches :: forall p C(r u t). RepoPatch p => Repository p C(r u t) -> [DarcsFlag]
>> >> - -> FL (Named p) C(r t) -> IO ()
>> >> -tentativelyReplacePatches repository opts ps =
>> >> +tentativelyReplacePatches :: forall p C(r u t x). RepoPatch p => Repository p C(r u t) -> [DarcsFlag]
>> >> + -> FL (Named p) C(x r) -> IO ()
>> >> +tentativelyReplacePatches repository@(Repo x y z w) opts ps =
>> >> + -- tentativelyRemovePatches_ leaves the repository in state C(x u t)
>> >> do tentativelyRemovePatches_ DontUpdatePristine repository opts ps
>> >
>> > Again, this is vague, given that t and r are identical, but the
>> > correct answer is clearly t (because this calls
>> > tentativelyRemovePatches_).
>>
>> If we were tracking tr an tu, the first step would result:
>> C(r u tr tu) -> C(r u x tu)
>>
>> So, I disagree. Again, I took the liberty of ignoring t and using r
>> (for the reasons above).
>>
>> >
>> >> hunk ./src/Darcs/Repository/Internal.lhs 647
>> >> - sequence_ $ mapAdd repository ps
>> >> + -- Now we add the patches back so that the repo again has state C(r u t)
>> >> + sequence_ $ mapAdd ((Repo x y z w) :: Repository p C(x u t)) ps
>> >> where mapAdd :: Repository p C(i l m) -> FL (Named p) C(i j) -> [IO ()]
>> >> mapAdd _ NilFL = []
>> >> mapAdd r@(Repo dir df rf dr) (a:>:as) =
>> >
>> > Again, same issue here, that we can't write safe code that changes the
>> > repository, and thus must use unsafe hacks.
>>
>> Yup :)
>>
>> >> hunk ./src/Darcs/Repository/Internal.lhs 718
>> >> -patchSetToPatches :: RepoPatch p => PatchSet p C(x) -> FL (Named p) C(() x)
>> >> +patchSetToPatches :: RepoPatch p => RL (RL (PatchInfoAnd p)) C(x y) -> FL (Named p) C(x y)
>> >> patchSetToPatches patchSet = mapFL_FL hopefully $ reverseRL $ concatRL patchSet
>> >
>> > Fine.
>> >
>> >> hunk ./src/Darcs/Repository/Internal.lhs 783
>> >> remove_from_unrevert_context :: forall p C(r u t x). RepoPatch p
>> >> - => Repository p C(r u t) -> FL (Named p) C(x t) -> IO ()
>> >> + => Repository p C(r u t) -> FL (Named p) C(x r) -> IO ()
>> >
>> > Same issue. This function is only called once, and that single call
>> > was wrong.
>>
>> Again, pick your poison.
>>
>> >> remove_from_unrevert_context repository ps = do
>> >> Sealed bundle <- unrevert_patch_bundle `catchall` (return $ seal (NilRL:<:NilRL))
>> >> remove_from_unrevert_context_ bundle
>> >> hunk ./src/Darcs/Repository/Internal.lhs 806
>> >> debugMessage "Adjusting the context of the unrevert changes..."
>> >> ref <- readTentativeRepo repository
>> >> case get_common_and_uncommon (bundle, ref) of
>> >> + -- This case means that the pending state has no changes which are
>> >> + -- unique to the tentative state.
>> >> + -- This means that as far as the unrevert state is concerned, r = t.
>> >> + -- This is why we have the unsafeCoerceP below.
>> >> (common,(h_us:<:NilRL):<:NilRL :\/: NilRL:<:NilRL) ->
>> >> hunk ./src/Darcs/Repository/Internal.lhs 811
>> >> - case commuteRL (reverseFL ps :> hopefully h_us) of
>> >> + case commuteRL (reverseFL ps :> hopefully (unsafeCoerceP h_us :: (PatchInfoAnd p) C(r x))) of
>> >> Nothing -> unrevert_impossible unrevert_loc
>> >> Just (us' :> _) -> do
>> >> s <- slurp_recorded repository
>> >
>> > This comment is wrong, and the code is buggy as written--if you count
>> > the type witness as part of the code. A simple fix would be to
>> > replace readTentativeRepo with read_repo and to remove the
>> > unsafeCoerceP, but that would be a regression--reducing the code
>> > functionality to match what the type witnesses are capable of.
>>
>> It's true the comment is wrong. I forgot to update that as my
>> understanding changed.
>>
>> > A more interesting and correct fix would be to switch argument back to
>> > type 't' instead of 'r' and fix the calling code to also respect that
>> > type. But the 't' type really is useless in the current code, since
>> > the type witnesses don't support any scenario in which the two types
>> > are different.
>>
>> Yeah, t is wrong.
>>
>> > I'm pushing a change fixing these type witnesses... I guess it's
>> > basically just a revert of most of this patch, but it involved a
>> > careful review.
>>
>> Okay, but I wish you hadn't :( If we're going to stop ignoring t and
>> really fix it we need to add tr and tu. Of course, that change
>> doesn't solve the problem that you want to solve. Adding those types
>> without the mutation tracking means the burden of proof is still on
>> the programmer.
>
> What's tr and tu?
I promise the explanation of tr and tu is in my email :) Maybe you
need to start from the top and reread. Might be jumbled in with other
stuff.
>> I hope you can appreciate that from my point of view your reverts are
>> equally wrong to my changes. But, at least with my changes I was able
>> to add documentation at the call sites which tried to explain or give
>> a proof as to why the type witnesses didn't match the usage. In my
>> opinion, without the state tracking, the context of Repository is just
>> machine checkable documentation. meaning, it's not a proof, but a
>> guide and way to understand the code.
>
> I understand that, but your changes are wrong with respect to the
> code, and that's worse. We may as well make Repository.Internal
> right, since we can't make the commands right.
I disagree that your changes are any more correct.
> And the truth is that the tentative state *does* exist, and we
> *should* document it, and we should document it correctly. Certain
> functions (e.g. those I changed back) can be run after a previous
> function has changed the tentative state, and this needs to be
> documented. Alas, we have no tracking of changes of the tentative
> state, but that just means that we gain nothing by converting all the
> commands to use type witnesses. It doesn't mean that we can't gain
> anything in converting Repository--when we convert Repository, we gain
> documentation, and I want it to be correct.
Near as I can tell, tentative state t is not well-defined but tr and
tu exist and are well-defined.
Jason
More information about the darcs-users
mailing list