[Haskell-cafe] Why is this strict in its arguments?

[Janis Voigtlaender]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 

-- 
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt at tcs.inf.tu-dresden.de