2009/3/6 <[email protected]>: > > 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 _______________________________________________ Haskell mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell
