[Haskell-cafe] Re: evaluation semantics of bind

[wren ng thornton]

Gregg Reynolds wrote:
> 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.

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.

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