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. Amr Sabry in a paper ``What is a Purely Functional Language?'' J. Functional Programming, 8(1), 1-22, Jan. 1998. http://www.cs.indiana.edu/~sabry/papers/purelyFunctional.ps proposed the definition of purity, see p 2 and Definition 4.7. The definition essentially states that call-by-name, call-by-value and call-by-need evaluation functions must be weakly equivalent. These evaluation functions map programs to observables. The part of evaluation dealing with observing the answers may have side effects! Sec 5.1 rigorously shows that lambda-calculus with global state and destructive mutation may be called pure functional, if effects are regarded as values and the program is written in what we now call a monadic style (whose idea was proposed by Reynolds back in 1981 when studying Idealized Algol). The end of Sec 5.1 remarks that IO can be treated that way -- and in fact, Appendix D of Haskell report 1.2 indeed had described such a semantics of IO: http://haskell.org/definition/haskell-report-1.2.ps.gz (the appendix starts on p. 139). Thanks to Paul Hudak for pointing this out three years ago. 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.
On Thu, 2009-03-05 at 20:11 -0800, oleg@okmij.org wrote:
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.
I think that `real' is a poor term to use in this context. In any case, we don't really need to assert that *any* IO action is non-deterministic; we just have to assert that: a) The result returned by unsafeInterleaveIO is non-deterministic, and b) The point in the execution thread when the side effects performed by unsafeInterleaveIO are inserted is non-deterministic. As for the first claim: we have *stronger* guarantees for unsafeInterleaveIO than for getStdRandom. As for the second claim: we have *stronger* guarantees for unsafeInterleavIO than for forkIO. I don't think it removes all possibility of reasoning about Haskell programs to say these things. You might want to stop hyper-ventilating.
We can't be sure of soundness of any compiler optimization.
Nope. *You* claim, without proof, that re-writing x `seq` y `seq` x - y to y `seq` x `seq` x - y is an un-sound optimization, for Haskell. *We* claim it is perfectly sound. Who is denying the soundness of Haskell optimization again?
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.
And plenty of C programs have situations where the relative ordering of side effects is undefined. In fact, quite a few syntactically valid, well-typed, conforming C programs are declared `undefined' (and hence not *strictly* conforming) by the standard, because their meaning depends on the order of evaluation beyond the degree to which it is well-defined. So C is hardly `far [better]' than Haskell in this regard!
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?
How weak?
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*.
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.
Amr Sabry in a paper ``What is a Purely Functional Language?'' J. Functional Programming, 8(1), 1-22, Jan. 1998. http://www.cs.indiana.edu/~sabry/papers/purelyFunctional.ps
proposed the definition of purity, see p 2 and Definition 4.7. The definition essentially states that call-by-name, call-by-value and call-by-need evaluation functions must be weakly equivalent.
How weakly? (False && undefined) gives different answers under call-by-name and call-by-value, but I don't think calling Haskell `unpure' because it exists is useful.
These evaluation functions map programs to observables. The part of evaluation dealing with observing the answers may have side effects! Sec 5.1 rigorously shows that lambda-calculus with global state and destructive mutation may be called pure functional, if effects are regarded as values and the program is written in what we now call a monadic style (whose idea was proposed by Reynolds back in 1981 when studying Idealized Algol). The end of Sec 5.1 remarks that IO can be treated that way -- and in fact, Appendix D of Haskell report 1.2 indeed had described such a semantics of IO: http://haskell.org/definition/haskell-report-1.2.ps.gz (the appendix starts on p. 139). Thanks to Paul Hudak for pointing this out three years ago.
Ahah! Haskell 1.2 had lazy IO (readChan), no?
Thus Haskell even with IO may be called pure functional. With Lazy IO,
For Lazy IO, read unsafeInterleaveIO.
it can no longer be called pure functional as different orders of evaluation of arguments of a function lead to different program observations.
Maybe. Nothing says GHC *won't* re-write f1 into f2, or vice-versa; it just happens to be the case that when you tried it it didn't happen. jcc
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
2009/3/6 <oleg@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
On Thu, 2009-03-05 at 20:11 -0800, oleg@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.h... 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
participants (5)
-
Dan Doel -
Duncan Coutts -
Jonathan Cast -
minh thu -
oleg＠okmij.org