On Mon, 2009-03-16 at 00:14 +0100, Daniel Fischer wrote:
Am Sonntag, 15. März 2009 23:30 schrieb Jonathan Cast:
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?
Good question. Because forkIO is a way to explicitly say one doesn't want the one thing necessarily done before the other, I'd say.
As is unsafeInterleaveIO. (And as is unsafePerformIO, as per the docs:
If the I/O computation wrapped in unsafePerformIO performs side effects, then the relative order in which those side effects take place (relative to the main I/O trunk, or other calls to unsafePerformIO) is indeterminate.
)
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
From the documentation of System.IO.Unsafe.
This version of those docs: http://haskell.org/ghc/docs/latest/html/libraries/base/System-IO-Unsafe.html leaves unsafeInterleaveIO completely un-documented. So I'm still not sure what you're quoting from.
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).
Maybe.
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.
The full paragraph from the report:
" The I/O monad used by Haskell mediates between the values natural to a functional language and the actions that characterize I/O operations and imperative programming in general. The order of evaluation of expressions in Haskell is constrained only by data dependencies; an implementation has a great deal of freedom in choosing this order. Actions, however, must be ordered in a well-defined manner for program execution -- and I/O in particular -- to be meaningful. 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."
I read it as saying that IO *does* allow the programmer to control when the effects are performed.
Right. But by using forkIO or unsafeInterleaveIO you waive that ability.
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.
I suppose that's a typo and should be "unneeded". But can it prove that f v is unneeded? After all, it may influence whether 0 or 1 is printed.
[Ignored: begging the question] jcc