[Haskell-cafe] What unsafeInterleaveIO is unsafe

[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?

> 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