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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe