Am Dienstag, 25. Januar 2005 10:17 schrieben Sie:
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. ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Quite my point. Jules: In your example, the state is explicitely mentioned, no reason for confusion
Okay, so everything in an IO type has an implicit RealWorld parameter, right? In the above formulation, I meant 'pure' to exclude the RealWorld. If IO always includes RealWorld, we are d'accord. there.
"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.
And I can agree with it.
-kzm
D.