[Haskell-cafe] What unsafeInterleaveIO is unsafe

[Jonathan Cast]

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