[Haskell-cafe] What unsafeInterleaveIO is unsafe

[Jonathan Cast]

On Mon, 2009-03-16 at 01:04 +0100, Daniel Fischer wrote:
> Am Montag, 16. März 2009 00:47 schrieb Jonathan Cast:
> > On Mon, 2009-03-16 at 00:14 +0100, Daniel Fischer wrote:
> >
> > > > > 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.htm
> >l
> >
> > leaves unsafeInterleaveIO completely un-documented.  So I'm still not
> > sure what you're quoting from.
> 
> The documentation haddock-0.9 built when I compiled ghc-6.8.3 last year.

So it's a GHC (and base) major version out of date.

> > > > 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.
> 
> That depends on the specification of unsafeInterleaveIO. If it is "unspecified 
> order of evaluation", then yes, if it is "do when needed, not before",

Note that `when needed' is still dependent on the (still unspecified)
(non-IO) Haskell evaluation order.  Also note that, to demonstrate any
strong claims about unsafeInterleaveIO, you need to show that the
compiler *must* perform in such-and-such a way, not simply that it
*will* or that it *may*.

> as my 
> local documentation can be interpreted, then unsafeInterleaveIO reduces that 
> ability, but doesn't completely remove it.

Sure.  The question is whether the compiler has still enough options for
re-ordering the program that transforming a program according to the
standard equational axiomatic semantics for Haskell doesn't change the
set of options the compiler has for the behavior of its generated code.

jcc