[Haskell-cafe] Re: what is inverse of mzero and return?
Jorge Adriano Aires
jadrian at mat.uc.pt
Mon Jan 24 20:53:57 EST 2005
> >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.
More information about the Haskell-Cafe
mailing list