"Simon Marlow" <[EMAIL PROTECTED]> 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?
[ Hmm, maybe you would want to say that there _are_ WHNFs inside the
value of "print ones", we just can't see them. Abstractly, there is
reduction going on like:
print ones
==> putChar '1' >> print ones
==> putChar '1' >> putChar '1' >> print ones
==> putChar '1' >> putChar '1' >> putChar '1' >> print ones
and each of those sequenced putChar actions is like a WHNF that is
being consumed by the RTS driver.
]
> > This infinite computation produces an infinite output.
>
> Depends entirely on whether putStrLn yields at regular intervals while
> it is evaluating its argument. If we are to allow cooperative
> scheduling, then the spec needs to say whether it does or not (and
> similarly for any IO operation you want to implicitly yield).
Indeed, I was assuming that I/O implied a yield, but this assumption
should definitely be made explicit. I propose that a cooperative
scheduler ought to yield at all primitive I/O actions, where primitive
means things like hPutChar, or takeMVar, which are implemented at a
lower level than Haskell.
> You seem to be assuming more about cooperative scheduling than eg.
> Hugs provides. I can easily write a thread that starves the rest of
> the system without using any _|_s. eg.
>
> let loop = do x <- readIORef r; writeIORef r (x+1); loop in loop
I wasn't originally aware that Hugs scheduler only yields on MVar
operations. That seems too restrictive. I believe the "all I/O
primitives" rule would guarantee progress in the absence of _|_.
Unless you can think of another counter-example?
Regards,
Malcolm
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
