[Haskell-cafe] Re: [Haskell] Lazy IO breaks purity
jonathanccast at fastmail.fm
Thu Mar 5 11:05:38 EST 2009
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
More information about the Haskell-Cafe