Re: [Haskell-cafe] Proof that Haskell is RT

On Wed, 2008-11-12 at 22:16 +0000, David MacIver wrote:

On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson wrote:

...

Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.

Really? It seems easy to create things with it which when passed to ostensibly pure functions yield different results depending on their evaluation order:

module Main where

import System.IO.Unsafe import Data.IORef

main = do w1 <- weirdTuple print w1 w2 <- weirdTuple print $ swap w2

swap (x, y) = (y, x)

weirdTuple :: IO (Int, Int) weirdTuple = do it <- newIORef 1 x <- unsafeInterleaveIO $ readIORef it y <- unsafeInterleaveIO $ do writeIORef it 2 >> return 1 return (x, y)

david@mel:~$ ./Unsafe (1,1) (1,2)

So show isn't acting in a referentially transparent way: If the second part of the tuple were evaluated before the first part it would give a different answer (as swapping demonstrates).

It seems that this argument depends on being able to find a case where w1 and swap w1 actually behave differently. weirdTuple is non-deterministic, but that's fine, since it's in the IO monad. And w1 and w2 are simply two (distinct!) lambda-bound variables; there is no requirement that two different lambda-bound variables behave in the same fashion, regardless of how values may be expected to be supplied for them at run time (what values the functions in question may be expected to be applied to) unless the function(s) they are formal parameters of are (both) applied to the same expression. (>>=) certainly does not count as `application' for present purposes. Even if it is insisted (why? I don't think GHC actually guarantees to produce the above result when main is executed) that main must always yield the above result, it does not follow that unsafePerformIO is non-RT; it is still only non-causal. But referential transparency doesn't require that the result of an IO action must depend only on events that transpire by the time it finishes running; it places, in fact, no requirement on the run-time behavior of any IO action at all. It requires only that equal expressions be substitutable for equals; and, again, w1 and w2 being the result of calling a single IO action with no dependence on the outside world does not require them to be equal, under any system of semantics. So, no violation of RT. jcc