preemptive vs cooperative: attempt at formalization
simonmar at microsoft.com
Thu Apr 13 06:55:55 EDT 2006
On 13 April 2006 11:41, Malcolm Wallace wrote:
> "Simon Marlow" <simonmar at microsoft.com> wrote:
>>> Well, the expression "ones" on its own is non-terminating.
>> under what definition of non-termination? Non-termination has meant
>> the same as _|_ in a call-by-name semantics as far as I'm concerned,
>> and "ones" is most definitely not == _|_.
> Ok, fair enough, if we accept that "ones" is terminating, because it
> reaches a WHNF, then tell me what is the value of "print ones"? For a
> terminating computation, x, "print x" would have a real value of type
> IO (), even though that value is abstract and you cannot name it. But
> surely the value of "print ones" is _|_, because it never terminates?
"print ones" always has the value "print ones", i.e. it's already in
You could additionally give a semantics for running IO actions that
includes a concept of _|_ (see my other message), but we shouldn't
confuse this with the pure denotational semantics of Haskell.
(*) if print is an IO primitive, that is. In practice it probably
evaluates to "hPutStr stdout (show ones)".
More information about the Haskell-prime