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

[Ketil Malde]

Daniel Fischer <daniel.is.fischer at web.de> writes:

>> getChar = 'the action that, when executed, reads a character from stdin and
>> returns it'

> I still say, getChar is not a well defined value of IO Char.

By this line of reasoning, I think any imperative, real-world
interacting program is ill-defined.  While in principle, I'd be happy
to champion pure functional programs, I would worry that this
definition is slighly too narrow to be useful. :-)

> 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

This is an IO action parametrized by another IO action.

> that produces different results every time a different character is
> handed to getChar.

But the IO action it returns is still equal to itself, even if it
gives different results for different inputs.

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

Or rather:
         getChar :: (?x :: RealWorld) -> (Char,RealWorld)

Which is the whole point of IO, no?  So yes, that's the essence.

> if you insist on getChar being of 
> pure type IO Char, I still have a problem.

Not if "pure type IO" means RealWorld -> (_,RealWorld)

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

Well, why not use the same definition as for functions - quoted
previously in this thread.  They must have the same domain and range,
and for each value in the domain, they must give the same result.

So for (f,g :: IO a), for these to be equal, they must produce the
same value of type a if the state of the RealWorld is equal.

"Relevance" isn't necessary for this definition, but I guess you could
consider a dimension of the domain irrelevant if the resulting values
of f and g is independent of it.

> It's plain that not all measurable effects are relevant. 

I'm not sure.  If I can tell the difference from within my program, I
would say that they were different -- even if the difference was
"irrelevant" (e.g. one function taking more time than another).

But as Eq isn't defined for IO actions, it's a metaphysical question;
you can happily call two IO actions the same, even if you can measure
a different number of reductions or whatever - for getChar you usually
care about input and output, and not about pedantic resource use, so
this is not "relevant" in that particular case.  (In a real-time
setting, you would perhaps ha different criteria for relevance.)

Just my opinion, anyway.

-kzm
-- 
If I haven't seen further, it is by standing in the footprints of giants