[Haskell-cafe] Re: evaluation semantics of bind

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 7:19 PM, wren ng thornton <wren at freegeek.org> 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.  Bind can be thought of as an
"augmented application" operator: x >>= f applies f to x, but it may
fiddle with x first.  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.

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

-gregg