> We face a severe problem here, not only that IO a is not an instance of Eq, > which takes this whole discussion outside the realm of Haskell, on top of > > that we find the horrible fact that x /= x may be true in the IO Monad, > consider > > x = getLine >>= putStrLn > > or anything similar -- actually we already have getChar /= getChar
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... In fact, I do not agree. See Rant 2 below. > The sad truth is that IO actions in general aren't well defined entities > (unless we index them with the space-time-coordinates of their invocation). > So I suggest ending the discussion by agreeing that the question whether or > not > x >> mzero == mzero > holds in the IO-Monad is meaningless (at least, it's fruitless). > If you cannot agree, I have another question: is > > return 4 >> return 5 == return 5 > > true in the IO-Monad? Yeap, I thought about it too, have no idea, and cannot afford to spend much time thinking about it now either, since I got work to do... :-/ --- Rant 1 My gut feeling would be no. I think my intuitive reasoning is too just consider that, every IO action is equal to itself, then take the closure with respect to function application, and assume all others cannot be proved. That is, x === x, for all x :: IO a f x === g x, for all x :: a and f,g :: a -> IO b, such that f === g Where equality between functions is defined the usual way. --- Rant 2 Nope, we have to have getChar === getChar. I think you'll agree if I say that we have: 1. return === return 2- return 5 === return 5 return 5 >> return 5 === return 5 >> return 5 Because this has nothing to do with IO. 1. We have that, return :: a->IO a is a function, not an action, so it must be equal to itself. 2. We have that, return :: a->IO a is a function, not an action, so it must return the same value when applied to the same element. 3. (>>) :: (Monad m) => m a -> m b -> m b It is also a function, so (>>) x === (>>) x. And by the same reasoning (>>) x y === (>>) x y. So from 2 we have 3. A constant c :: a is just morphism(function) c : 0 -> a, where 0 is the initial object (empty set). So we must have c === c. Which means getChar === getChar. In other words, by questioning wether you can have x ==/= x for x :: IO a, you are questioning wether we really have f === f for all functions f::a->b. --- > > return "hello" >>= putStrLn > > > > this does not only have the same type as putStrLn "hello", and return > > the same value (), but it also carries out exactly the same actions. > > But does it really? hugs thinks otherwise: > Prelude> putStrLn "hello" > hello > () > (28 reductions, 55 cells) > Prelude> return "hello" >>= putStrLn > hello > () > (31 reductions, 56 cells) > Prelude> putStrLn "hello" > hello > () > (26 reductions, 50 cells) > > even the same input does not necessarily lead to exactly the same actions, > depending on whether "hello" is already known or not. 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 just showed is that those IO () elements (actions) when executed, always created different side effects in the real world. Not that the actions themselves are different. J.A. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
