[Haskell-cafe] Re: what is inverse of mzero and return?

[Jorge Adriano Aires]

> 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.