On Sun, Dec 17, 2006 at 10:22:15AM +0000, Ganesh Sittampalam wrote: > On Sat, 16 Dec 2006, David Roundy wrote: > >Pending handling is definitely the place where I'm most thoroughly > >wishing for the GADT type witnesses to verify correctness. > > Now that both the "old" and "new" GHCs support them, would it be feasible > to switch?
Yeah, I think so. The catch is that it's a big job, and I'm not sure when I'll have the time, and of the two big jobs I'd like to do, conflicts win out (and the hashed inventories, which I hope will be relevant to the conflicts code). I was just this morning wondering how best to implement the pending handling with GADTs. It's actually tempting to rebind (>>=) and use a modified monadic notation, which would actually be a monad with type guarantees. I'm thinking something like: class WitnessMonad wm where (>>=) :: wm w w' a -> (a -> wm w' w'' b) -> wm w w'' b (>>) :: wm w w' a -> wm w' w'' b -> wm w w'' b return :: a -> wm w w' a fail :: String -> wm w w' a which obviously just adds a couple of phantom types indicating the monad state prior to and after each operation. I actually rather like this redefined monad, as it seems like it'd be useful in lots of places (e.g. a restricted IO monad that disallows use of a file handle after it's closed). Then we'd define a repository-modification monad which would have a witness type like (recordedstate,unrecordedstate). Then our functions would not only document their behavior, but would also enforce proper usage: addToPending :: Patch p p' -> RepoMonad (rec,p) (rec,p') () addPatchToRecorded :: Patch r r' -> RepoMonad (r,p) (r',p) () I'm not sure that these are right, but the good news would be that adding the GADT interface would force us to quantify these questions, and document them in the code itself for future developers, and would even check that we didn't make this sort of mistake. The trouble is that all the core patch code would need to be rewritten. I have a feeling this is either a job for a hackathon, or for a lot of work by one person. Probably the latter, since there are "interesting" design issues to be worked out, regarding the proper use of unsafeCoerce#. It actually may be possible to convert just the highest-level repository manipulation code to use GADT type witnesses without converting all of patch logic. If we just wrapped type witnesses around get_repo and the Repository functions, we might be able to make that interface typesafe without mucking with the code below. Not that we don't want to fix the code below, but I'm thinking in terms of an intermediate state. We'd also need to mess with get_common_and_uncommon, and maybe a few more, but it might be doable. I'll think. Because I'd *really* love to have the type checker help me with the correctness of pending code, it's just been broken *way* too often! -- David Roundy Department of Physics Oregon State University _______________________________________________ darcs-devel mailing list [email protected] http://www.abridgegame.org/cgi-bin/mailman/listinfo/darcs-devel
