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

[David Roundy]

On Wed, Mar 12, 2008 at 03:30:50PM -0700, Jason Dagit wrote:
> On Wed, Mar 12, 2008 at 6:48 AM, David Roundy <droundy at darcs.net> wrote:
> > 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.

As you will see in my previous email (responding to your later email), we
can implement read_repo_private without any unsafeCoerceP.

> > 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.

I agree that read_repo_private should be implemented (and implementable) safely.

> > 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

no, x /= y, and we know that.  x == a, and y == b.

> 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?

IsEq proves that type x and type y are the same, but since x is a and y is
b, we've proven that type a and b are the same.  Thus we're able to return
our input of type a as if it were type b!

> 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

I think we may need to add some type signatured and scoped types to the
above code to make it work (but I still haven't tested this)

_myCoerce :: forall a b. a -> b
_myCoerce = do let h = unsafeContext "" :: Context String a b

Actually, probably all you need to do is to change your pai to be of type
PatchInfoAnd Prim C(a b).  (and add the forall, to get lexical type
scoping)
-- 
David Roundy
Department of Physics
Oregon State University