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

[Jonathan Cast]

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. 
> This is on dodgy ground, IMO: either you admit that the IO monad contains 
> an Oracle, or you admit it can time-travel.   I don't believe in either of 
> those things :-)

That's the charm of denotational semantics --- you're outside the laws
of physics.

jcc