foldl (+) 0 [1..10000000] :: Integer *** Exception: stack overflow foldl' (+) 0 [1..10000000] :: Integer 50000005000000
I thought both of these were perfectly well defined in denotational semantics (and equal to 50000005000000). The first is merely a failure of one person's computer to implement the (perfectly well-defined) denotational semantics of the program. If we are going to document the officially valid deficiencies of each compiler and machine architecture, perhaps that should not be in the *language* definition, but in the Haskell Platform users' guide. And those who are trying to distinguish between terminating and nonterminating bottom are claiming to solve the Halting Problem. There is no general way to reliably distinguish these two, and I believe that valid program transformations exist that can convert one to the other. Bottom has only one value, not two. Otherwise bottom would have been called buttocks. Dan Malcolm Wallace wrote:
Yet I think it would be valid to say that seq can turn a non-terminating (exceptioning) program into a terminating one. Do you have an example of that?
Sure. foldl (+) 0 [1..10000000] :: Integer *** Exception: stack overflow foldl' (+) 0 [1..10000000] :: Integer 50000005000000
The only difference between foldl and foldl' is strictness (the use of seq). By "non-terminating (exceptioning)" I of course really meant "terminating with bottom" as opposed to "terminating with a defined value", but since non-termination and exceptions are semantically both bottom, you won't mind that slip. :-)
Regards, Malcolm
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime