text: > >This. Agree. But I don't say? 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.