[Haskell] Definitions of purity and Lazy IO

[Dan Doel]

On Thursday 05 March 2009 11:48:33 pm Jonathan Cast wrote:
> > That is, for any program context C[] such that C[f1] is well-typed,
> > the program C[f2] must too be well-typed, and if one can observe the
> > result of C[f1] and of C[f2], the two observations must be identical.
>
> Every time?  For every context?  What about the context
>
>   do
>      x <- getStdRandom random
>      y <- getStdRandom random
>      print $ [] x y
>
> ?  By the standard above, f1 is not even observationally equivalent to
> *itself*.

One could theoretically dismiss this by saying that any particular IO context 
contains some random seed that determines the results of generating the random 
numbers. So, when you run the program and get different results, that's due to 
your actually running it in different contexts (with different seeds).

However, it's possible to get this sort of non-determinism in other ways. For 
instance, consider the following fragment:

  do ctr <- newMVar 0
     let inc = do i <- takeMVar ctr ; putMVar ctr (i+1) ; return i
     v1 <- newEmptyMVar
     v2 <- newEmptyMVar
     forkIO $ do inc >>= putMVar v1
     forkIO $ do inc >>= putMVar v2
     i1 <- takeMVar v1
     i2 <- takeMVar v2
     print $ i1 - i2

If forkIO provides real concurrency, this fragment should be capable of 
displaying either -1 or 1 (of course, everything happens too fast here, so I 
always end up getting -1, but I think the point is sound). So it's another 
context where (-) isn't equivalent to itself.

So, to fix this up in the same way as the random example, you have to add 
something to the context that will supposedly completely determine the 
scheduling order of the threads in the program, so that when threads run in a 
different order, and you get a different result, you can say that you ran the 
program in a different context. But once we start doing that, how much more 
contrived is it to say that each context has some hidden state that determines 
how effects are interleaved with unsafeInterleaveIO such that we see the 
results we do (even though we know that isn't what's going on operationally; 
it isn't what's going on operationally with concurrency, either).

The real issue is that lazy IO sometimes leads people to write buggier 
programs than they otherwise might. The same is true of, say, head and tail, 
but they are not impure by Sabry's definition, nor do they break referential 
transparency. They're 'impure' in that they're partial functions, but I'm not 
sure everyone's ready for Haskell to become a total language yet. :)

Cheers,
-- Dan