On Sun, 2009-03-15 at 23:18 +0100, Daniel Fischer wrote:
Am Sonntag, 15. März 2009 22:20 schrieb Jonathan Cast:
There is *no* guarantee that main0 prints 0, while main1 prints 1, as claimed. The compiler is in fact free to produce either output given either program, at its option. Since the two programs do in fact have exactly the same set of possible implementations, they *are* equivalent. So the ordering in fact *doesn't* matter.
Hum. Whether the programme prints 0 or 1 depends on whether "writeIORef r 1" is done before "readIORef r". That depends of course on the semantics of IO and unsafeInterleaveIO.
In so far as the compiler is free to choose there, it can indeed produce either result with either programme. But I think "Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order." (report, section 7) restricts the freedom considerably.
Why not read that line as prohibiting concurrency (forkIO) as well?
However, I understand "unsafeInterleaveIO allows IO computation to be deferred lazily. When passed a value of type IO a, the IO will only be performed when the value of the a is demanded."
Where is this taken from? If GHC's library docs try to imply that the programmer can predict when an unsafeInterleaveIO'd operation takes place --- well, then they shouldn't. I'm starting to suspect that not starting from a proper denotational theory of IO was a major mistake for GHC's IO system (which Haskell 1.3 in part adopted).
as explicitly allowing the programmer to say "do it if and when the result is needed, not before".
Haskell's order of evaluation is undefined, so this doesn't really allow the programmer to constrain when the effects are performed much.
So I think main0 *must* print 0, because the ordering of the statements puts the reading of the IORef before the result of the unsafeInterleaveIOed action may be needed, so an implementation is obliged to read it before writing to it.
In main1 however, v may be needed to decide what action's result x is bound to, before the reading of the IORef in the written order, so if f is strict, the unsafeInterleaveIOed action must be performed before the IORef is read and the programme must print 1,
Although as Ryan pointed out, the compiler may decide to omit the case statement entirely, if it can statically prove that f v is undefined.
but if f is lazy, v is not needed for that decision, so by the documentation, the unsafeInterleaveIOed action will not be performed, and the programme prints 0.
jcc