-allow-extension-for-bottom
Dear Haskell implementors, 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. I suspect that after compiling and running of a program under -allow-extension-for-bottom the user will discover many helpful information about the original program. For example, under -allow-extension-for-bottom it may run 1000 times faster, and then, the user finds out what to change to have a 1000 times speed-up for the original program for the standard Haskell. Thus, in my particular practical example, it is evident to me that it is better to specify (2). But many similar effects are hard to find out without compiling under -allow-extension-for-bottom. Maybe, the compiler could issue the warnings like, say, "Consider factoring `if' in ... This may improve ... " ? Copy, please, the answer to mechvel@botik.ru, ----------------- Serge Mechveliani mechvel@botik.ru
Dear Haskell implementors,
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.
Is it not the case that with -allow-extension-for-bottom all programs are equivalent to error "Finished" and hence not just 1000 times faster but infinitely faster (asymptotically)? Seriously, I can see that something like this might be of interest, but the details are not trivial. For a start, you'd want to allow refinements only - from _|_ to non-_|_ - rather than in both directions, to disallow the above transformation. But then you'd have to deal with refinement relations rather than equivalences everywhere in the theory, losing symmetry and making things more complicated. --KW 8-)
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
participants (3)
-
Keith Wansbrough -
Nils Anders Danielsson -
Serge D. Mechveliani