RE: preemptive vs cooperative: attempt at formalization

On 13 April 2006 11:41, Malcolm Wallace wrote:

"Simon Marlow" 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)".