[Haskell-cafe] Re: what is inverse of mzero and return?
Jorge Adriano Aires
jadrian at mat.uc.pt
Mon Jan 24 18:29:35 EST 2005
> 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,
> 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
> 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
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"
> (28 reductions, 55 cells)
> Prelude> return "hello" >>= putStrLn
> (31 reductions, 56 cells)
> Prelude> putStrLn "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.
More information about the Haskell-Cafe