[Haskell] Definitions of purity and Lazy IO
minh thu
noteed at gmail.com
Fri Mar 6 03:29:23 EST 2009
2009/3/6 <oleg at okmij.org>:
>
> As Amr Sabry aptly observed more than a decade ago discussions of
> purity and referential transparency usually lead to confusion and
> disagreement. His JFP paper provided the needed rigor and argued that
> Haskell even _with regular file (stream) IO_ is pure. As was shown
> yesterday, with Lazy IO, Haskell is not pure.
>
> Before we discuss definitions, let us note the motivations. Suppose I
> have a Haskell program. As every single (compiled) Haskell program it
> has the main function, of the type IO a for some a. It must use IO, at
> least to print the final result, the observation of the
> program. Suppose the program contains the expression "e1 + e2" adding
> two integer expressions. Can I replace this expression with "e2 + e1"
> and be sure the observations of my program are unaffected?
>
> If one says that ``you should assume that every IO operation returns a
> random result'' then we have no ability to reason about any
> real Haskell program. We can't be sure of soundness of any compiler
> optimization. So, Haskell is far worse than C!? With C, Xavier Leroy
> has managed to create a provably correct optimizing compiler, and
> mechanically _prove_ the soundness of all optimizations. A C program,
> just like a Haskell program, must use IO at least to print the
> final result. We can never hope to build a provably correct compiler for
> Haskell? We cannot prove observational equivalences of any real
> Haskell program? Isn't that sad?
>
> The formal question is thus: are the following two expressions f1 and f2,
> of a *pure type* Int->Int->Int
>
> f1, f2:: Int -> Int -> Int
> f1 = \e1 e2 -> case (e1,e2) of
> (1,_) -> e1 - e2
> (_,_) -> e1 - e2
>
> f2 = \e1 e2 -> case (e1,e2) of
> (_,1) -> e1 - e2
> (_,_) -> e1 - e2
>
> equal? 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.
> [...]
Thanks for clarifying, I see how I was wrong yesterday. I was to quick at
pointing the use of IO instead of observing that the pure functions f1 and f2
have themself an effect.
Thu
More information about the Haskell
mailing list