[Haskell-cafe] Proof that Haskell is RT

[Dan Doel]

On Wednesday 12 November 2008 6:18:38 pm David MacIver wrote:
> To put it a different way, in the absence of unsafeInterleaveIO the IO
> monad has the property that if f and g are observably equal up to
> termination then x >>= f and x >>= g are equivalent in the IO monad
> (actually this may not be true due to exception handling. Our three
> main weapons...). In the presence of unsafeInterleaveIO this property
> is lost even though referential transparency is retained.

I'm not sure what exactly you mean by this, but, for instance:

    randomIO >>= (print :: Int -> IO ())

obviously isn't going to give the same results as:

    randomIO >>= (print :: Int -> IO ())

every time. Your weirdTuple is semantically similar, in that it selects 
between returning (1,1) and (2,1), but instead of being random, it 
operationally selects depending on how you subsequently evaluate the value. 
That may not seem like the same thing, because you know what's going on, but 
formally, I imagine you can treat it all as a black box where either "this 
time it gave (2,1)" or "this time it gave (1,1)", and what you see is always 
consistent. The fact that it sort of uses an oracle to see what will happen in 
its future is just The Power of IO (it does have a sort of "spooky action" 
feel to it). :)

-- Dan