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 _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell