On Tue, Sep 1, 2009 at 3:05 AM, staafmeister
Hi,
I've been wondering about Lazy IO for a while. Suppose we have a program like
main = interact (unlines . somefunction . lines)
then somefunction is a pure function. With the semantic interpretation of: given a input list return an output list. However I, the user, can change my input depending on the output of this function. Now in simple cases like this, this will not be a problem. But suppose you are reading and writing to a file. Now the result of pure functions become dependent on the order of execution, breaking (I think) referential transparency. Am I wrong here or how could you prove that Lazy IO is consistent nonetheless?
Ignoring timeliness in responses (which our theory doesn't talk about), you are allowed to change your input based on its output in exactly the same way as any other function could. The reason this is okay is in the realm of domain theory. There is a good introductory tutorial in the Haskell wikibook: http://en.wikibooks.org/wiki/Haskell/Denotational_semantics Here is an intuition. Let's forget you are a user, and just call you a function "user". user :: String -> String program :: String -> String The input and output of a program is related to these functions like so: let input = user output output = program input in (input, output) Now, user could certainly be a function like: user ('a':rest) = 'x':rest user ('b':rest) = 'y':rest Which makes a decision about what to "type" before seeing all the output. Program could make use of this: program inp = 'a':case inp of { 'x':_ -> "hello"; 'y':_ -> "world" } This mutual recursion would not be well-defined if all of the output must be seen before the input can be known, because the output depends on the input and the input depends on the output. However, this is a perfectly valid Haskell program, without considering I/O, and will compute (input, output) to be ("xhello", "ahello"). I have now tried twice to explain why this is possible more deeply in terms of domain theory, but it has bloated the message to three times this size. If you would like me to include my response, I'd be more than happy to, but it does get rather technical. Luke