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

[Jason Dagit]

On Mon, Mar 17, 2008 at 8:45 AM, David Roundy <droundy at darcs.net> wrote:

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


I'


>
>
> > 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
> _______________________________________________
> darcs-devel mailing list
> darcs-devel at darcs.net
> http://lists.osuosl.org/mailman/listinfo/darcs-devel
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.osuosl.org/pipermail/darcs-devel/attachments/20080317/a238327a/attachment.htm