[Haskell-cafe] Re: what is inverse of mzero and return?
jules at jellybean.co.uk
Tue Jan 25 04:07:15 EST 2005
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
>> 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
> 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
> 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
>>> 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
> that not all measurable effects are relevant. My inclination to ignore
> side-effects stemmed from the (irrational) desire to have IO's
> instance justified, now I'm prepared to say yes, side-effects such as
> do count, so the instance MonadPlus IO is erroneous, but may be
> 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.
More information about the Haskell-Cafe