[Haskell-cafe] Proof that Haskell is RT

[Jonathan Cast]

On Wed, 2008-11-12 at 23:02 +0000, David MacIver wrote:
> On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart <dons at galois.com> wrote:
> > david.maciver:
> >> 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).
> >
> > Mmmm? No. Where's the pure function that's now producing different
> > results?  I only see IO actions at play, which are operating on the
> > state of the world.
> 
> I suppose so. The point is that you have a pure function (show) and
> the results of evaluating it totally depend on its evaluation order.

Sure.  But only because the argument to it depends on its evaluation
order, as well.

jcc