On Thu, 2009-03-05 at 20:11 -0800, o...@okmij.org wrote: > > Before one invokes an equational theory or says that both these > expressions are just integer subtraction, let me clarify the > question: are f1 and f2 at least weakly observationally equivalent? > 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. The > observation of a program may (and often does) involve side-effects and > IO (more on it below). The message posted yesterday exhibited a > context C[] that distinguishes f1 from f2. Thus, in presence of Lazy > IO, any equational theory that equates f1 and f2 cannot be sound. I > don't think one can design such a context C[] using the regular, eager > file IO.
I'm not sure that observational equivalence on IO computations the right approach. For example it means we cannot explain imprecise exceptions. http://research.microsoft.com/en-us/um/people/simonpj/papers/imprecise-exn.htm With imprecise exceptions we define the meaning of a value that could return one of a number of exceptions to actually return the whole set (see Sections 3.4, 3.5 and 4 above). But on any particular run the representative member of that set of exceptions can be different. They give the example: do v1 <- getException ((1/0) + error "Urk") v2 <- getException ((1/0) + error "Urk") return (v1 == v2) The solution is that getException makes a non-deterministic choice each time. I expect that unsafeInterleaveIO can be explained in a similar way, via non-determinism in the choice of interleaving of events. Any final observations correspond to some particular interleaving, we just do not know which one it is going to be until we inspect the value. The semantics is that it can be any of them. Different runs of the program, different compiler transformations or evaluation orders can change which values we typically observe without breaking the semantics that it could be any of the possible values. This is somewhat stronger than the semantics of a random number generator in IO because not all interleavings are possible and some interleavings of effects do not interfere with each other. > Thus Haskell even with IO may be called pure functional. With Lazy IO, > it can no longer be called pure functional as different orders of > evaluation of arguments of a function lead to different program > observations. The same is true of imprecise exceptions and yet we do not seem to be worried about them destroying purity. Duncan _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell