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

[Daniel Fischer]

Am Montag, 24. Januar 2005 22:59 schrieb Benjamin Franksen:
> I wonder how you derive at this strange conclusion. Of course, getChar ==
> getChar is always true. Now we clearly have to say what we mean by this
> kind of equality. Well, there is an operational model of the program inside
> its environment (OS, etc..) in identity resp. equality of IO actions are
> defined with respect to this model. For instance:
>
> getChar = 'the action that, when executed, reads a character from stdin and
> returns it'
>
> > and that holds whether we just consider the values returned by an IO
> > action or take the action performed into account.
> > The sad truth is that IO actions in general aren't well defined entities
>
> I think the above definition is quite well defined.

I still say, getChar is not a well defined value of IO Char.
If it were, applying a function to it would always produce the same result.
Take the function
printAndReturnChar :: IO Char -> IO Char
printAndReturnChar ioC = do c <- ioC
                                              print c
                                              return c

that produces different results every time a different character is handed to 
getChar. And in this formulation, I see a solution to all this confusion, 
for, as I see it now, getChar is not a value of IO Char at all, it is a 
function with an implicit parameter, its type is actually
getChar :: (?x :: RealWorld) => IO Char.
As such it is of course well defined.
If I'm wrong, please tell me in what way.

> > 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).
>
> It is obviously plain wrong.

It is, if the above view is correct, however if you insist on getChar being of 
pure type IO Char, I still have a problem.

> Both are wrong. 'just the result matters' is the correct POV for functions,
> but not for IO actions. 'everything matters' is wrong even for IO actions,
> because the actual value returned when the action is executed is completely
> irrelevant to the IO action's identity.
>
> Seriously, the model in which the 'sameness' resp. identity of IO actions
> is defined takes into account only (a subset of all) externally observable
> effects, not the way a certain interpreter/compiler executes the action
> internally.
>
> I'll stop here; think I have made my point
>
> Ben
Now, I'd say two values of type IO a are the same if (on execution)
1. they return the same result,
2. they have the same relevant side effects.

I think, 1. should be acceptable to everybody, and 2. as a principle too, only 
the question of which effects are relevant needs to be answered. It's plain 
that not all measurable effects are relevant. My inclination to ignore the 
side-effects stemmed from the (irrational) desire to have IO's MonadPlus 
instance justified, now I'm prepared to say yes, side-effects such as output 
do count, so the instance MonadPlus IO is erroneous, but may be maintained 
for practical reasons.

Is there an authoritative list of which side-effects are relevant?
This would settle the question.

Daniel