preemptive vs cooperative: attempt at formalization

[Simon Marlow]

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
WHNF(*).

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.

Cheers,
	Simon

(*) if print is an IO primitive, that is.  In practice it probably
evaluates to "hPutStr stdout (show ones)".