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

[Jason Dagit]

If it helps to see some of the possibilities and their type errors check
this page:
http://hpaste.org/6316

I'm annotating it with some of the different things I have tried and their
type errors.  Maybe this will help step you through the difficulties I've
had with getting read_repo_private to work.

Thanks,
Jason

On Wed, Mar 12, 2008 at 3:30 PM, Jason Dagit <dagit at codersbase.com> wrote:

>
>
> 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/9331d31f/attachment.htm