[Haskell] -allow-extension-for-bottom

[Nils Anders Danielsson]

On Mon, 11 Oct 2004, Serge D. Mechveliani wrote:

> Consider the compilation flag  -allow-extension-for-bottom
>
> which changes the language meaning so that allows to ignore
> the bottom value. For example, the programs
>
>    (1)   (\ x -> (if p x then  foo (g x)  else  foo (h x)) )
> and
>    (2)   (\ x -> foo ((if p x then  g x  else  h x)) )
>
> become equivalent, and many program transformations become
> possible.

You may be interested in knowing that, under some circumstances, the
"feature" you are looking for is actually implemented, and you don't need
any flag to activate it. Try this function under GHC 6.2.1, for example:

> f = \x -> if x then (\y -> 0) else (\y -> 1)

*Main ChasingBottoms> isBottom (f bottom)
False

(Using your notation p = g = h = id, foo = const.)

I prefer to call this a bug, though. See
  http://www.haskell.org/pipermail/glasgow-haskell-bugs/2003-November/003735.html
and possibly
  http://www.cs.chalmers.se/~nad/software/ChasingBottoms/docs/index.html
for more details.

I should add that I think that the Haskell semantics makes proofs of
correctness overly complicated. A conservative approximation should
suffice in most cases. Hence there could also be a compiler setting which
took advantage of such approximations.

/NAD