[Haskell] Definitions of purity and Lazy IO

[Duncan Coutts]

On Thu, 2009-03-05 at 20:11 -0800, oleg at 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