[Haskell-cafe] Documenting the impossible

[Thomas M. DuBuisson]

I think when Andy made HPC he added a way to mark code unreachable so it
wouldn't "harm" your test coverage report.


On Sat, 2008-06-14 at 19:58 +0100, Andrew Coppin wrote:
> I have a small idea. I'm curios if anybody else thinks it's a good idea...
> 
> How about a {-# IMPOSSIBLE #-} pragma that documents the fact that a 
> particular point in the program *should* be unreachable?
> 
> For example, you look up a key in a Map. You know the key is there, 
> because you just put it there yourself two seconds ago. But, 
> theoretically, lookup returns a Maybe x so - theoretically - it's 
> possible it might return Nothing. No matter what you do, GHC will insert 
> code to check whether we have Just x or Nothing, and in the Nothing case 
> throw an exception.
> 
> Obviously there is no way in hell this code path can ever be executed. 
> At least, assuming your code isn't broken... This is where the pragma 
> comes in. The idea is that you write something like
> 
>   case lookup k m of
>     Just v -> process v
>     Nothing -> {-# IMPOSSIBLE "lookup in step 3" #-}
> 
> When compiled without optimisations, the pragma just causes an exception 
> to be thrown, rather like "error" does. When compiled with 
> optimisations, the whole case alternative is removed, and no code is 
> generated for it. (And if the impossible somehow happens... behaviour is 
> undefined.) So you test your program with your code compiled 
> unoptimised, and when you're "sure" the impossible can't happen, you 
> tell the compiler to remove the check for it. (Actually, it would 
> possibly be a good idea to have a switch to turn this on and off 
> seperately if needed...)
> 
> Does anybody think this is a useful idea? If so I'll add a feature 
> request ticket to the GHC Trac. But I want to see if folks like the idea 
> first...
> 
> (I was thinking the message in the pragma would be what gets displayed 
> on screen, along with some auto-generated location info. Just a module 
> name and line number ought to be sufficient...)
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 197 bytes
Desc: This is a digitally signed message part
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20080614/3ff4acbd/attachment.bin