[Haskell-cafe] Documenting the impossible

[Don Stewart]

andrewcoppin:
> 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" #-}

You could try using an 'assert' , which has the property of being
compiled out at higher optimisation levels. And you can use 'error' or
'undefined' for undefined behaviour.

    http://www.haskell.org/ghc/docs/latest/html/users_guide/assertions.html

Not very Haskelly though.

-- Don