[Haskell-cafe] Why is this strict in its arguments?
derek.a.elkins at gmail.com
Wed Dec 5 18:15:18 EST 2007
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 at haskell.org
More information about the Haskell-Cafe