Excellent. Applied! Let us know if you need any help. wouter:
I found a really minor bug in the "new" function in StackSet.hs. I've attached a patch to fix it.
More interesting, however, is how I found this. I've been transcribing XMonad's StackSets to the functional language/proof assistant Coq. I've set up a darcs repository with my work so far:
darcs get www.cs.nott.ac.uk/~wss/repos/StackSet
At the moment I have a fairly complete implementation of StackSets in Coq. I have to admit that I did cut a few corners here and there, but there's nothing that can't be fixed with a bit more work. From this Coq file, you can (in principle) extract Haskell code that is pretty close to the current StackSet.hs.
I should emphasize that I haven't proven much about StackSets just yet. This only shows that the definitions in StackSet.hs can be made total (i.e. non-crashing and terminating) in a richer type theory. It should be fun to prove some QuickCheck properties in Coq – which is what I'd like to do next.
Wouter
_______________________________________________ xmonad mailing list xmonad@haskell.org http://www.haskell.org/mailman/listinfo/xmonad