[darcs-devel] darcs patch: start gadt stuff (and 1 more)

Eric Y. Kow eric.kow at gmail.com
Sun Jun 3 13:37:28 PDT 2007


Well, I've had a look and it does seem to be good stuff (nice proactive
use of the type system to catch potential errors).

On the other hand, there are some compile errors which GHC 6.6.  Is this
code meant to work with a more recent GHC?  The 6.6.1 release notes
don't suggest any major GADTy changes... Just checking.  It doesn't hurt
when you don't set the configure flag, so I could push it in.  Will sit
on it until next week though.

Sorry David, I'm not advanced enough of a Haskeller to review this code
properly, so my comments are not going to be of much help.

Remarks for the interested
--------------------------
[again with lots of potential for errors]

The basic idea is to use witness types to add more safety to the darcs
patch code.  Right now, we have a lot of code that manipulates two
patch sequences, for instance:
   commute :: (Patch, Patch) -> Perhaps (Patch, Patch)

Here the commute function takes a two patch sequence (p1,p2) and perhaps
returns another sequence (p2,p1).  So we might use the code like this:
   (b2,a2) <- commute (a,b)

This is what darcs patch code looks like up to now.  It's ok, but it
turns out that there's a lot more safety to be had.  For example,
consider, this larger, made up example,

commute3 :: (Patch, (Patch, Patch)) -> Perhaps (Patch, (Patch, Patch))
commute3 (a,(b,c)) = -- a b c <-> b2 a2 c <-> b2 c2 a3
 do (b2,a2) <- commute (a,b)
    (c2,a3) <- commute (a2,c)
    return (b2,(c2,a3))

What's to prevent us from accidentally switching around one of our patch
sequences?  For example, we could just as easily write that first line as
 do (a2,b2) <- commute (a,b)

Such mistakes would not be noticed by the type checker.  With tuples, we
think of all Patch pairs as being interchangeable.  We can do better!
The job of a patch is to transform some input context (the repository
has a file foo with the contents 'xx') into an output context (the
file's contents are 'yy).  So why don't we exploit this extra little bit
of knowledge to make our code a little safer?  The idea is that
sequences of patches should have contexts that fit together.
Schematically:
   xx P1 yy P2 zz

The key here is that the code doesn't really have to know what these
contexts are, just that they are different for each patch.  Just knowing
this let's us trap errors like saying
   xx P1 zz P2 yy
if somewhere along the line we mention offhand that
   (xx P1 yy) and (yy P2 zz)

David's code basically replaces the tuples with something a little more
informative.  Instead of writing (bland, uninformative) tuples like
 (b2, a2) <- commute (a,b)

We write something more like
 (b2 :> a2) <- commute (a :> b)

The difference is that the :> type (and its friends) carry around
contextual information in the types.  Not actual contexts, mind you,
just little annotations which let the type system to sanity check our
code.

Let's see an application of this with the commute3 example above.
First we rewrite it with the extra context information

commute3 :: (Patch ww xx :> (Patch xx yy :> Patch yy zz))
         -> Perhaps (Patch ww :> yy (Patch yy zz :> Patch zz xx))
commute3 (a,(b,c)) = -- a b c <-> b2 a2 c <-> b2 c2 a3
 do (b2 :> a2) <- commute (a  :> b)
    (c2 :> a3) <- commute (a2 :> c)
    return (b2 :> (c2 :> a3))

And now what happens if we switch something around?
 do (a2 :> b2) <- commute (a  :> b) -- wrong!
    (c2 :> a3) <- commute (a2 :> c)
    return (b2 :> (c2 :> a3))

The type checker notices that we contradicted ourselves and it
complains... which is good. The grouchier our type checker, the happier
we are.

Further reading
---------------
The following docs might also be helpful:

* David's FOSDEM 2006 talk
    http://darcs.net/fosdem_talk/talk.pdf
* Haskell wikibook on GADT
    http://en.wikibooks.org/wiki/Haskell/GADT

This is if you are trying to read the code...

* what unsafeCoerce# does (just magically turns type a to b)
    http://www.haskell.org/ghc/docs/latest/html/libraries/base/GHC-Prim.html#v%3AunsafeCoerce%23
* infix type constructors
    http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#infix-tycons

General notes for David
------------------------
I'm guessing this is a work in progress which you're not even expecting
to compile with --with-type-witnesses enabled.  For example,
unsafeCompare is not implemented yet (which had me scratching my head
for a while :-) )

I get this error if I ./configure --with-type-witnesses
src/Darcs/Patch/Core.lhs:68:11:
    Type found where type variable expected

I found that adding parentheses helped (and made it easier for me to
understand the code:
  data (a1 :> a2) C(x,y) where
    (:>) :: a1 C(a,b) -> a2 C(b,c) -> (a1 :> a2) C(a,c)

... assuming that's what you meant, of course.

I assume you're going to need to add something like
    data Patch C(a,b)

But I'm a bit confused about how... For example, what do you do with
    | Split [Patch]
?

Not too urgent, but it would be nice if you could submit a patch
fixing Darcs.Patch.Test.  Otherwise, I can't run make slowtest,
even without the configure test.

> +#define FORALL(a,b) forall a b.

Is there still a use for this, or is it subsumed by the GADT stuff?

Otherwise, I've had a look at the rest of the code, and it seems ok.

-- 
Eric Kow                     http://www.loria.fr/~kow
PGP Key ID: 08AC04F9         Merci de corriger mon français.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 186 bytes
Desc: not available
Url : http://lists.osuosl.org/pipermail/darcs-devel/attachments/20070603/eeacd892/attachment.pgp


More information about the darcs-devel mailing list