[darcs-devel] darcs patch: add context to HashedRepo.copy_repo (and 2 more)

[Jason Dagit]

On Wed, Mar 12, 2008 at 6:48 AM, David Roundy <droundy at darcs.net> wrote:

> On Tue, Mar 11, 2008 at 02:27:18PM -0700, Jason Dagit wrote:
> > On Tue, Mar 11, 2008 at 1:07 PM, David Roundy <droundy at darcs.net> wrote:
> > > The problem is that you expose a constructor for Context, and you
> > > unseal the output from createHashed and friends (I believe).  Which is
> > > effectively equivalent to simply unsealing the output of createHashed
> > > and friends.
> >
> > If I just unseal createHashed and friends then I end up with existential
> > types which are not equal to any other type.  To then put the freshly
> > created patches into a sequence I would have to unsafeCoerceP them.
>  This
> > use of unsafeCoerceP seemed unconstrained and susceptible to misuse.
>
> I don't think you should ever need an unsafeCoerceP just to read patches
> into a sequence using createHashed.  That's why a sealed patch has only
> one
> of its two contexts sealed.
>
> Oh, I see the trouble:  it's that you want to constrain the final state.


I'm not sure what you mean.  This isn't about the difference of read_repo
and  read_tenative_repo.  It's about getting enough context to parse,
read_patches, rp and createHashed so that the resulting patches can be
placed into a sequence.


> This is an inherently unsafe operation, so it makes sense to use
> unsafeCoerceP.  Why not just use it, rather than making the patch reading
> itself unsafe?


I guess I misunderstood the unsafeCoerceP.  I thought that would make things
more unsafe by using it a lot inside of read_repo_private where I am reading
patches.  Perhaps I have the wrong impression, but I thought I would be
making things worse by using it here and making patch reading unsafe.  I
don't fully understand how the Context approach is actually worse than just
applying the unsafeCoercePs.


> The existing unsafeCoerceP's in read_repo and
> read_tentative_repo are in exactly the place where we need an unsafe
> operation.  What is wrong with this? It *is* unsafe, and needs to be
> unsafe, and it's at the exact bit of code where we know that this unsafe
> operation needs to be performed.  I like that a lot more than sprinkling
> the unsafe operations all over the place.


I haven't modified read_repo or read_tentative_repo.  They both still
contain an unsafeCoerceP and I have no plans to change that.  My Context
trick doesn't apply to them or address them at all.

Were there more unsafeCoerceP's that you needed to add? I'm really feeling
> doubtful that this Context approach is the way to go.  You can't remove
> the
> use of unsafe operations from HashedRepo, because that is where high-level
> invariant properties of repositories are defined.


There are 4 more unsafeCoercePs that would have been needed in
read_repo_private.  That's what I've been trying to explain by talking about
parse, createHashed, read_patches and rp.  If you look at the code prior to
this patch bundle you'll see a few things.  Currently read_patches and rp
try to allow an existentially quantified type variable to escape (it may
help to see the exact compiler message yourself, this is easy to reproduce,
look at the patch bundle I sent in that uses unsafeCoerceP instead of
Context for details).

Or in other words, when we unseal the result of createHashed (even if we put
it into a sequence as we unseal it), the type checker complains that the
previously sealed phantom type is going to escape this context.  That gives
us 4 places in read_repo_private that requires an unsafeCoerceP.

My objection to adding these is that without considering that whole function
(which is quite large) and understanding it very carefully, I cannot tell
that those unsafeCoercePs are valid.  Granted, I've done that work already
to some extent to figure out that it doesn't type check, why it doesn't type
check and possible ways to fix it.  So in some sense, I could probably add
those unsafeCoercePs into the core of that function, but then would others
trying to maintain the code know they are valid?  I know that many of these
functions are marginally dangerous already.  I was trying to be creative and
do something safer than just sprinkling in unsafeCoerceP.  It seems to me
that since we assume the inventory is stored correctly that we should be
able to use that assumption here to read in a valid patch sequence.


> > The only way I could think of to eliminate this was to pass more context
> > information to those functions.  As I said before, it seemed best to do
> > this incrementally instead of completely changing the PatchInfo type.
> > For the Context type to be useful at all I need a way to assign context
> > to objects and conversely a way to remove it again.  Even if I hide the
> > constructor of Context I still have to expose:
> > unsafeContext :: a -> Context a C(x y)
> > unsafeUncontext :: Context a C(x y) -> a
>
> But unsafeUncontext is actually safe, only unsafeContext is unsafe.  Thus
> by hiding the constructor we're able to distinguish between safe and
> unsafe
> uses.


Okay, I can rename unsafeUncontext to just unContext.

No, there's no guarantee that Context just manipulates phantom types.
> unsafeContext can create concrete types, so you could write (this is
> pseudocode):


I'm still not convinced that unsafeContext can allow us manipulate
non-phantom types in an unsafe way.  For example, wrapping the identity
function in a Context gives, Context id :: Context (a -> a) x y (I tested
this in ghci).  Then as soon as you unwrap it to use the identity function
the phantom types are gone and you can't play with them anymore.  If you've
seen something about this in the literature I'd be happy to go learn about
it.  I don't think my arguments about type theory are sophisticated enough
to come up with the necessary proofs unassisted to demonstrate the safety or
unsafety here.

unsafeCoerce# :: a -> b
> unsafeCoerce# x = fromJust $ do let myid = identity
>                                    h = unsafeContext (hash myid)
>                                    p = createHashed h (parse $ showPatch
> myid)
>                                IsEq <- sloppy_identity p
>                                return x
>
> and you've got an inplementation of unsafeCoerce# (which never returns
> Nothing).


If I'm understanding your pseudo code correctly, (and I pulled the type for
`hash` out of the source), I get something like the following.  I'm assuming
that identity is of the type that hash takes, but represents an identity
patch.  Maybe that's not what you meant?

Maybe you meant for it to work like this (ignoring IO):
h :: Context Int32 C(x y) -- x and y are arbitrary, we know x == y, but the
type checker doesn't
p :: ReadPatch p => Hopefully p C(x y)

I can see how this would then match for the pattern "IsEq <- sloppy_identity
p", since p was created from the string representing the identity patch.  I
fail to see how the overall type could be "a -> b".  We do all of that work
and then return x, which we already stated to have type 'a'.  Or am I
missing something?

I'm attempting to implement this, and I have this defined inside of
read_repo_private:
          _myCoerce :: a -> b
          _myCoerce x = fromJust $
            do let h = unsafeContext ""
                   s = unsafeContext idpatchinfo
                   p = (unsafePerformIO $ createHashed h (parse $ s))
                   pai = idpatchinfo `patchInfoAndPatch` p :: PatchInfoAnd
Prim C(x y)
               IsEq <- return $ sloppyIdentity pai
               return x

The _ is just there to stifle warnings about not using myCoerce and I'm
using idpatchinfo defined in Darcs.Patch.Info.  Also for h I just use the
empty string since I'm really only interested in getting this to type check.

You'll notice I changed it a fair but, but all my changes are just there to
get it as close to compiling as possible.  I even threw in an
unsafePerformIO and the type checker tells me that a and b do not unify.  So
it seems that it would still behave as the identity function even though it
may be a bit unsafe internally.  Perhaps I'm taking the formal parameter 'x'
too literally here?  You did say it was pseudo code, but my version has this
error:
src/Darcs/Repository/HashedRepo.lhs:214:24:
    Couldn't match expected type `b' (a rigid variable)
           against inferred type `a' (a rigid variable)
      `b' is bound by the type signature for `_myCoerce'
        at src/Darcs/Repository/HashedRepo.lhs:213:28
      `a' is bound by the type signature for `_myCoerce'
        at src/Darcs/Repository/HashedRepo.lhs:213:23

My only complaint with the above code is that the type checker doesn't force
me to prove that h and s have the same context.  I tested this by replacing
x with undefined.  That is quite unfortunate (and in my mind makes this
Context business pointless here and something I didn't realize as a problem
until now).  I basically want something that works like "PatchInfoAnd" since
I have PatchInfos and the raw strings of the patches which I will parse
later when I actually need them.  Perhaps saying that I want something like
PatchInfoAnd makes it more clear what I want?  Maybe you disagree with my
creation of the Context type but you see how something analogous to
PatchInfoAnd, such as PatchInfoAndRawPatchString is useful here?  Maybe:
data PatchInfoAndRawPatchString C(a b) = PIARPS !PatchInfo String {- what to
put here? -} C(a b)

Do you think putting something in the structure to hold the context is a
better approach?  At some point it did occur to me that PatchInfos really
shouldn't have a context so modifying PatchInfo to hold the context seems
like the wrong thing to do.  My reasoning is that when you commute patches
the PatchInfos don't change.  Because of this I believe PatchInfoAnd is
implemented correctly and I want something like it, but instead of
associating a patch and it's context with the PatchInfo I want to associate
an unparsed patch (the raw patch string) and the context that it will have
once we parse it.  Does that make sense?  I think doing this would allow us
to remove some unsafeCoercePs from read_repo_private.  Everything should
work essentially like it does with the Context type but the context would be
part of the PatchInfoAndRawPatchString type instead of the phantom wrapper
that is Context.

Thanks,
Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.osuosl.org/pipermail/darcs-devel/attachments/20080312/7da17a31/attachment-0001.htm