Re: [Haskell-cafe] Re: [Haskell] Lazy IO breaks purity

You're assuming that IO operations have semantics.

From the Haskell program's point of view, and when reasoning about Haskell programs (not their interaction with the world) you should assume that every IO operation returns a random result. The way Oleg's program behaves does not break RT under the random result assumption.

What could break RT is if you could do this f :: Int -> Int <- someIOoperation let x = f 0; y = f 0 and end up with x and y not being equal. It's (of course) easy to construct someIOoperation that has this behaviour (using FFI), but I don't think you can construct it just using the normal IO operations and unsafeInterleaveIO. But as I said, I think this is a problem anyway, because IO without semantics is rather useless. -- Lennart On Thu, Mar 5, 2009 at 1:08 PM, Simon Marlow wrote:

Lennart Augustsson wrote:

...

I don't see any breaking of referential transparence in your code. Every time you do an IO operation the result is basically non-deterministic since you are talking to the outside world. You're assuming the IO has some kind of semantics that Haskell makes no promises about.

I'm not saying that this isn't a problem, because it is. But it doesn't break referential transparency, it just makes the semantics of IO even more complicated.

(I don't have a formal proof that unsafeInterleaveIO cannot break RT, but I've not seen an example where it does yet.)

So the argument is something like: we can think of the result of a call to unsafeInterleaveIO as having been chosen at the time we called unsafeInterleaveIO, rather than when its result is actually evaluated. This is on dodgy ground, IMO: either you admit that the IO monad contains an Oracle, or you admit it can time-travel.   I don't believe in either of those things :-)

Cheers,        Simon

...

 -- Lennart

On Thu, Mar 5, 2009 at 2:12 AM,   wrote:

...

We demonstrate how lazy IO breaks referential transparency.  A pure function of the type Int->Int->Int gives different integers depending on the order of evaluation of its arguments. Our Haskell98 code uses nothing but the standard input.  We conclude that extolling the purity of Haskell and advertising lazy IO is inconsistent.

Henning Thielemann wrote on Haskell-Cafe:

...

Say I have a chain of functions: read a file, ... write that to a file, all of these functions are written in a lazy way, which is currently considered good style

Lazy IO should not be considered good style. One of the common definitions of purity is that pure expressions should evaluate to the same results regardless of evaluation order, or that equals can be substituted for equals. If an expression of the type Int evaluates to 1, we should be able to replace every occurrence of the expression with 1 without changing the results and other observables.

The expression (read s) where s is the result of the (hGetContents h1) action has the pure type, e.g., Int. Yet its evaluation does more than just producing an integer: it may also close a file associated with the handle h1. Closing the file has an observable effect: the file descriptor, which is a scarce resource, is freed. Some OS lock the open file, or prevent operations such as renaming and deletion on the open file. A file system whose file is open cannot be unmounted. Suppose I use an Haskell application such as an editor to process data from a removable drive. I mount the drive, tell the application the file name. The (still running) application finished with the file and displayed the result. And yet I can't unplug the removable drive, because it turns out that the final result was produced without needing to read all the data from the file, and the file remains unclosed.

Some people say: the programmer should have used seq. That is the admission of guilt! An expression (read s)::Int that evaluates to 1 is equal to 1. So, one should be able substitute (read s) with 1. If the result of evaluating 1 turns out not needed for the final outcome, then not evaluating (read s) should not affect the outcome. And yet it does. One uses seq to force evaluation of an expression even if the result may be unused. Thus the expression of a pure type has *side-effect*.

The advice about using seq reminds me of advice given to C programmers that they should not free a malloc'ed pointer twice, dereference a zero pointer and write past the boundary of an array. If lazy IO is considered good style given the proper use of seq, then C should be considered safe given the proper use of pointers and arrays.

Side affects like closing a file are observable in the external world. A program may observe these effects, in an IO monad. One can argue there are no guarantees at all about what happens in the IO monad. Can side-effects of lazy IO be observable in _pure_ Haskell code, in functions with pure type? Yes, they can. The examples are depressingly easy to write, once one realizes that reading does have side effects, POSIX provides for file descriptor aliasing, and sharing becomes observable with side effects. Here is a simple Haskell98 code.

...

{- Haskell98! -}

module Main where

import System.IO import System.Posix.IO (fdToHandle, stdInput)

-- f1 and f2 are both pure functions, with the pure type. -- Both compute the result of the subtraction e1 - e2. -- The only difference between them is the sequence of -- evaluating their arguments, e1 `seq` e2 vs. e2 `seq` e1 -- For really pure functions, that difference should not be observable

f1, f2:: Int -> Int -> Int

f1 e1 e2 = e1 `seq` e2 `seq` e1 - e2 f2 e1 e2 = e2 `seq` e1 `seq` e1 - e2

read_int s = read . head . words $ s

main = do       let h1 = stdin       h2 <- fdToHandle stdInput       s1 <- hGetContents h1       s2 <- hGetContents h2       print $ f1 (read_int s1) (read_int s2)       -- print $ f2 (read_int s1) (read_int s2)

One can compile it with GHC (I used 6.8.2, with and without -O2) and run like this  ~> /tmp/a.out  1  2  -1 That is, we run the program and type 1 and 2 as the inputs. The program prints out the result, -1. If we comment out the line "print $ f1 (read_int s1) (read_int s2)" and uncomment out the last line the transcript looks like this  ~> /tmp/a.out  1  2  1

Running the code with Hugs exhibits the same behavior. Thus a pure function (-) of the pure type gives different results depending on the order of evaluating its arguments.

      Is 1 = -1?

_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell

_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe