[Haskell-cafe] Question about Lazy.IO

[Luke Palmer]

On Tue, Sep 1, 2009 at 3:05 AM, staafmeister<g.c.stavenga at uu.nl> wrote:
> 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