This isn't obvious to me. So x is an action, and it does not always produces the same side effects when executed. But why should that make x/=x? It is the same action, it gets one line from the input, and then prints it...
OK, but then the different side-effects could not be used to distinguish putStrLn "hello" >> mzero and mzero. So I still believe, if you say these two are different, because they produce different output, you cannot easily insist on x === x.
Agree. But I don't say that.
This I don't agree with, I think you are using the word actions for two different things, the elements of type IO a, and their execution. What you
You're right, but one of my problems is to identify elements of type IO a. If the returned value isn't the thing, the execution must matter, but which parts of the execution are to be taken into account?
How can we tell if functions f === g? They must have the same domain, codomain and return the same result for every element of the domain. This is just the mathematical definition. For any two arbitrary functions f,g, can you tell if they are the same or not? As a definition, I'd be happy to have, x,y :: IO a are the same if, given the same, real world, they produce the same effects and return the same result. Now I'm not saying we can derive that x === x, for x ::IO, from that, but it is certainly consistent with that point of view, so we can take it as an axiom. Which I think we already do. We also have that if f === g than f x === g x. That includes functions of type f,g :: a -> IO b. All seems consistent. Any other "equality" relation should include that one. Is it enough? It's enough to be able to tell that: putStrLn "hello" >> return 3 === putStrLn ("he"++"llo") >>=\ _ return (1+2) And it would say nothing about things like: return 4 >> return 5 ==?== return 5 I can live with it. To prove that two functions are in deed the same, we may use, say, number theory knowledge, which falls outside the scope of haskell. I find it sensible to do the same with actions. Maybe (not sure) it is sensible to specify return::(a -> IO a), as an action with no side effects such that return x === return x iff x === x. If we add that to our knowledge of IO, along with an appropriate specification for (>>=), then we would have: return 4 >> return 5 === return 5 J.A.