Daniel Fischer
getChar = 'the action that, when executed, reads a character from stdin and returns it'
I still say, getChar is not a well defined value of IO Char.
By this line of reasoning, I think any imperative, real-world interacting program is ill-defined. While in principle, I'd be happy to champion pure functional programs, I would worry that this definition is slighly too narrow to be useful. :-)
If it were, applying a function to it would always produce the same result. Take the function printAndReturnChar :: IO Char -> IO Char printAndReturnChar ioC = do c <- ioC print c return c
This is an IO action parametrized by another IO action.
that produces different results every time a different character is handed to getChar.
But the IO action it returns is still equal to itself, even if it gives different results for different inputs.
And in this formulation, I see a solution to all this confusion, for, as I see it now, getChar is not a value of IO Char at all, it is a function with an implicit parameter, its type is actually getChar :: (?x :: RealWorld) => IO Char.
Or rather: getChar :: (?x :: RealWorld) -> (Char,RealWorld) Which is the whole point of IO, no? So yes, that's the essence.
if you insist on getChar being of pure type IO Char, I still have a problem.
Not if "pure type IO" means RealWorld -> (_,RealWorld)
Now, I'd say two values of type IO a are the same if (on execution) 1. they return the same result, 2. they have the same relevant side effects.
I think, 1. should be acceptable to everybody, and 2. as a principle too, only the question of which effects are relevant needs to be answered.
Well, why not use the same definition as for functions - quoted previously in this thread. They must have the same domain and range, and for each value in the domain, they must give the same result. So for (f,g :: IO a), for these to be equal, they must produce the same value of type a if the state of the RealWorld is equal. "Relevance" isn't necessary for this definition, but I guess you could consider a dimension of the domain irrelevant if the resulting values of f and g is independent of it.
It's plain that not all measurable effects are relevant.
I'm not sure. If I can tell the difference from within my program, I would say that they were different -- even if the difference was "irrelevant" (e.g. one function taking more time than another). But as Eq isn't defined for IO actions, it's a metaphysical question; you can happily call two IO actions the same, even if you can measure a different number of reductions or whatever - for getChar you usually care about input and output, and not about pedantic resource use, so this is not "relevant" in that particular case. (In a real-time setting, you would perhaps ha different criteria for relevance.) Just my opinion, anyway. -kzm -- If I haven't seen further, it is by standing in the footprints of giants