See http://doi.acm.org/10.1145/301631.301637
and http://dx.doi.org/10.1016/S1571-0661(05)80288-9 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? 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. 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
-- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:[EMAIL PROTECTED] _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
