[darcs-users] darcs patch: Add Repository IO monad, RIO. (and 31 more)

[Jason Dagit]

On Thu, Sep 4, 2008 at 3:19 AM, Eric Y. Kow <eric.kow at gmail.com> wrote:
> So, I've had a look at the first few patches and have little to add
> except a few annotations on pre-existing darcs code or stuff that Jason
> and David have already agreed on.
>
>> I constructed this set of patches by pulling over my previous patches,
>> unrecording them, fixing up conflicts, checking that they compile with/without
>> type witnesses and every several files checking that the tests still pass.
>
> I realise that this is a pretty massive pain in the rear, but I think
> not only will this make David and other reviewers' job easier, it's also
> the kind of thing that future-Jason will thank you for when he's poring
> over ChangeLogs and trying to figure something out :-)
>
> Being in deep must-get-job-done territory, I can understand that caring
> about future-Jason is hard to do.  I guess I can't do much else here but
> wish you great courage!
>
> Add Repository IO monad, RIO.
> -----------------------------
> So David has already reviewed this, but I glanced at it anyway out of
> curiosity and desire to some day get past the
> write-your-first-monad-tutorial part of my Haskell education.
>
> For other people in my shoes, the RIO monad does one thing and one
> thing only
>
>  (>>>=) ::       RIO p C(r u t  t1) a
>         -> (a -> RIO p C(r u t1 t2) b)
>         -> RIO p C(r u t t2) b
>
> Given an RIO action X followed by the RIO action Y, the monad enforces a
> simple constraint, namely that the tentative recorded state after X s
> same as the one before Y.  Of course, we're just dealing with type
> witnesses here, so these states do not actually have any concrete
> representation in reality.  They're just little markers we jot down for
> compile-time verification of our expectations.  If our little markers
> fail to unify the way we think they should, then we know we're in
> trouble!

This is an excellent way to phrase it.  Because it compiles with type
witnesses does not mean it does what we want.  Also, just because it
doesn't compile with typenesses it's not automatically incorrect.
But, it is safe to say that when the type witnesses fail to unify that
something is wrong.  Sometimes it's just that the encoding we use
isn't powerful enough but most often it means the programmer is
specifying something that is fundamentally wrong.

>> +-- | Repository IO monad.  This monad-like datatype is responsible for
>> +-- sequencing IO actions that modify the tentative recorded state of
>> +-- the repository.
>> +newtype RIO p C(r u t t1) a = RIO {
>> +        unsafeUnRIO :: Repository p C(r u t) -> IO a -- ^ converts @RIO a@ to @IO a at .
>
> I generally like it when 'unsafe' functions tell me in what sense they
> are unsafe.  Here I guess it's because we stop tracking type witnesses.

Personally, I don't see it as a terribly unsafe thing.  It's really a
lossy transformation.  We had some type information, then we 'used it
up' to convert to IO.  To improve the haddock we could say,

-- ^ Unsafe in the sense that we give up type witnesses to convert
from @RIO a@ to @IO a at .

>> +-- | This corresponds to @>>@ from the Monad class.
>> +(>>>) :: RIO p C(r u t t1) a -> RIO p C(r u t1 t2) b -> RIO p C(r u t t2) b
>> +a >>> b = a >>>= (const b)
>
> I wonder if we need to toss it one of those infixr thingies to avoid
> having to write these parentheses.  I guess whatever makes this behave
> like >> would be good

Good catch.  I'll do that.

> Begin using RIO
> ---------------
> In the spirit of one thing at a time, this patch lays down the
> infrastructure without actually using the extra verification.
>
>> -    (map drop_dotslash . list_slurpy) `fmap` (withRepository [] slurp_pending)
>> +  withRepository [] $ do
>> +    r <- getRepository
>> +    s <- rIO $ slurp_pending r
>> +    return $ (map drop_dotslash . list_slurpy) s
>
> I wonder if something like a withRepositoryRIO could have helped us
> here, and in the rest of the code.  Oh well :-)

What is withRepositoryRIO?

>> +withGutsOf :: Repository p C(r u r) -> RIO p C(r u r t) ()
>> +           -> IO ()
>
> I'm guessing this is the focus of this patch and that the rest of it is
> just the consequences

That's a pretty good summary.

> updates to Darcs.Match to support type witness refactor of various commands
> ---------------------------------------------------------------------------
>> +    case get_patches_beyond_tag (n2pia pinfo) repo of
>
> Out of curiosity, is there any difference between pia and piap?

pia = PatchInfoAnd
piap = PatchInfoAnd "Patch"

I haven't thought about when one is used over the other and I didn't
write that code so I'm not sure I can effectively comment.

> rename get_patches_beyond_tag and add more typeful version
> ----------------------------------------------------------
>> -                      :>: reverseRL (concatRL $ unsafeUnflippedseal $ get_patches_beyond_tag chtg patches)
>> +                      :>: reverseRL (concatRL $ unsafeUnflippedseal $ get_patches_beyond_taginfo chtg patches)
>
> Hmm. Would a darcs replace not have been practical or sensible here?

It would have been prefect probably, but I don't (yet) think in terms
of replace patches.  I'll work on it.

>> -get_patches_beyond_tag :: RepoPatch p => PatchInfo -> PatchSet p C(x) -> FlippedSeal (RL (RL (PatchInfoAnd p))) C(x)
>> -get_patches_beyond_tag t ((hp:<:NilRL):<:_) | info hp == t = flipSeal $ NilRL :<: NilRL
>> +get_patches_beyond_tag :: RepoPatch p => (PatchInfoAnd p) C(x y) -> PatchSet p C(z) -> (RL (RL (PatchInfoAnd p))) C(y z)
>> +get_patches_beyond_tag t ((hp:<:NilRL):<:_) | IsEq <- sloppyIdentity t
>> +                                            , IsEq <- sloppyIdentity hp
>> +                                            , info hp == info t = unsafeCoerceP $ NilRL :<: NilRL
>
> No comments on Jason's code itself.  I'm guessing it does exactly the
> same thing but without hiding quite so many types.

That is my intent.  Hopefully David will spot anything I missed.  As
far as I can tell the code is right and so are the witnesses, but
extra eyes are always helpful.

>> + prepend :: (PatchInfoAnd p) C(a z) -> (RL (RL (PatchInfoAnd p))) C(y a) -> (RL (RL (PatchInfoAnd p))) C(y z)
>> + prepend pp NilRL = (pp:<:NilRL) :<: NilRL
>> + prepend pp (p:<:ps') = (pp:<:p) :<: ps'
>
> Again a comment on darcs and not on Jason's code.  I wonder if there is
> something more efficient than (p `prepend` next) that we ought to be
> doing here.

It's good to be looking out for changes like that.  In my type
witnesses refactorings I'm avoiding rewriting things.  Once we have
extensive type witness usage refactoring will be safer and we can
tackle things like this more confidently.

As David commented, I'm not sure how we could do this one more
efficiently.  Here we just have a pattern patch and then we construct
a new list with lots of sharing with the old list.  GHC should be
optimize this into some pretty simple code I hope.

Thanks for the feedback,
Jason