
13 Feb
2009
13 Feb
'09
2:20 p.m.
Joseph Garvin wrote:
I recall reading at some point an article or blog post that discussed how XMonad leveraged the type system to guarantee that X errors couldn't occur. But no matter how much googling I do now I can't find it; I musn't be using the right search terms. Anyone know where it is?
The type system can't guarantee that xmonad produces no X errors, since it relies on the ffi and secondly, matching types don't imply correctness, especially when dealing with IO-ish stuff. I think you might be referring to this article by Neil Mitchell(author of Hoogle and Catch, iirc) that proves for an old xmonad that the core won't fail due to error-calls or failed pattern matches: http://neilmitchell.blogspot.com/2007/05/does-xmonad-crash.html