[xmonad] StackSet patch

[Wouter Swierstra]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: stackset.patch
Type: application/octet-stream
Size: 6307 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/xmonad/attachments/20090504/263c0519/stackset.obj
-------------- next part --------------