[Haskell-cafe] Re: what is inverse of mzero and return?
Benjamin Franksen
benjamin.franksen at bessy.de
Mon Jan 24 16:59:30 EST 2005
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
More information about the Haskell-Cafe
mailing list