[darcs-users] darcs patch: Make Darcs.Repository.Internal compile w... (and 1 more)
Jason Dagit
dagit at codersbase.com
Sat Aug 9 02:47:44 UTC 2008
On Fri, Aug 8, 2008 at 5:45 PM, David Roundy <droundy at darcs.net> wrote:
> On Thu, Aug 07, 2008 at 08:01:32PM -0700, Jason Dagit wrote:
> > David,
> >
> > I have more type witnesses coming up, but I'm finally done screwing up
> and
> > fixing Darcs.Repository.Internal so I thought I'd send it your way for a
> > review :)
> >
> > Jason
> >
> > Thu Aug 7 18:53:43 PDT 2008 Jason Dagit <dagit at codersbase.com>
> > * Make Darcs.Repository.Internal compile with type witnesses.
> >
> > Thu Aug 7 19:30:25 PDT 2008 Jason Dagit <dagit at codersbase.com>
> > * fixed a bug in identity_commutes property
> > In the right identity check the patch order should have gone from
> > (identity :> p) to (p2 :> i2). I added a rigid type context too
> > so that ghc 6.8 and newer would type the definition.
>
> First off, I'd rather use fmap rather than liftM, simply because it
> requires one less import. It's not a big deal, but when writing new
> code that's my preferred approach.
Alright, I'll try to remember that.
> hunk ./src/Darcs/Patch/Ordered.lhs 244
> > +dropWhileFL :: (FORALL(x y) a C(x y) -> Bool) -> FL a C(r v) ->
> FlippedSeal (FL a) C(v)
> > +dropWhileFL _ NilFL = flipSeal NilFL
> > +dropWhileFL p xs@(x:>:xs')
> > + | p x = dropWhileFL p xs'
> > + | otherwise = flipSeal xs
> > +
> > +dropWhileRL :: (FORALL(x y) a C(x y) -> Bool) -> RL a C(r v) -> Sealed
> (RL a C(r))
> > +dropWhileRL _ NilRL = seal NilRL
> > +dropWhileRL p xs@(x:<:xs')
> > + | p x = dropWhileRL p xs'
> > + | otherwise = seal xs
>
> I wonder about these. It seems like they're functions that we're
> better off not using. I see that dropWhileRL is never used, and
> dropWhileFL is used precisely once. Maybe we're better off not
> defining a general function? The problem is that it's a lossy one, so
> it seems like one that we'd not use in (most?) good code.
The final version of my patch didn't use dropWhileFL, but since there was a
locally defined dropWhileRL, I thought it would be best to define it with
the rest of the general purpose forward and backward list functions. I can
move it back to a where clause though.
As for being lossy, I don't follow why that makes it a bad function or how
to avoid needing it from time to time. It seems like one of the useful
points of the Seal types is that we can use them to safely, albeit lossily,
implement many of the startard idioms and combinators.
>
>
> > +consFLSealed :: a C(x y) -> Sealed (FL a C(y)) -> Sealed (FL a C(x))
> > +consFLSealed a (Sealed as) = seal $ a :>: as
> > +
> > +consRLSealed :: a C(y z) -> FlippedSeal (RL a) C(y) -> FlippedSeal (RL
> a) C(z)
> > +consRLSealed a (FlippedSeal as) = flipSeal $ a :<: as
>
> These two don't seem to be used at all... and I suspect that reducing
> the number of functions we define is more beneficial that providing
> every possibly-useful helper.
I don't think consFLSealed made the final cut so I can kill that one, but
I'm definitely using consRLSealed, once in Darcs/Match.lhs and once in
Darcs/Repository.lhs. I'm not a huge fan of writing "unsealFlipped
(flipSeal . (:<:))", or at least I think that's equivalent without testing,
but I'm probably missing a (.) somewhere. So I'd like to leave that one and
not redefine it in several modules, since that seems like a waste too. I
should also add, that for some reason mapSeal doesn't seem to work as a
drop-in replacement very often, even when its function body does. I played
with the type signature of it a bit, but in the end moved on because it
seemed like a time sink. I think the problem may have been that ($) doesn't
compose with mapSeal in a type safe way.
>
> > hunk ./src/Darcs/Repository/Internal.lhs 403
> > -handle_pend_for_add :: (RepoPatch p, Effect q) => Repository p -> q ->
> IO ()
> > +handle_pend_for_add :: forall p q C(r u t x y). (RepoPatch p, Effect q)
> > + => Repository p C(r u t) -> q C(x y) -> IO ()
> > hunk ./src/Darcs/Repository/Internal.lhs 412
> > - writePatch pn $ (fromPrims newpend :: Patch)
> > - where rmpend :: FL Prim C(x y) -> FL Prim C(x z) -> Sealed (FL Prim)
> C(y)
> > + writePatch pn $ fromPrims_ newpend
> > + where rmpend :: FL Prim C(a b) -> FL Prim C(a c) -> Sealed (FL Prim
> C(b))
> > hunk ./src/Darcs/Repository/Internal.lhs 419
> > + fromPrims_ :: FL Prim C(a b) -> Patch C(a b)
> > + fromPrims_ = fromPrims
> > hunk ./src/Darcs/Repository/Internal.lhs 439
> > -tentativelyMergePatches :: RepoPatch p => Repository p -> String ->
> [DarcsFlag]
> > - -> FL (PatchInfoAnd p) -> FL (PatchInfoAnd p) ->
> IO (FL Prim)
> > +
> > +tentativelyMergePatches :: RepoPatch p
> > + => Repository p C(r u t) -> String ->
> [DarcsFlag]
> > + -> FL (PatchInfoAnd p) C(u r) -> FL
> (PatchInfoAnd p) C(u y)
> > + -> IO (Sealed (FL Prim C(u)))
> > hunk ./src/Darcs/Repository/Internal.lhs 446
> > -considerMergeToWorking :: RepoPatch p => Repository p -> String ->
> [DarcsFlag]
> > - -> FL (PatchInfoAnd p) -> FL (PatchInfoAnd p) ->
> IO (FL Prim)
> > +considerMergeToWorking :: RepoPatch p
> > + => Repository p C(r u t) -> String -> [DarcsFlag]
> > + -> FL (PatchInfoAnd p) C(u r) -> FL (PatchInfoAnd
> p) C(u y)
> > + -> IO (Sealed (FL Prim C(u)))
> > hunk ./src/Darcs/Repository/Internal.lhs 454
> > -tentativelyMergePatches_ :: RepoPatch p => MakeChanges
> > - -> Repository p -> String -> [DarcsFlag]
> > - -> FL (PatchInfoAnd p) -> FL (PatchInfoAnd p)
> -> IO (FL Prim)
> > +tentativelyMergePatches_ :: forall p C(r u t y). RepoPatch p
> > + => MakeChanges
> > + -> Repository p C(r u t) -> String ->
> [DarcsFlag]
> > + -> FL (PatchInfoAnd p) C(u r) -> FL
> (PatchInfoAnd p) C(u y)
> > + -> IO (Sealed (FL Prim C(u)))
> > hunk ./src/Darcs/Repository/Internal.lhs 462
> > - pc = case merge (progressFL "Merging them" them :\/: progressFL
> "Merging us" us) of
> > - _ :/\: x -> x
> > + Sealed pc <- case merge (progressFL "Merging them" them :\/:
> progressFL "Merging us" us) of
> > + _ :/\: x -> return $ seal x
>
> We could cut a line and a case statement here by writing
>
> _ :/\: x <- return (merge (progressFL "Merging them" them :\/: progressFL
> "Merging us" us))
>
> oh, but that runs into the ghc bug that Simon PJ doesn't consider a
> bug, right? :(
The do-notation seems to desugar to a rigid type context so I haven't had
any wobbly type problems there. It's usually when there are nested case
expressions involving GADTs that I have problems. Here I was just focused
on translating the code and not shortening it, but now that you mentioned
it I cleaned it up to one line and it compiles and type checks no problem.
>
> > -tentativelyAddPatch :: RepoPatch p => Repository p -> [DarcsFlag] ->
> PatchInfoAnd p -> IO ()
> > +tentativelyAddPatch :: RepoPatch p
> > + => Repository p C(r u t) -> [DarcsFlag] ->
> PatchInfoAnd p C(x y) -> IO ()
>
> This type looks wrong to me. How can we add a patch which has an
> unknown relationship to our repository?
>
> > hunk ./src/Darcs/Repository/Internal.lhs 561
> > -applyToTentativePristine :: (Effect q, Patchy q) => Repository p -> q ->
> IO ()
> > +applyToTentativePristine :: (Effect q, Patchy q) => Repository p C(r u
> t) -> q C(x y) -> IO ()
>
> Similarly here...
I'm not really sure what the difference is between tentative, pending,
pristine and tentative pristine, tentative pending, etc. I was hoping you
could comment on this, but I forgot to ask.
It seems like in Repository p C(r u t), that maybe the pending/tentative
state is t, and the pristine state is r? I'll make that assumption for now
and see what type checks. Take for example:
setTentativePending :: forall p C(r u t x y). RepoPatch p => Repository p
C(r u t) -> FL Prim C(x y) -> IO ()
Am I updating the pending or the tentative state or some hybrid?
>
> > hunk ./src/Darcs/Repository/Internal.lhs 607
> > -tentativelyRemovePatches :: RepoPatch p => Repository p -> [DarcsFlag]
> > - -> FL (Named p) -> IO ()
> > +tentativelyRemovePatches :: RepoPatch p => Repository p C(r u t) ->
> [DarcsFlag]
> > + -> FL (Named p) C(x t) -> IO ()
>
> Note that in contrast, this looks okay.
>
> Mostly it looks good, and most of my comments were the sorts of code
> cleanup thing that I wouldn't insist on. But I'd really like to see
> whether we could extend the type checking to these functions
> (tentativelyAddPatch, applyToWorking, applyToTentativePristine and
> others), and to have a more careful search for similar issues. Any
> time we've got a function in Repository or Internal that accepts a
> Repository and some sort of patch type, one of the contexts of the
> patch had better match one of the contexts in the repository, or we'd
> better have a very good reason (indicated in a comment) why not.
>
> As it is, these functions only typecheck because HashedRepo and
> DarcsRepo are themselves do not export a safe API. Which is all
> right, but Repository really needs to export a safe API if we're going
> to make any significant claims about the safety gained by compiling
> the entire code with type witnesses enabled.
Okay, although I'm limited by own understanding and what I can infer from
reading the code. I could use a crash course on the terminology used in
these modules.
Thanks. I'm working a new patch to address some of this.
Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.osuosl.org/pipermail/darcs-users/attachments/20080808/35a8ccc6/attachment-0001.html
More information about the darcs-users
mailing list