[Haskell-cafe] Proof that Haskell is RT

[Derek Elkins]

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.
> But you're still in the IO monad at this point so I suppose it
> technically "doesn't count" because it's only observable as the result
> of IO.
> 
> It's pretty suspect behaviour, but not actually a failure of
> referential transparency.

Indeed.  There's a difference between purity and referential
transparency.  A lack of purity is when behaviour, as in semantics,
depends on evaluation order (modulo bottom of course).  Referential
transparency is being able to substitute equals for equals.  These
notions are related but independent.

Examples of failures of referential transparency that aren't failures of
purity are easy to find.  A simple one would be some kind of
introspection feature, such as various forms of quotation, being able to
ask for the name of a variable, being able to serialize functions.  So
purity doesn't imply referential transparency.

Failures of purity that aren't failures of referential transparency are
a bit trickier since without purity (i.e. evaluation order independence)
what constitutes a valid substitution may vary.  Still, as an easy
start, a language with no binding forms is trivially referentially
transparent regardless of how impure it may be.  If you use a
call-by-name evaluation order, the full beta rule holds and evaluation
proceeds by substituting equals for equals and therefore such a language
is also referentially transparent.  So referential transparency doesn't
imply purity.