On Tue, Dec 04, 2007 at 03:07:01PM -0800, Ryan Ingram wrote:
Is there a reason why strictness is defined as
f _|_ = _|_
instead of, for example,
forall x :: Exception. f (throw x) = throw x where an exception thrown from pure code is observable in IO.
In the second case we need to prove that the argument is evaluated at some point, which is also equivalent to the halting problem but more captures the notion of "f evaluates its argument" rather than "either f evaluates its argument, or f _ is _|_"
I suppose the first case allows us to do more eager evaluation; but are there a lot of cases where that matters?
"Is there a reason why 2 + 2 is defined as 4 instead of, for example, 5?" Strictness is more useful in practice, simpler to define, and easier to approximate. What benefit does your notion offer? Stefan