[Haskell-cafe] Proof that Haskell is RT

[Jonathan Cast]

On Wed, 2008-11-12 at 22:16 +0000, David MacIver wrote:
> On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
> <lennart at augustsson.net> 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 at 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