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

[Jorge Adriano Aires]

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