re: I/O monad

[juan_gandhi]

Just agreed with Runar that, well, it's not a monad, because there's no associativity (duh)

Or? (ok, ok, lax weak pseudo promonad...)

Comments

[thedeemon.livejournal.com]

Why?
It's building a sequence of actions, so it's as associative as list.

[nponeccop.livejournal.com]

Тут мы упираемся в отсутствие у IO денотационной семантики.

А если смотреть операционно - то ассоциативности (и монадичности) нет.

[thedeemon.livejournal.com]

А подробнее? Почему нет?

[nponeccop.livejournal.com]

Ну, на языке labelled transitions её нет. См. http://research.microsoft.com/en-us/um/people/simonpj/papers/marktoberdorf/mark.pdf раздел 3

[sassa-nf.livejournal.com]

гм, я, может, пропустил, но где там об отсутствии ассоциативности в operational semantics?

[huzhepidarasa.livejournal.com]

It is not entirely clear what is meant here. Can you give an example?

[juan-gandhi.livejournal.com]

First, we have to come up with a formal definition. The way he defines it (or it is defined in Haskell), it is not.

But also see other comments with detailed paper link.

[huzhepidarasa.livejournal.com]

Associativity is defined like this:

 (m >>= f) >>= g ≡	 m >>= (\x -> f x >>= g)

Or with the Kleisli arrow notation:

 (a >=> b) >=> c ≡	 a >=> (b >=> c)

Can you give an example of m,f,g or a,b,c or whatever that violate these axioms? The linked paper seems to say nothing about it.

I have tried the usual functions like getChar and putChar, and also bottom, and they all seem to obey.

[sassa-nf.livejournal.com]

I couldn't find this in the paper quoted above, but I guess it could be this:

if you look at a >=> (b >=> c), what is the meaning of parentheses? Does this mean you can evaluate the term on the right of (a >=>) to get a value, which then is cobined with >=>?

Eg will it be allowed to reduce (getChar >>= (\c -> getChar >>= (\d -> print [c,d]))) by first evaluating (getChar >>= (\d -> print [c,d])) to obtain (\c -> print [c,d])?

[huzhepidarasa.livejournal.com]

It's exactly as with any other binary operation. (+) is associative when we are talking about integers (or integers modulo something). We are talking about the integer data type here as it exists in the language. This means a+(b+c) always produces the same integer as (a+b)+c. What does it mean for integers to be the same? We interpret integers (the language data type) as mathematical integers and say they are the same if their denotational semantics (i.e. corresponding mathematical integers) are the same.

(+) is not associative when we are talking about machine floating point numbers. (-) is not associative for any type of numbers. (++) is associative for lists.

(>=>) is associative for functions returning lists. Which means functions produced by f >=> (g >=> h) and (f >=> g) >=> h are the same, for any f g h. Again, list-returning functions are a Haskell type. What does it mean for such functions to be the same? We cannot compare functions directly, but we can say that if (f x) and (g x) are the same for all possible x, then f and g are the same.

Is (>=>) associative for functions returning IO actions? Maybe. What does it mean for two IO-action-returning functions to be the same? Well it's just like for any other function type (see above). So what does it mean for two IO actions to be the same? We cannot compare IO actions directly, but we can apply them to the ("an") outside world and observe the results. When f::IO() and g::IO(), applied to the same world, produce the same observable behaviour, we say they f and g are the same. I cannot give a formal definition to observable behaviour, or at least I cannot give one that is easy to work with. But I can damn well see when two programs in the same environment produce different results. So if there's no associativity, one should be able to observe different behaviour of f >=> (g >=> h) and (f >=> g) >=> h. So far I could not reproduce it.

[sassa-nf.livejournal.com]

You could not reproduce it, because you don't have a Haskell that lets you reproduce it.

But come back to the example I gave. If Haskell evaluated (getChar >>= \d -> print [c,d]) first (would that not be allowed?), to produce a function (\c -> print [c,d]), you'd notice that (getChar >>= (\c -> print [c,d])) prints characters in the order opposite to the evaluation order evaluating actions left to right. What rules forbid that evaluation order? Technically, nothing - only the beta reduction rule; which is not good enough of a promise - the beta reduction becomes dependent on evaluation order where it wasn't.

Or, like in your example with lists. World is such a datatype (and >>= is such an operation) that (World >>= World) >>= World is not the same as World >>= (World >>= World); meaning, if you have a World that is the result of combining World >>= World, you cannot insert another effect _before_ this combination. It could work in an abstract machine, but does not work in real hardware - which works sequentially - where it matters in which order the terms are reduced.

[huzhepidarasa.livejournal.com]

Um, no. f >=> g means execute f first, g next. That's what people normally want when they do IO. It is not commutative. Note I say execute, not evaluate. IO values can be evaluated in any order, but after they are evaluated, they are executed by the IO execution mechanism, which is totally separate from the Haskell evaluation mechanism. And the execution is done *in order*. That's why we need the IO monad in the first place.

f >=> (g >=> h) means do f first, then do the combined action (g >=> h).

If you are switching the execution order around you are not doing IO.

[huzhepidarasa.livejournal.com]

Roughly, IO-monadic bind corresponds to a semicolon in C. You would translate f >=> g to C code like this:

run_io_action(f);
run_io_action(g)

(I omit parameters and results handling). Now, associativity of >=> is associativity of semicolon, so

{
  run_io_action(f);
  run_io_action(g);
}
run_io_action(h)

is the same as

run_io_action(f);
{
  run_io_action(g);
  run_io_action(h);
}

You would not execute the g;h block in the second example before you execute f.

[sassa-nf.livejournal.com]

yes, it is a semicolon even for other monads. (eg synchronized(){} is also a monad, and so is try{}catch{}finally{} - the monad specifies what the meaning of the semicolon is)

yes, I see it is associativity of composition. So then the claim that IO is not associative is not clear again.

[thedeemon.livejournal.com]

Remember that IO is a State monad with RealWorld as the state type. Try expanding it in your example.

[sassa-nf.livejournal.com]

yes, it doesn't work. I mean, the claim that it's not associative doesn't work.

In the end it is associativity of composition, because everything is turned into function of World returning World.

[juan-gandhi.livejournal.com]

Actually I can't. I'm still puzzled.

[huzhepidarasa.livejournal.com]

Both left-biased and right-biased triple composition can be translated to the same imperative code, which I guess *is* the operational semantics here. So I don't really see how there could be no associativity.

The Kleisli arrow can be translated to

arrow(f,g,a):
  u = runMonad(g,a)
  v = runMonad(f,u)
  return unitMonad(v)

Associativity here simply means you can inline procedure calls.