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

[Jules Bean]

On 25 Jan 2005, at 08:53, Daniel Fischer wrote:

> Am Montag, 24. Januar 2005 22:59 schrieb Benjamin Franksen:
>> 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.

You are wrong in suggesting that an 'action' must necessarily give the 
same result every time it is called.

Your action (printAndReturnChar getChar) :: IO Char is a single, 
well-defined member of the type IO Char. Its denotation in a particular 
model will be something like 'read a character from stdin, print it and 
then return the value'. One can imagine a simplistic (pure haskell) 
implementation of IO in which a member of IO a is a list of 'SysCalls' 
together with a 'wiring diagram' which indicates how to connect 
together the return values of SysCalls. Others have alluded to concrete 
implementations along these lines but a bit more sophisticated.

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

I think you misunderstand 'pure type IO Char'. Being of 'pure type IO 
Char' does not mean that you will always return the same Char value.

Does it help you to think of the State monad? It is easy to imagine a 
value of (pure!) type State s Char which returns a different value 
depending on the state 's' which is passed to evalState.

In this way, the return value of an action of type IO Char depends on 
the state of the real world which is 'passed to it' by the haskell main 
loop (which is the analogue of evalState for the real world).

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

1 is quite incorrect. Two values of type 'State s a' can be precisely 
the same (even syntactically the same, which is stronger) and still 
return different results when run in different states.

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

The 'relevant' side effects are approximately 'Syscalls'. These include 
all such things as reading/writing, generating random numbers, opening 
network sockets, displaying windows, and so on.

Jules