blackholes and exception handling
Hello, GHC can spot (some) non-terminating computations and terminate with blackhole: <<loop>> instead of running indefinitely. With exception handling one can handle such situations. The following program 'launches missiles': import Control.Exception main = do handle go_ahead don't_launch_first launch_missiles don't_launch_first = don't_launch_first go_ahead :: SomeException -> IO () go_ahead _ = putStr "go ahead, " launch_missiles = putStr "fire!" The output of this program is go ahead, fire! although, don't_launch_first is a non-terminating computation. Without black-hole detection this code would never 'launch missiles'. Is the above output intended? The idea behind black-hole detection is that one bottom is as good as another [1]. Consequently, exception handling may not distinguish between non-termination and other errors. Is the equation _|_ `catch` const a = a supposed to hold in general (for every kind of bottom)? Or is it a bug in GHC that programmers can handle black-hole errors? Sebastian [1] A semantics for imprecise exceptions http://portal.acm.org/citation.cfm?id=301637 -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
On Sun, May 02, 2010 at 12:10:23AM +0200, Sebastian Fischer wrote:
although, don't_launch_first is a non-terminating computation. Without black-hole detection this code would never 'launch missiles'.
Is the above output intended?
Yes.
go_ahead :: SomeException -> IO () go_ahead _ = putStr "go ahead, "
Note that catching all exceptions is rarely the right thing to do. See http://www.haskell.org/ghc/docs/6.12.2/html/libraries/base-4.2.0.1/Control-E... for more details.
The idea behind black-hole detection is that one bottom is as good as another [1]. Consequently, exception handling may not distinguish between non-termination and other errors.
Pure code can't distinguish, but exception handling code in IO can. Thanks Ian
Is the above output intended?
Yes.
Interesting.
Note that catching all exceptions is rarely the right thing to do. See http://www.haskell.org/ghc/docs/6.12.2/html/libraries/base-4.2.0.1/Control-E... for more details.
I should have written go_ahead :: NonTermination -> IO () in the first place.
The idea behind black-hole detection is that one bottom is as good as another [1]. Consequently, exception handling may not distinguish between non-termination and other errors.
Pure code can't distinguish, but exception handling code in IO can.
What makes me wary is that GHC distinguishes between different kinds of non-terminating computations (those it can detect as black holes and those it can't). As a consequence, the semantics of my program depends on how I define the infinite loop don't_launch_first (the program either writes to stdout or doesn't). For me, it is interesting to notice (and slightly disturbing) that this is intended and that the Control.Exception module defines the NonTermination exception to explicitly handle black holes. Thank you for clarifying! Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
On Sun, May 02, 2010 at 01:10:17PM +0200, Sebastian Fischer wrote:
What makes me wary is that GHC distinguishes between different kinds of non-terminating computations (those it can detect as black holes and those it can't). As a consequence, the semantics of my program depends on how I define the infinite loop don't_launch_first (the program either writes to stdout or doesn't).
For me, it is interesting to notice (and slightly disturbing) that this is intended and that the Control.Exception module defines the NonTermination exception to explicitly handle black holes.
If you think about it, there aren't a lot of options: (a) Don't provide a way of catching *any* kind of non-terminating computations. (b) Provide a way to catch some of them. (c) Solve the halting problem and catch'em all. =) Considering that someone who wants (a) can live with (b) or (c) just by ignoring the extra functionality, and that (c) is impossible, GHC provides (b). Cheers, -- Felipe.
On 02/05/10 12:10, Sebastian Fischer wrote:
Is the above output intended?
Yes.
Interesting.
Note that catching all exceptions is rarely the right thing to do. See http://www.haskell.org/ghc/docs/6.12.2/html/libraries/base-4.2.0.1/Control-E...
for more details.
I should have written
go_ahead :: NonTermination -> IO ()
in the first place.
The idea behind black-hole detection is that one bottom is as good as another [1]. Consequently, exception handling may not distinguish between non-termination and other errors.
Pure code can't distinguish, but exception handling code in IO can.
What makes me wary is that GHC distinguishes between different kinds of non-terminating computations (those it can detect as black holes and those it can't). As a consequence, the semantics of my program depends on how I define the infinite loop don't_launch_first (the program either writes to stdout or doesn't).
For me, it is interesting to notice (and slightly disturbing) that this is intended and that the Control.Exception module defines the NonTermination exception to explicitly handle black holes.
The imprecise exceptions paper that you referenced describes exactly this issue in some detail - see Section 4.4, the semantics of getException (which is a simpler version of catch). Basically, catch is non-deterministic, so when the value is _|_ it can make a non-deterministic choice between diverging or catching an exception. Cheers, Simon
participants (4)
-
Felipe Lessa -
Ian Lynagh -
Sebastian Fischer -
Simon Marlow