[darcs-users] darcs patch: enable type witnesses for show commands. (and 4 more)

Jason Dagit dagit at codersbase.com
Sun Nov 9 01:01:00 UTC 2008


On Sat, Nov 8, 2008 at 4:26 PM, Eric Kow <kowey at darcs.net> wrote:
> Hi David,
>
> On Fri, Nov 07, 2008 at 07:35:58 -0500, David Roundy wrote:
>> Here are some more patches I had lying around (I just amended them to
>> resolve some conflicts).  Not important stuff, just type witness cleanups.
>> At least the cutting of dead code should be accepted.
>
> Nice to see our witness coverage creeping forward.  Having realised that
> Jason has a thesis to work on and that I shouldn't be asking any patch
> review from him, I've taken a look and applied these, thanks!

I did read your email though and I thought maybe the practice of
explaining the concepts would be good for everyone :)

>
> enable type witnesses for show commands.
> ----------------------------------------
>> +     src/Darcs/Commands/Show.o \
>
> Shouldn't ShowFiles be added to this list?
>
>> -    where slurp :: RepoPatch p => Repository p -> IO Slurpy
>> +    where slurp :: RepoPatch p => Repository p C(r u r) -> IO Slurpy
>
> For the interested, the three witnesses are recorded state, unrecorded
> state and tentative state, and here our slurp function expects a
> repository whose recorded and tentative state witnesses unify... which
> if I understand correctly means you can't accidentally pass in a
> repository from a function that uses type witnesses to say "this changes
> the tentative state"
>
> cut dead code from Unrecord.
> ----------------------------
>> -rempatch :: RepoPatch p => Named p -> PatchSet p -> PatchSet p
>> -rempatch p (pps:<:ppss) =
>
> Hooray! We should maybe have some sort of automated dead-code detector
> to help us find these things

That would be nice.  I guess it requires GHC to look at the entire
project and see which things are exported but never imported.  Kind of
a tricky problem perhaps?

>
> make unrecord work with type witnesses.
> ---------------------------------------
>> +     src/Darcs/Commands/Show.o src/Darcs/Commands/Unrecord.o \
>
> Likewise, shouldn't Rollback be added to this list?
>
>> +  FlippedSeal patches <- return $ if first_match opts
>> +                                  then get_last_patches opts allpatches
>> +                                  else FlippedSeal $ concatRL allpatches
>
> It's been explained to me countless times, but I still don't fully get
> the notion of sealing.  The situation is that typically when working
> with patches, we use type witnesses to refer to two states for a patch,
> the 'before' and the 'after' state, which we can write
>   p C(before after)
>
> I vaguely understand that sealing is useful because it gives us a way
> to say 'we only know things about some of these states', where with
> Sealed things, we only know about the 'before' state, and with
> FlippedSealed things, we only know about the 'after' state.  Anyway,
> that's my very shaky take on things.

When you seal away a value you agree to lose information about it.
Once you hide the value in a seal all you know about it is that it
exists.  You could optionally add type class constraints to the data
constructor so that you know that it exists and it instances specific
type classes.  You could use this trick to create heterogenous lists
of showable things:
data ShowableThing where
  S :: Show a => a -> ShowableThing

When you then open up the seal later and try to get back the value,
the type system assigns a fresh new name for the type, or
eigenvariable.  This eigenvariable is not equal to any other type
including the original type of the value that was sealed away.  It's
completely distinct.

In our case, we seal away phantom types.  As you'll recall phantom
types are types that have no value associated with them, like this:
data P a = P

Here, 'a' is a phantom type.  This means that in darcs we actually
seal way types that have no values associated with them.  Which is a
bit odd on the surface.

We use these seals to control the way in which phantom types will
unify.  Since phantoms have no value associated with them then in
principle when you construct the value that has a phantom type you can
make the phantom unify with any type.  Ah, but if instead you seal the
phantom type then you have a way to make that phantom type distinct so
that it will not unify with arbitrary types.

Now this creates two problems:
1) An eigenvariable cannot be returned to a higher level of scope
2) Sometimes you know that two phantoms are equal but the type system
is pessimistic and says "Nope, they're eigenvariables and therefore
distinct."

To solve (1) you can seal the eigenvariable before returning the
value.  This is quite common and seems to be happening here.

It's this (2) that makes us implement things like (=\/=) and (=/\=)
that I seem to go on about :)  The thing is, you can use unsafeCoerce
to convince the type checker whenever you know two eigenvariables are
equal.  But, using unsafeCoerce everywhere is bad so we made a witness
type, EqCheck, that can act as a first class proof that two types are
equal.  First class just meaning you can pass an IsEq around and when
you examine the value it provides the proof.  So, we bundle the test
into (=\/=) and return the evidence (IsEq).

I hope that helps,
Jason


More information about the darcs-users mailing list