[Haskell] -allow-extension-for-bottom
Nils Anders Danielsson
nad at cs.chalmers.se
Tue Oct 12 04:12:14 EDT 2004
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
More information about the Glasgow-haskell-users
mailing list