[Haskell-cafe] Question about Lazy.IO
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? Greetings, Gerben -- View this message in context: http://www.nabble.com/Question-about-Lazy.IO-tp25236848p25236848.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Question about Lazy.IO
On Tue, Sep 1, 2009 at 3:05 AM, staafmeisterg.c.stave...@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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Question about Lazy.IO
Dear Luke, Thanks for your reply. I am interested in a more detailed explanation. If it's to long for this forum you can also mail it to me. In response to your answer. In your program the user is also a pure function. But I, as a user, am not pure so I can do side effects. More specific suppose I program something like this ss - hGetContent handle (lazy IO) dosomethingweird handle ss (a function that alters the file at will) Now as a programmer I should be positive that ss will be the file as it was before dosomethingweird modifies it. But this can never be guaranteed if ss is lazy. And now things start to depend on the order of evaluation breaking referential transparency, or do I overlook something. For concreteness suppose dosomethingweird appends ss to the end of the file. If ss is strict then it just copies the whole file, if ss is lazy it copies the whole file an infinite number of times. Gerben -- View this message in context: http://www.nabble.com/Question-about-Lazy.IO-tp25236848p25238044.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Question about Lazy.IO
2009/09/01 Luke Palmer lrpal...@gmail.com: 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. I'm sure I'm not alone when I say I'd like to see the longer, more technical response. -- Jason Dusek ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Question about Lazy.IO
I'm sure I'm not alone when I say I'd like to see the longer, more technical response. No, you aren't. Please `flood in' :-) -- ~dsouza yahoo!im: paravinicius gpg key fingerprint: 71B8 CE21 3A6E F894 5B1B 9ECE F88E 067F E891 651E ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
