Re: [Haskell-cafe] Re: evaluation semantics of bind

Gregg Reynolds wrote:

On Thu, Feb 5, 2009 at 7:19 PM, wren ng thornton wrote:

...

Gregg Reynolds wrote:

...

...

as the formal semantics of the language are concerned, there's no essential difference between "getChar >>= \x -> getChar" and " Foo 3

...

...

= \x -> Foo 7 " for some data constructor Foo. I should think the latter would be optimized; if so, why not the former? The presence of some hidden (from me, anyway) semantics is inescapable. There's no reason to assume the latter would be "optimized" either. Consider:

...

data NotIO a = NotIO String a

instance Monad NotIO where return x = NotIO "" x (NotIO s x) >>= f = (\(NotIO z y) -> NotIO (s++z) y) (f x)

notGetChar = NotIO "foo" 'a'

Let's consider your example:

notGetChar >>= \x -> notGetChar == (NotIO "foo" 'a') >>= (\x -> NotIO "foo" 'a') == (\(NotIO z y) -> NotIO ("foo"++z) y) ((\x -> NotIO "foo" 'a') 'a') == (\(NotIO z y) -> NotIO ("foo"++z) y) (NotIO "foo" 'a') == NotIO ("foo"++"foo") 'a'

You've defined >>= in such a way that it carries additional semantic weight. My example doesn't do that.

Yes, is does. Every bind operator does so (trivially for the Identity monad). What else would bind be "augmented" with if it's "augmented application"? Augmentation means to add structure. Bind does not "apply f to x", x is a monadic value which carries additional structure. What bind does is map f over x's structure and then calls join to collapse the monadic layers from the result.

If it doesn't then it amounts to ordinary function application, which can be optimized out. That's the point of my example: data constructors don't munge their arguments, and getChar is essentially a data constructor.

...

= f which the monad laws require to equal f x. Just because the Identity monad is trivial does not mean that bind is trivial. That's

Data constructors in general are not monads. To the extent that your Foo example is well typed it is isomorphic to the Identity monad. In which case your Foo x >>= f is exactly return x like saying that addition must do nothing because of it's behavior on 0.

...

NotIO has a Chars for "side effects". IO is a perfectly fine mathematical object, the only difference is that it is appending sequences of an abstract

Gotcha! "appending sequences" is not something mathematical values are inclined to do. They neither spin nor toil, let alone append.

Balderdash.

The dominant idiom - "IO values are actions" just doesn't work if you want formal semantics, no matter how useful it may be pedagogically.

IO values are absolutely not actions, that's the whole point. Actions, such as they exist at all, are merely a domain over which we've constructed a monoid. The semantics from this are minimal, but if you'd like to define the domain more precisely there are many people who would be grateful for your contribution to research on effect systems and the ontology of computational effects on reality.

...

The only way we can optimize away one of the calls to notGetChar (or any other monadic function) is if we can guarantee that no other computation will use either the monoidal values or the "contained" values associated with it. IO is defined with a bind operator that's strict in the monoidal value, which means we can never remove things (unless, perhaps, we can

Ok; but where does it say that in the language definition? I understand how it all works, but that comes from the many informal narrative expositions; my point is that if you tried to write a formal semantics for Haskell, a la ML, you couldn't do it without coming up with a different story for IO.

It says that in the function definitions for bind and return on the IO type. In GHC the IO type is defined such that it's a specialized version of the State monad where RealWorld is the type of the state it carries. You can look in the source code that defines IO if you care. Other compilers may choose a different implementation for IO which has the same observational behavior in which case their "story" will be different. IO is an abstract type which is defined only by its observational behavior. One aspect of this behavior is that it is a monad and is not the Identity monad. Everything else follows. -- Live well, ~wren