[Haskell-cafe] Proof that Haskell is RT

[Jonathan Cast]

On Wed, 2008-11-12 at 23:18 +0000, David MacIver wrote:
> On Wed, Nov 12, 2008 at 11:05 PM, Jonathan Cast
> <jonathanccast at fastmail.fm> wrote:
> > 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.
> 
> That's not really better. :-)

I never said it was.

jcc