On Sat, Nov 8, 2008 at 4:26 PM, Eric Kow <[EMAIL PROTECTED]> 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 _______________________________________________ darcs-users mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-users
