On Wed, 2007-12-05 at 10:01 +0100, Pablo Nogueira wrote:
Hasn't Ryan raised an interesting point, though?
Bottom is used to denote non-termination and run-time errors. Are they the same thing?
Up to observational equality, yes.
To me, they're not. A non-terminating program has different behaviour from a failing program.
When it comes to strictness, the concept is defined in a particular semantic context, typically an applicative structure:
[[ f x ]] = App [[f]] [[x]]
Function f is strict if App [[f]] _|_ = _|_
Yet, that definition is pinned down in a semantics where what _|_ models is clearly defined.
I don't see why one could not provide a more detailed semantics where certain kinds of run-time errors are distinguished from bottom.
When there is reason to, that is exactly what is done. The domain grows from 1+V to 1+V+E. However, when run-time errors can be observed you start having to provide answers to undesirable questions: what is the behavior of error "foo" + error "bar"? Another person has pointed you to the imprecise exceptions paper that gives one well thought out answer for this in the context of Haskell.
Actually, this already happens. Type systems are there to capture many program properties statically. Some properties that can't be captured statically are captured dynamically: the compiler introduces run-time tests. Checking for non-termination is undecidable, but putting run-time checks for certain errors is not. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe