[PRL] referential transparency

[Dave Herman]

>>So Scheme is not r.t. because you can't replace the following
>>expression....
> 
> Right.

I wish Matthias were around, because I remember several months ago he 
was protesting the claim that Haskell is r.t. and Scheme isn't, claiming 
(I think) that they didn't have a proper definition for r.t. I wonder 
what he had in mind.

> If you can treat your program as a functional transducer then you can
> treat your input as a lazy sequence of values.  Since each term in the
> sequence never changes, you can freely substitute the value of the
> term wherever a reference to the term appears *provided* that you
> continue to enforce the constraint that a term is never `forced' until
> the one immediately preceeding it has been forced.

Okay, so here's a simple example:

-- BEGIN PROGRAM

test :: Int -> IO Bool
test = \i -> do c <- hGetChar stdin
                 return ((c == 'q') && (i < 10))

main :: IO ()
do b <- test 5
    if b then (putStrLn "foo") else (putStrLn "bar")

-- END PROGRAM

The definition of `test' looks like it's not r.t., because given the 
same integer, it might give a different boolean answer based on what it 
reads from stdin. However, since it translates to a "world transformer," 
it's got a functional definition. Here's an unfolding of the definitions:

-- BEGIN COMPILATION

hGetChar :: Handle -> World -> (World, Char)
test :: Int -> World -> (World, Bool)
main :: World -> (World, ())

test = \i -> bind (hGetChar stdin)
                   \c -> return ((c == 'q') && (i < 10))
      {- def'n hGetChar, return -}
      = \i -> bind \world -> $PRIM.hGetChar world stdin
                   \c -> \world -> (world, ((c == 'q') && (i < 10)))
      {- def'n bind -}
      = \i -> \w1 -> let (w2, ch) = $PRIM.hGetChar w1 stdin
                     in (((\c -> \w3 -> (w3, ((c == 'q') && (i < 10))))
                          ch) w2)
      {- beta-substitution -}
      = \i -> \w1 -> let (w2, ch) = $PRIM.hGetChar w1 stdin
                     in (w2, ((ch == 'q') && (i < 10)))

main = bind (test 5)
             \b -> if b then (putStrLn "foo") else (putStrLn "bar")
      {- def'n bind -}
      = \w1 -> let (w2, b) = ((test 5) w1)
               in (if b then (putStrLn "foo") else (putStrLn "bar"))
      {- def'n test -}
      = \w1 -> let (w2, b) = let (w3, ch) = ($PRIM.hGetChar w1 stdin)
                             in (w3, ((ch == 'q') && (i < 10)))
                   in (if b then ($PRIM.putStrLn "foo" w2, ())
                            else ($PRIM.putStrLn "bar" w2, ()))
      {- let-rotation -}
      = \w1 -> let (w3, ch) = $PRIM.hGetChar w1 stdin
               in let (w2, b) = (w3, ((ch == 'q') && (i < 10)))
                  in (if b then ($PRIM.putStrLn "foo" w2, ())
                           else ($PRIM.putStrLn "bar" w2, ()))

-- END COMPILATION

In the end, the program translates to a world transformer where every 
subexpression can be replaced with the value it converges to, but since 
all IO-related expressions rely on the world that results from the 
previous IO-related expression, that world has to have been computed 
before we can know what that value is.

Which is all just a long-winded way of saying what Carl and Joe just said.

Dave