[Haskell-cafe] Re: [Haskell] Lazy IO breaks purity

[Duncan Coutts]

On Thu, 2009-03-05 at 13:08 +0000, Simon Marlow wrote:
> Lennart Augustsson wrote:
> > I don't see any breaking of referential transparence in your code.
> > Every time you do an IO operation the result is basically
> > non-deterministic since you are talking to the outside world.
> > You're assuming the IO has some kind of semantics that Haskell makes
> > no promises about.
> > 
> > I'm not saying that this isn't a problem, because it is.
> > But it doesn't break referential transparency, it just makes the
> > semantics of IO even more complicated.
> > 
> > (I don't have a formal proof that unsafeInterleaveIO cannot break RT,
> > but I've not seen an example where it does yet.)
> 
> So the argument is something like: we can think of the result of a call to 
> unsafeInterleaveIO as having been chosen at the time we called 
> unsafeInterleaveIO, rather than when its result is actually evaluated.

But surely that is the mistake. With IO, bound values depend solely on
the effects that happened previously (no time travel). With ordinary
sequential IO, that's easy to understand and explain because the binding
and the effects happen at the same time/place.

The extension to unsafeInterleaveIO is not to pretend that the value is
chosen at the point it is bound. The value depends on the effects not
the binding. The extension is that we separate the binding point and the
effects. The effects can be arbitrarily interleaved with other effects.
The value we get does potentially depend on all those prior effects.

The arbitrary interleaving of effects is obviously weaker than them
happening now, in sequence, before the next action. This works well when
the deferred side effect do not interfere with other side effects and is
non-deterministic when they do interfere, as in Oleg's example. It
doesn't break referential transparency though, thanks to memoisation we
only observe one final value.

The standard libs, being sensible, mostly only use unsafeInterleaveIO in
the cases where we expect little interference. Note how Oleg has to go
out of his way to construct the example, circumventing the semi-closed
Handle state which was designed to stop people from shooting themselves
in the foot.

There used to be a real example where unsafeInterleaveIO did break
referential transparency. That was due to concurrency and lack of
locking.
http://hackage.haskell.org/trac/ghc/ticket/986
When the bug was around there was a *single* pure value that if used by
two different threads could be observed to be different. There's nothing
similar happening here.

Duncan