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.h... 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