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

[Benjamin Franksen]

On Monday 24 January 2005 21:23, Daniel Fischer wrote:
> Am Montag, 24. Januar 2005 11:47 schrieb Jules Bean:
> <snip>
>
> > Here are the three monad laws as written on the nomaware site:
> >
> > 	1.  	(return x) >>= f == f x
> > 	2.  	m >>= return == m
> > 	3.  	(m >>= f) >>= g == m >>= (\x -> f x >>= g)
> >
> > Taking rule 1, we do not simply mean that return x >>= f and f x have
> > the same type. (This is obviously true). We require that they are equal
> > as values of the type m a. In the case of IO, this means that they
> > perform the same action before yielding the same result.
>
> We face a severe problem here, not only that IO a is not an instance of Eq,
> which takes this whole discussion outside the realm of Haskell, on top of
> that we find the horrible fact that x /= x may be true in the IO Monad,
> consider 
>
> x = getLine >>= putStrLn
>
> or anything similar  -- actually we already have getChar /= getChar

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.

> (unless we index them with the space-time-coordinates of their invocation).

No need to do that.

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

> If you cannot agree, I have another question: is
>
> return 4 >> return 5 == return 5
>
> true in the IO-Monad?

Why, yes of course. That doesn't mean you can generalize it arbitrarily. It is 
true, because 'return 4' has no effect, other than returning '4' which is 
ignored by the '>>' operator. In our operational model, 'return 4 >> return 
5' has exactly the same externally visible effect as 'return 5', so they are 
equal.

> >From the 'just the result matters'-point of view, obviously.
> >From the 'everything matters'-point of view not.

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.

> I feel a little more at home with the former, because it matches the
> extensional equality of set theory, but I'm not happy with either.
> For any mathematician, the function
> \x -> 2*sin x * cos x
> IS the same function as
> \x -> sin (2*x)
> (given the equality of their respective domains -- though, for ghc they
> aren't, due to rounding errors), 

The above equality depends on what sin and cos mean. Regarded as functions on 
real numbers it is correct. It is false if they are considered functions on 
floating point numbers (and thus only approximating the 'real' sin/cos).

> so if we transport this extensionality to 
> our problem -- I am aware that is problematical because of the side-effects
> -- we get
> putStrLn "hello" >> mzero == mzero.

As I said, this is complete nonsense.

> > Example:
> >
> > return "hello" >>= putStrLn
> >
> > this does not only have the same type as putStrLn "hello", and return
> > the same value (), but it also carries out exactly the same actions.
>
> But does it really? hugs thinks otherwise:
> Prelude> putStrLn "hello"
> hello
> ()
> (28 reductions, 55 cells)
> Prelude> return "hello" >>= putStrLn
> hello
> ()
> (31 reductions, 56 cells)
> Prelude> putStrLn "hello"
> hello
> ()
> (26 reductions, 50 cells)
>
> even the same input does not necessarily lead to exactly the same actions,
> depending on whether "hello" is already known or not.

And also some of the electrons on transistor 19348587434 on the CPU chip move 
with a slightly reduced velocity due to the computer user shouting curses at 
his machine...

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