Re: [Haskell-cafe] evaluation semantics of bind

[Alberto G. Corona]

Yes,  Just must be executed because by the very definition of bind for the
Maybe mondad,

 (>>=) Nothing f = Nothing
 (>>=) (Just x) f = f x

He need to know if the value injected is Just or   Nothing, but anyway, my
point is : it is just plain lazy functional code!. No magic inside.
everything depend on the definition of bind.


2009/2/11 wren ng thornton 
>
> Alberto G. Corona wrote:
>>
>> forwarded:
>>
>> Yes!  if no state is passed, the optimization makes sense and the term is
>> not executed, like any lazy evaluation. For example, I used the debugger
>> (that is, without optimizations) to verify it with the Maybe monad:
>> op x= x+x
>>
>> print $ Just (op 1) >>= \y-> return (Just 2)
>>
>> does not evaluate  op 1
>
> Presumably you mean?: print $ Just (op 1) >>= \y-> return 2
>
>
>> but
>>
>> print $ Just (op 1) >>= \y-> return y
>>
>> does execute it.
>
>
> Dashing off towards the White Knight, we should be careful what is said
here. If we take only the expression "Just (op 1) >>= \y-> return y" then
evaluating it yields "Just (op 1)". That is, it only evaluates to WHNF and
does not evaluate what's inside. It is only once this value is subsequently
handed off to print or some other function, that it may become evaluated.
>
> Similarly with the first example as originally written. It so happens that
bind is non-strict for the field in Just, so we can discard the "op 1".
However, according to the semantics we do not evaluate "Just 2" either; we
only need to evaluate the return which will produce Just and pass the
operand down. (Regardless of the fact that the value yielded by applying
Just to 2 is Just 2. Expressions and their denotations are different.)
>
> --
> Live well,
> ~wren
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[wren ng thornton]

Alberto G. Corona wrote:

forwarded:

Yes!  if no state is passed, the optimization makes sense and the term is
not executed, like any lazy evaluation. For example, I used the debugger
(that is, without optimizations) to verify it with the Maybe monad:
op x= x+x

print $ Just (op 1) >>= \y-> return (Just 2)

does not evaluate  op 1


Presumably you mean?: print $ Just (op 1) >>= \y-> return 2



but

print $ Just (op 1) >>= \y-> return y

does execute it.



Dashing off towards the White Knight, we should be careful what is said 
here. If we take only the expression "Just (op 1) >>= \y-> return y" 
then evaluating it yields "Just (op 1)". That is, it only evaluates to 
WHNF and does not evaluate what's inside. It is only once this value is 
subsequently handed off to print or some other function, that it may 
become evaluated.


Similarly with the first example as originally written. It so happens 
that bind is non-strict for the field in Just, so we can discard the "op 
1". However, according to the semantics we do not evaluate "Just 2" 
either; we only need to evaluate the return which will produce Just and 
pass the operand down. (Regardless of the fact that the value yielded by 
applying Just to 2 is Just 2. Expressions and their denotations are 
different.)


--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Richard O'Keefe]

On 11 Feb 2009, at 2:22 am, Gregg Reynolds wrote:

Is the result of evaluation a thunk/suspension/closer?


As T. S. Eliot wrote,
  "Teach us to care and not to care
   Teach us to sit still."

There are some things it is better not to care about
and this is one of them.




(Dash it, this really is getting us into White Knight land.)

What's White Knight land?


From Alice in Wonderland.


``You are sad,'' the Knight said in an anxious tone:
``let me sing you a song to comfort you.''

``Is it very long?'' Alice asked,
for she had heard a good deal of poetry that day.

``It's long,'' said the Knight,
``but it's very, {\it very} beautiful.
Everybody that hears me sing it---either
it brings tears to their eyes, or else---''

``Or else what?'' said Alice,
for the Knight had made a sudden pause.

``Or else it doesn't, you know.
The name of the song is called {\it `Haddocks' Eyes.'\/}{}''

``Oh, that's the name of the song, is it?''
Alice said, trying to feel interested.

``No, you don't understand,'' the Knight said,
looking a little vexed.
``That's what the name is {\it called}.
The name really {\it is `The Aged Aged Man.'\/}{}''

``Then I ought to have said, `That's what the {\it song}
is called?'' Alice corrected herself.

``No, you oughtn't:  that's quite another thing!
The {\it song} is called {\it `Ways and Means'\/}:
but that's only what it's {\it called}, you know.''

``Well, what {\it is} the song, then?'' said Alice,
who was by this time completely bewildered.

``I was coming to that,'' the Knight said.
``The song really {\it is `A-sitting On a Gate'\/}:
and the tune's my own invention.''


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Lennart Augustsson]

The result of an evaluation is always in WHNF (weak head normal form).
So if it's a function, it's been evaluated to \ x -> ..., but no
evaluation under lambda.
Similarely, if it's a data type it has been evaluated so the outermost
form is a constructor, but no evaluation inside the constructor.

The terms thunk/suspension/closure usually refer to implementation
rather than semantics.
But in terms of an implementation, the answer is no.  After evaluation
you will have none of those as the outmost thing.

  -- Lennart

2009/2/10 Gregg Reynolds :
> Is the result of evaluation a thunk/suspension/closer?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Mon, Feb 9, 2009 at 10:17 PM, Richard O'Keefe  wrote:

>
> On 10 Feb 2009, at 5:07 pm, Gregg Reynolds wrote:
>
>> Thanks.  I see the error of my ways.  So, IO expressions must be evaluated
>> if they are in the chain leading to main.
>>
>
>
> We need some standard terminology to distinguish
> between *evaluating* an expression and *performing*
> the result of an expression of type IO something.
>

Indeed.  Wrote a blog article about this proposing a semiotic approach:
http://syntax.wikidot.com/blog:4

>
> An IO expression that is passed to a function at a
> strict position must be evaluated whether the result
> is performed or not.
>
> An IO expression whose result will be performed must
> be evaluated before that performance can take place.
>

Is the result of evaluation a thunk/suspension/closer?


>
> (Dash it, this really is getting us into White Knight land.)
>

What's White Knight land?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Alberto G. Corona]

forwarded:

Yes!  if no state is passed, the optimization makes sense and the term is
not executed, like any lazy evaluation. For example, I used the debugger
(that is, without optimizations) to verify it with the Maybe monad:
op x= x+x

print $ Just (op 1) >>= \y-> return (Just 2)

does not evaluate  op 1

but

print $ Just (op 1) >>= \y-> return y

does execute it.



The trace of the first:

[1 of 1] Compiling Main ( test.hs, interpreted )
Ok, modules loaded: Main.
*Main> :set stop :list
*Main> :step main
Stopped at test.hs:4:6-43
_result :: IO () = _
3
4  main= print $ Just (op 1) >>= \y-> return  2
 ^^
5
[test.hs:4:6-43] *Main> :step
Stopped at test.hs:4:14-43
_result :: Maybe Integer = _
3
4  main= print $ Just (op 1) >>= \y-> return  2
^^
5
[test.hs:4:14-43] *Main> :step
Stopped at test.hs:4:14-24
_result :: Maybe Integer = _
3
4  main= print $ Just (op 1) >>= \y-> return  2
  ^^^
5
[test.hs:4:14-24] *Main> :step
Stopped at test.hs:4:35-43
_result :: Maybe Integer = _
3
4  main= print $ Just (op 1) >>= \y-> return  2
   ^
5
[test.hs:4:35-43] *Main> :step
Just 2


But in the second case op is executed:


*Main> :step main
Stopped at test.hs:4:6-43
_result :: IO () = _
3
4  main= print $ Just (op 1) >>= \y-> return  y
   ^^
5
[test.hs:4:6-43] *Main> :step
Stopped at test.hs:4:14-43
_result :: Maybe Integer = _
3
4  main= print $ Just (op 1) >>= \y-> return  y
   ^^
5
[test.hs:4:14-43] *Main> :step
Stopped at test.hs:4:14-24
_result :: Maybe Integer = _
3
4  main= print $ Just (op 1) >>= \y-> return  y
  ^^^
5
[test.hs:4:14-24] *Main> :step
Stopped at test.hs:4:35-43
_result :: Maybe Integer = _
y :: Integer = _
3
4  main= print $ Just (op 1) >>= \y-> return  y
   ^
5
[test.hs:4:35-43] *Main> :step
Just Stopped at test.hs:4:20-23
_result :: Integer = _
3
4  main= print $ Just (op 1) >>= \y-> return  y
  
5
[test.hs:4:20-23] *Main> :step
Stopped at test.hs:6:0-8
_result :: Integer = _
5
6  op x= x+x
^
7
[test.hs:6:0-8] *Main> :step
Stopped at test.hs:6:6-8
_result :: Integer = _
x :: Integer = _
5
6  op x= x+x
  ^^^
7
[test.hs:6:6-8] *Main> :step
Just 2




2009/2/5 Gregg Reynolds - Ocultar texto citado -

>
> On Thu, Feb 5, 2009 at 9:27 AM, Bulat Ziganshin 
wrote:
>>
>> Hello Gregg,
>>
>> Thursday, February 5, 2009, 6:20:06 PM, you wrote:
>>
>> > An optimizer can see that the result of the first getChar is
>> > discarded and replace the entire expression with one getChar without
>> > changing the formal semantics.
>>
>> this is prohibited by using pseudo-value of type RealWorld which is
>> passed through entire action stream. actually, order of execution is
>> controlled by dependencies on this values
>>
>> http://haskell.org/haskellwiki/IO_inside
>>
> Thanks.  I actually read that a few weeks ago and forgot all about it.  So
the gist is that type IO has special magic semantics.  Formal, but hidden.
Which means monad semantics are built in to the language, at least for that
type.  The Haskell Report doesn't seem to say anything about this, which
seems odd.
>
> But then for non-IO monads, the optimization would be allowed, no?  Of
course; only the IO monad has external world behavior.
>
> Thanks,
>
> gregg
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[wren ng thornton]

Gregg Reynolds wrote:

Tillmann Rendel wrote:
> An example where it would be wrong to ignore e:
>
>  sum ([1, 2] >>= const [21])
>
> This expression should evaluate to sum [21, 21] = 42, not sum [21] = 21.
>

Sigh.  I hate it when this happens.  Just when I thought I had it figured
out, it turns out I'm clueless.  This is very enlightening and should
definitely be included in any monad tutorial.  Actually you don't even need
"sum" and "const" to demo the point,  "[1,2] >>= \x -> [21]" evals to "[21,
21]" in ghci.  And I have absolutely no idea why.  Very mysterious, the
Kleisli star.  :(


Just walk through the evaluation step by step, it's not so mysterious.

[1,2] >>= \x -> [21]
  == {CT definition of bind}
join . fmap (\x -> [21]) $ [1,2]
  ==
join [(\x -> [21]) 1, (\x -> [21]) 2]
  ==
join [[21],[21]]
  ==
[21,21]

Or if you prefer to use the Haskell function definitions instead of the 
category theory definitions (it's all the same):


[1,2] >>= \x -> [21]
  ==
concatMap (\x -> [21]) [1,2]
  ==
concat . map (\x -> [21]) $ [1,2]
  ==
concat [(\x -> [21]) 1, (\x -> [21]) 2]
  ==
concat [[21],[21]]
  ==
[21,21]


This is exactly the point I was raising earlier. The "statefullness" of 
monads has nothing to do with IO, but every monad has some of it. In 
general it is wrong to throw it away just because the function passed to 
bind happens to ignore the value associated with it. There are some 
cases where that can be correct, but in general it is not.


For lists, we can envision the statefullness as a path through a 
decision tree. To get the intuition right, it's easiest to pretend that 
we never call join (or that join does nothing). If we don't call join, 
eventually after a number of binds or maps we'll end up with some value 
of type [[...[a]...]]. We can draw that value out as a B-tree where each 
level has a branch of whatever arity it needs. In this B-tree, every 
leaf is associated with a unique path through the tree and therefore 
they can be distinguished.


The reason the above example works the way it does is that the initial 
list has two leaves each associated with their unique paths through this 
 tree of choices. The function passed into bind is a continuation of 
sorts. So, given that we can non-deterministically choose either of the 
paths in the original tree, for each choice we must then continue with 
(\x -> [21]) applied to the seed value for that choice (1 or 2, as 
appropriate). Because we had two choices initially, and from there we 
have only one choice, we will have 2*1 choices in the end:


   /\
  /  \
 (1) (2)
  |   |
  |   |
 21   21


If we imagine a finite state automaton, we might think that the two 21s 
could be collapsed together since they represent the same "state". But 
that is not so: the list monad is for *paths* through an FSA not for 
states in an FSA. (For states in an FSA we'd want the set monad 
instead.) Of course for the list monad we don't actually keep around the 
decision tree. In fact lists generalize over all possible decision trees 
which could yield the given distribution of path-endpoints, so it's not 
quite the way envisioned above.


--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[David Menendez]

2009/2/9 Gregg Reynolds :
> On Mon, Feb 9, 2009 at 11:06 AM, Tillmann Rendel  wrote:
>>
>> Gregg Reynolds wrote::
>>>
>>> My original question was motivated by the observation that a human reader
>>> of
>>> an expression of the form "e >>= f" , on seeing that f is constant, may
>>> pull
>>> the constant value out of f, disregard e and dispense with the
>>> application f
>>> e.
>>
>> While a human reader may well do that, but it would be correct or wrong
>> depending on the definition of >>=. The same is of course true for
>> compilers. By the way, there is no "application f e".
>
> I guess it would help if I got the notation right.  My intended meaning was
> f* e, where * is the Kleisli star.  Sorry about that.

You can't assume f* is a constant function just because f is. In fact,
in most monads (excluding Identity and Reader) f* is never constant.

>> An example where it would be wrong to ignore e:
>>
>>  sum ([1, 2] >>= const [21])
>>
>> This expression should evaluate to sum [21, 21] = 42, not sum [21] = 21.
>
> Sigh.  I hate it when this happens.  Just when I thought I had it figured
> out, it turns out I'm clueless.  This is very enlightening and should
> definitely be included in any monad tutorial.  Actually you don't even need
> "sum" and "const" to demo the point,  "[1,2] >>= \x -> [21]" evals to "[21,
> 21]" in ghci.  And I have absolutely no idea why.  Very mysterious, the
> Kleisli star.  :(

Here are two ways to think about it.

First, you can decompose the Kleisli star into two operations. That
is, for a monad T with multiplication mu,

   f* = mu . T f

Or in Haskell notation,

(f =<<) = join . fmap f

For the list monad, join is concat and fmap is map. So we have,

  [1,2] >>= \x -> [21]
= concat (map (\x -> [21])) [1,2]
= concat [[21],[21]]
= [21,21]

Second, in the list monad, we have a distributive law relating mplus and >>=.

mplus x y >>= f = mplus (x >>= f) (y >>= f)

We can rewrite [1,2] >>= \x -> [21] as

mplus (return 1) (return 2) >>= \x -> return 21

then we can distribute >>=,

mplus (return 1 >>= \x -> return 21) (return 2 >>= \x -> return 21)

then by the monad laws,

mplus (return 21) (return 21)

-- 
Dave Menendez 

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Richard O'Keefe]

On 10 Feb 2009, at 5:07 pm, Gregg Reynolds wrote:
Thanks.  I see the error of my ways.  So, IO expressions must be  
evaluated if they are in the chain leading to main.



We need some standard terminology to distinguish
between *evaluating* an expression and *performing*
the result of an expression of type IO something.

An IO expression that is passed to a function at a
strict position must be evaluated whether the result
is performed or not.

An IO expression whose result will be performed must
be evaluated before that performance can take place.

(Dash it, this really is getting us into White Knight land.)

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Mon, Feb 9, 2009 at 8:37 PM, Richard O'Keefe  wrote:

>
> There isn't any "application f e".
> Any human reader who does that is simply WRONG to do so.
>

Sorry, should have written f*

>
> In your fragmentary example,  may be discarded
> EVEN IF it contains IO expressions, it's only if they are linked into
> the IO chain using >> and/or >>= that the environment will perform
> their values.
>

Thanks.  I see the error of my ways.  So, IO expressions must be evaluated
if they are in the chain leading to main.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Mon, Feb 9, 2009 at 11:06 AM, Tillmann Rendel  wrote:

> Gregg Reynolds wrote::
>
>> My original question was motivated by the observation that a human reader
>> of
>> an expression of the form "e >>= f" , on seeing that f is constant, may
>> pull
>> the constant value out of f, disregard e and dispense with the application
>> f
>> e.
>>
>
> While a human reader may well do that, but it would be correct or wrong
> depending on the definition of >>=. The same is of course true for
> compilers. By the way, there is no "application f e".
>

I guess it would help if I got the notation right.  My intended meaning was
f* e, where * is the Kleisli star.  Sorry about that.

>
>
> An example where it would be wrong to ignore e:
>
>  sum ([1, 2] >>= const [21])
>
> This expression should evaluate to sum [21, 21] = 42, not sum [21] = 21.
>

Sigh.  I hate it when this happens.  Just when I thought I had it figured
out, it turns out I'm clueless.  This is very enlightening and should
definitely be included in any monad tutorial.  Actually you don't even need
"sum" and "const" to demo the point,  "[1,2] >>= \x -> [21]" evals to "[21,
21]" in ghci.  And I have absolutely no idea why.  Very mysterious, the
Kleisli star.  :(

Back to the drawing board!

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Richard O'Keefe]

On 10 Feb 2009, at 1:35 am, Gregg Reynolds wrote:
My original question was motivated by the observation that a human  
reader of an expression of the form "e >>= f" , on seeing that f is  
constant, may pull the constant value out of f, disregard e and  
dispense with the application f e.


There isn't any "application f e".
Any human reader who does that is simply WRONG to do so.

  So can a compiler, unless IO expressions are involved, in which  
case such optimizations are forbidden.


Remember that (e >>= f) means (>>=) e f.
When/whether it is sound to replace (>>=) e f by (f undefined)
depends on the semantics of >>=.

But >>= is an operation of a type class (the Monad type class).
If we come across

g :: Monad m => m a -> b -> m b
g e r = e >>= \x -> return r

then the compiler doesn't know what m is, so it doesn't know
which, if any, of its arguments >>= depends on.

data Trivial x = Trivial x

instance Monad Trivial
  where return = Trivial
(>>=) (Trivial a) f = f a

If we now try
h :: Trivial a -> b -> Trivial b
h e r = g e r
then the compiler can inline the call to g
h e r = e >>= \x -> return r
and inline the calls to >>= and return
h (Trivial a) r = (\x -> Trivial r) a
then simplify to
h (Trivial _) r = Trivial r

You might have thought that the result doesn't depend on
the first argument to h, but as written, it does.  This
version of h is strict in its first argument, so even
though there are NO side effects whatever, the first
argument will be evaluated to weak head normal form.

Of course, since there is only one constructor for Trivial,
it could be a newtype.  If I change that declaration to

newtype Trivial x = Trivial x

then the pattern match is implicitly irrefutable,

h ~(Trivial _) r = Trivial r

and if the compiler doesn't simplify ~(NTC _) to _ when NTC
is a newtype constructor, I'll be surprised, so it's like

h _ r = Trivial r

and the function will *NOT* be strict in its first argument.
Here you see that the soundness or otherwise of eliminating
the first argument of >>= when the second argument doesn't
depend on the eventual result has nothing to do with IO as
such and certainly nothing to do with side effects.  It's
really all about whether the version of >>= used is strict
in its first argument or not.


  I wondered if that was due to the semantics of >>= or the  
semantics of IO.


It's about the semantics of IO's implementation of >>=.




To summarize what I've concluded thanks to the helpful people on  
haskell-cafe:


The compiler can optimize e >>= f except for any IO expressions in e  
and f.


False.  There is nothing unusual about IO here.


  IO expressions must be evaluated, due to the semantics of IO.


False.


  The may not be disregarded, memoized, or substituted.


False.  In Haskell there is nothing whatever unusual about
expressions of type IO something.  They *MAY* be disregarded:
let n = length [getChar, putChar 'f']
can be optimised to let n = 2.  They MAY be memoised.  They
MAY be substituted.

IO semantics may be implemented in different ways by different  
compilers;


True.  But then, so may Int semantics.

these implementation techniques are not part of the formal semantics  
of the language, which may be expressed as above:  IO expressions  
must be evaluated wherever and whenever they occur.


False. Utterly false.



The bind operator >>= enforces sequencing on arguments containing IO  
expressions, but does not force evaluation.


False.  For the special case of IO (and for other similar monads)
>>= enforced sequence BY forcing evaluation (more precisely, by
being strict in its first argument).


Even bind expressions involving IO may be optimized.  For example:

  getChar >>= \x -> .. putChar 'c'

The compiler may discard  (assuming it contains  
no IO expressions), but it must evaluate getChar and putChar (due to  
IO semantics) in the correct order (due to bind semantics).


You are conflating *evaluating* (by the Haskell evaluator) with
*performance* (by the Haskell environment).  IO *values* are
determined by the Haskell evaluator exactly like any other values;
IO *actions* are performed by the Haskell environment as part of
the process of forcing the lazy evaluator to do some work.

In your fragmentary example,  may be discarded
EVEN IF it contains IO expressions, it's only if they are linked into
the IO chain using >> and/or >>= that the environment will perform
their values.




Thanks all,

gregg


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[David Menendez]

2009/2/9 Gregg Reynolds :
> On Sun, Feb 8, 2009 at 6:25 PM, Richard O'Keefe  wrote:
>>
>> On 6 Feb 2009, at 4:20 am, Gregg Reynolds wrote:
>>>
>>>  However, consider:
>>>
>>>getChar >>= \x -> getChar
>>>
>>> An optimizer can see that the result of the first getChar is discarded
>>> and replace the entire expression with one getChar without changing the
>>> formal semantics.
>>
>> But the result of the first getChar is *NOT* discarded.
>> **As an analogy**, think of the type IO t as (World -> (t,World))
>> for some hidden type World, and
>>getChar w = (c, w')
>>-- get a character c out of world w somehow,
>>-- changing w to w' as you go
>>(f >>= g) w = let (v,w') = f w in (g v) w'
>>
>> In this analogy, you see that the result of getChar is a value of
>> type IO Char (not of type Char), and that while the character
>> part of the result of performing the result of getChar may be
>> discarded, the "changed world" part is NOT.
>
> That's an implementation detail.  It doesn't account for other possible IO
> implementations.
>
> My original question was motivated by the observation that a human reader of
> an expression of the form "e >>= f" , on seeing that f is constant, may pull
> the constant value out of f, disregard e and dispense with the application f
> e.  So can a compiler, unless IO expressions are involved, in which case
> such optimizations are forbidden.  I wondered if that was due to the
> semantics of >>= or the semantics of IO.

Neither. It's because the expression "e >>= f" is not "f e". As far as
Haskell is concerned, >>= is just a higher-order function. You can't
arbitrarily replace "foo bar (const baz)" with "baz", unless it turns
out that foo = \x y -> y x.

Perhaps you're thinking of the monad law,

forall x f. return x >>= f  =  f x

The presence of "return" is important. Among other things, there is no
x such that getChar = return x. That's because getChar has (or,
rather, causes when interpreted by the RTS) side-effects, whereas
"return x" is pure.


Here's some code you can try on your own:

data IO a = Return a | Get (Char -> IO a) | Put Char (IO a)

instance Monad IO where
return = Return
Return a >>= f = f a
Get k >>= f = Get (\c -> k c >>= f)
Put c k >>= f = Put c (k >>= f)

getChar :: IO Char
getChar = Get (\c -> Return c)

putChar :: Char -> IO ()
putChar c = Put c (Return ())


Now, if the compiler sees "getChar >>= \_ -> getChar", it *can*
optimize out the >>=. But the result would be "Get (\_ -> Get (\c ->
Return c))", which is not equivalent to getChar. Neither IO semantics
nor monad semantics are involved.

-- 
Dave Menendez 

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Tillmann Rendel]

Gregg Reynolds wrote::

My original question was motivated by the observation that a human reader of
an expression of the form "e >>= f" , on seeing that f is constant, may pull
the constant value out of f, disregard e and dispense with the application f
e.  


While a human reader may well do that, but it would be correct or wrong 
depending on the definition of >>=. The same is of course true for 
compilers. By the way, there is no "application f e".



An example where it would be wrong to ignore e:

  sum ([1, 2] >>= const [21])

This expression should evaluate to sum [21, 21] = 42, not sum [21] = 21.


There is nothing special with IO or >>=, so there is no need to 
introduce special cases for IO or >>= in a formal or informal semantics 
of Haskell.


  Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Mon, Feb 9, 2009 at 7:17 AM, Lennart Augustsson
wrote:

> Just to clarify a little.
> If you implement the IO monad in a sane way (as some kind of state
> monad or continuation monad) then the compiler can optimize e>>=f even
> for the IO monad.  The implementation of >>= will ensure the
> sequencing of effects in e before effects in f.


I think this answers one of my questions about the relation of category
theory to Haskell. Bind is an implementation of the Kleisli star, but the
latter, being abstract, may encode data dependency but not sequence.  The IO
implementation of >>= must ensure sequence, regardless of data dependency
(e.g. even for putChar 'a' >>= \x -> putChar 'c').

So if we wanted to write a Haskell specification with more formality and
detail than the Report, we could say that the IO monad must implement the
Kleisli star operator, but that would not be enough, we would also have to
require that the implementation ensure sequencing.  IOW, Kleisli star
implementation plus a constraint on the implementation.  Does that sound
right?

>
> The IO monad is less magic than you seem to think it is. :)
>

Any sufficiently advanced technology is isomorphic to magic.  ;)

(http://www.quotationspage.com/quote/776.html)

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Lennart Augustsson]

Just to clarify a little.
If you implement the IO monad in a sane way (as some kind of state
monad or continuation monad) then the compiler can optimize e>>=f even
for the IO monad.  The implementation of >>= will ensure the
sequencing of effects in e before effects in f.
The IO monad is less magic than you seem to think it is. :)

  -- Lennart

2009/2/9 Gregg Reynolds :
> On Sun, Feb 8, 2009 at 6:25 PM, Richard O'Keefe  wrote:
>>
>> On 6 Feb 2009, at 4:20 am, Gregg Reynolds wrote:
>>>
>>>  However, consider:
>>>
>>>getChar >>= \x -> getChar
>>>
>>> An optimizer can see that the result of the first getChar is discarded
>>> and replace the entire expression with one getChar without changing the
>>> formal semantics.
>>
>> But the result of the first getChar is *NOT* discarded.
>> **As an analogy**, think of the type IO t as (World -> (t,World))
>> for some hidden type World, and
>>getChar w = (c, w')
>>-- get a character c out of world w somehow,
>>-- changing w to w' as you go
>>(f >>= g) w = let (v,w') = f w in (g v) w'
>>
>> In this analogy, you see that the result of getChar is a value of
>> type IO Char (not of type Char), and that while the character
>> part of the result of performing the result of getChar may be
>> discarded, the "changed world" part is NOT.
>
> That's an implementation detail.  It doesn't account for other possible IO
> implementations.
>
> My original question was motivated by the observation that a human reader of
> an expression of the form "e >>= f" , on seeing that f is constant, may pull
> the constant value out of f, disregard e and dispense with the application f
> e.  So can a compiler, unless IO expressions are involved, in which case
> such optimizations are forbidden.  I wondered if that was due to the
> semantics of >>= or the semantics of IO.
>
> To summarize what I've concluded thanks to the helpful people on
> haskell-cafe:
>
> The compiler can optimize e >>= f except for any IO expressions in e and f.
> IO expressions must be evaluated, due to the semantics of IO.  The may not
> be disregarded, memoized, or substituted.  IO semantics may be implemented
> in different ways by different compilers; these implementation techniques
> are not part of the formal semantics of the language, which may be expressed
> as above:  IO expressions must be evaluated wherever and whenever they
> occur.
>
> The bind operator >>= enforces sequencing on arguments containing IO
> expressions, but does not force evaluation.  Even bind expressions involving
> IO may be optimized.  For example:
>
>   getChar >>= \x -> .. putChar 'c'
>
> The compiler may discard  (assuming it contains no IO
> expressions), but it must evaluate getChar and putChar (due to IO semantics)
> in the correct order (due to bind semantics).
>
> Thanks all,
>
> gregg
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Sun, Feb 8, 2009 at 6:25 PM, Richard O'Keefe  wrote:

>
> On 6 Feb 2009, at 4:20 am, Gregg Reynolds wrote:
>
>>  However, consider:
>>
>>getChar >>= \x -> getChar
>>
>> An optimizer can see that the result of the first getChar is discarded and
>> replace the entire expression with one getChar without changing the formal
>> semantics.
>>
>
> But the result of the first getChar is *NOT* discarded.
> **As an analogy**, think of the type IO t as (World -> (t,World))
> for some hidden type World, and
>getChar w = (c, w')
>-- get a character c out of world w somehow,
>-- changing w to w' as you go
>(f >>= g) w = let (v,w') = f w in (g v) w'
>
> In this analogy, you see that the result of getChar is a value of
> type IO Char (not of type Char), and that while the character
> part of the result of performing the result of getChar may be
> discarded, the "changed world" part is NOT.


That's an implementation detail.  It doesn't account for other possible IO
implementations.

My original question was motivated by the observation that a human reader of
an expression of the form "e >>= f" , on seeing that f is constant, may pull
the constant value out of f, disregard e and dispense with the application f
e.  So can a compiler, unless IO expressions are involved, in which case
such optimizations are forbidden.  I wondered if that was due to the
semantics of >>= or the semantics of IO.

To summarize what I've concluded thanks to the helpful people on
haskell-cafe:

The compiler can optimize e >>= f except for any IO expressions in e and f.
IO expressions must be evaluated, due to the semantics of IO.  The may not
be disregarded, memoized, or substituted.  IO semantics may be implemented
in different ways by different compilers; these implementation techniques
are not part of the formal semantics of the language, which may be expressed
as above:  IO expressions must be evaluated wherever and whenever they
occur.

The bind operator >>= enforces sequencing on arguments containing IO
expressions, but does not force evaluation.  Even bind expressions involving
IO may be optimized.  For example:

  getChar >>= \x -> .. putChar 'c'

The compiler may discard  (assuming it contains no IO
expressions), but it must evaluate getChar and putChar (due to IO semantics)
in the correct order (due to bind semantics).

Thanks all,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Richard O'Keefe]

On 6 Feb 2009, at 4:20 am, Gregg Reynolds wrote:

 However, consider:

getChar >>= \x -> getChar

An optimizer can see that the result of the first getChar is  
discarded and replace the entire expression with one getChar without  
changing the formal semantics.


But the result of the first getChar is *NOT* discarded.
**As an analogy**, think of the type IO t as (World -> (t,World))
for some hidden type World, and
getChar w = (c, w')
-- get a character c out of world w somehow,
-- changing w to w' as you go
(f >>= g) w = let (v,w') = f w in (g v) w'

In this analogy, you see that the result of getChar is a value of
type IO Char (not of type Char), and that while the character
part of the result of performing the result of getChar may be
discarded, the "changed world" part is NOT.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Nils Anders Danielsson]

On 2009-02-05 15:20, Gregg Reynolds wrote:

I think I've just about got monads figured out, but [...]


I don't think anyone has mentioned Simon's "Tackling the awkward squad"
paper in this thread. This tutorial, which contains a semantics for a
subset of IO, should answer some of the questions raised.

 http://research.microsoft.com/en-us/um/people/simonpj/Papers/marktoberdorf/

--
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 10:00 AM, Lennart Augustsson
 wrote:
>
> There's nothing magic about IO when it comes to monad semantics.
> If you take ghc's implementation of IO, it's a state monad.

Doesn't that mean the semantics are defined by the implementation?  My
problem is that I'm not seeing how correct eval sequencing can be
forced unless a magic token is passed around, which means that /some/
such hidden semantics must be part of the formal semantics of IO.  In
other words, it's not enough for it to be a monad, since >>= by itself
cannot guarantee data dependency.  If it doesn't pass around the World
token, we don't get sequencing.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Jeremy Shaw]

Hello,

The type IO (in many Haskell implemenations) is essentially:

> type IO a  =  RealWorld -> (a, RealWorld)

And >> would be implemented like:

> (>>) :: IO a -> IO b -> IO b
> action1 >>= action2 = \world0 ->
>   let (a, world1) = action1 world0
>   (b, world2) = action2 world1
>   in (b, world2)

So, even though action2 does not depend on the 'a' value returned by
action1, it does depend on the world value. Hence, the compiler will
not optimize away the call to action1, because then it would not have
a 'world1' value to pass to action2.

It is the passing around of these 'world*' values that causes the IO
operations to happen in the right order.

Of course, this only works if the programmer is careful to ensure that
each world variable is used exactly once, and that no functions are
accidently skipped, etc. For example, lets say that (>>) was
accidently defined like:

> (>>) :: IO a -> IO b -> IO b
> action1 >>= action2 = \world0 ->
>   let (a, world1) = action1 world0
>   (b, world2) = action2 world0 -- oops, should be world1
>   in (b, world2)

now action1 would not be run. Since it is so easy to accidently screw
up the passing around of world variables, we don't do it 'by hand'. We
get it right once in the Monad instance, and then we don't have to
worry about it anymore.

- jeremy



At Thu, 5 Feb 2009 09:20:06 -0600,
Gregg Reynolds wrote:
> 
> [1  ]
> [1.1  ]
> I think I've just about got monads figured out, but there's one detail that
> still escapes me.  As I understand it, a monad is a kind of programming
> trick the uses data dependency to force evaluation order.  x >>= f means
> apply f to x; since the value of f x depends on the value of x, the
> evaluator must evaluate x before f x. However, consider:
> 
> getChar >>= \x -> getChar
> 
> An optimizer can see that the result of the first getChar is discarded and
> replace the entire expression with one getChar without changing the formal
> semantics.  But that would change the behavior, so to get the desired
> behavior, there must be some principle that prevents this from happening,
> ensuring that x >>= f always evaluates f x.
> 
> I can see that the monad laws ensure this But I haven't found anything that
> states this.  Am I missing something?
> 
> Thanks,
> 
> gregg
> [1.2  ]
> 
> [2  ]
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Jake McArthur]

-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1

Gregg Reynolds wrote:
| As I understand it, a monad is a kind of programming trick the uses
data dependency to force evaluation order.

Actually, a monad does nothing more than supply some combinators. These
combinators (and some trivial laws) are all you really need to know to
understand monads. Specific monads are really just a case-by-case issue.

Using some function names that are not used in the standard Haskell
libraries, here are the important functions you have access to when you
have a monad, all of which return monadic values:

~point ::   a -> f a
~map   ::   (a ->   b) -> f a -> f b
~apply :: f (a ->   b) -> f a -> f b
~bind  ::   (a -> f b) -> f a -> f b

I aligned the type signatures the way I did so you could see their
similarities and differences more easily.

point is the same as the return and pure functions. It lifts a pure value.

map is the same as the (<$>), fmap, liftA, and liftM functions. It
applies a pure function to a lifted value.

apply is the same as the (<*>) and ap functions. It applies a lifted
function to a lifted value.

The type signature for bind is reversed from that of (>>=). It's the
same as (=<<). I think it is more clear and better parallels the other
functions I've already shown. It applies a "lifting" function to a
lifted value.

| since the value of f x depends on the value of x, the evaluator must
evaluate x before f x

This is actually not true. Remember, Haskell is a lazy language. x need
not be evaluated before applying f to it.

| However, consider:
|
| getChar >>= \x -> getChar
|
| An optimizer can see that the result of the first getChar is discarded
and replace the entire expression with one getChar without changing the
formal semantics.

Consider how this expression would actually look in a Haskell program:

~main :: IO ()
~main = getChar >>= \x -> getChar

Remember, a type coincides with a value. That is, the entire main
function is a _value_ of type IO (). The value, as it so happens, is an
imperative program which the Haskell runtime performs. That is, the
reduction semantics of IO expressions _produce_, rather than perform,
actions. The actions are only performed by the runtime. Every monad has
a "run" function. The IO monad's run function is the Haskell runtime.

If you think of the IO monad as some sort of Writer monad, it is easy to
see that Haskell's reduction semantics actually guarantee correct order
of operations, and a semantics-preserving optimizer will not change it.

In GHC, the IO monad is actually more like a State monad (over
RealWorld). It is also easy to see that this preserves correct ordering
of side-effects as well. I just wanted to present a different point of view.

- - Jake
-BEGIN PGP SIGNATURE-
Version: GnuPG v1.4.9 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkmLDpMACgkQye5hVyvIUKnUpwCfdAycTBv29wVt+J5VHZbNEQ3H
80kAnj7u7HS+5S1qxgzB90I7v+ftuazo
=poXT
-END PGP SIGNATURE-
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Lennart Augustsson]

There's nothing magic about IO when it comes to monad semantics.
If you take ghc's implementation of IO, it's a state monad.
The new state generated by x is passed to f, so there's no way to skip x.
(Well, if the compiler can show that the state is not used anywhere
then it can start removing things, but in that case there really is no
change in semantics.)

  -- Lennart

2009/2/5 Gregg Reynolds :
> On Thu, Feb 5, 2009 at 9:27 AM, Bulat Ziganshin 
> wrote:
>>
>> Hello Gregg,
>>
>> Thursday, February 5, 2009, 6:20:06 PM, you wrote:
>>
>> > An optimizer can see that the result of the first getChar is
>> > discarded and replace the entire expression with one getChar without
>> > changing the formal semantics.
>>
>> this is prohibited by using pseudo-value of type RealWorld which is
>> passed through entire action stream. actually, order of execution is
>> controlled by dependencies on this values
>>
>> http://haskell.org/haskellwiki/IO_inside
>>
> Thanks.  I actually read that a few weeks ago and forgot all about it.  So
> the gist is that type IO has special magic semantics.  Formal, but hidden.
> Which means monad semantics are built in to the language, at least for that
> type.  The Haskell Report doesn't seem to say anything about this, which
> seems odd.
>
> But then for non-IO monads, the optimization would be allowed, no?  Of
> course; only the IO monad has external world behavior.
>
> Thanks,
>
> gregg
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 9:27 AM, Bulat Ziganshin
wrote:

> Hello Gregg,
>
> Thursday, February 5, 2009, 6:20:06 PM, you wrote:
>
> > An optimizer can see that the result of the first getChar is
> > discarded and replace the entire expression with one getChar without
> > changing the formal semantics.
>
> this is prohibited by using pseudo-value of type RealWorld which is
> passed through entire action stream. actually, order of execution is
> controlled by dependencies on this values
>
> http://haskell.org/haskellwiki/IO_inside
>
> Thanks.  I actually read that a few weeks ago and forgot all about it.  So
the gist is that type IO has special magic semantics.  Formal, but hidden.
Which means monad semantics are built in to the language, at least for that
type.  The Haskell Report doesn't seem to say anything about this, which
seems odd.

But then for non-IO monads, the optimization would be allowed, no?  Of
course; only the IO monad has external world behavior.

Thanks,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Roman Cheplyaka]

* Gregg Reynolds  [2009-02-05 09:20:06-0600]
> I think I've just about got monads figured out, but there's one detail that
> still escapes me.  As I understand it, a monad is a kind of programming
> trick the uses data dependency to force evaluation order.  x >>= f means
> apply f to x; since the value of f x depends on the value of x, the
> evaluator must evaluate x before f x. However, consider:
> 
> getChar >>= \x -> getChar
> 
> An optimizer can see that the result of the first getChar is discarded and
> replace the entire expression with one getChar without changing the formal
> semantics.  But that would change the behavior, so to get the desired
> behavior, there must be some principle that prevents this from happening,
> ensuring that x >>= f always evaluates f x.

x >>= f doesn't mean apply f to x. It means, roughly, "construct (IO) action 
from
actions x and f(..), so that they are executed sequentially and f depends on
a resuls produced by x". Even if f does not depend on its argument,
there's no reason for compiler to think that the first action may be
ignored.

If you think in terms of dependency, the second action depends on the
state of the "world" left after executing x. So all IO actions take an
implicit "world" argument and (>>=) operator implicitely passes modified
"world" to the next action.

> I can see that the monad laws ensure this But I haven't found anything that
> states this.  Am I missing something?

-- 
Roman I. Cheplyaka :: http://ro-che.info/
"Don't let school get in the way of your education." - Mark Twain
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Bulat Ziganshin]

Hello Gregg,

Thursday, February 5, 2009, 6:20:06 PM, you wrote:

> An optimizer can see that the result of the first getChar is
> discarded and replace the entire expression with one getChar without
> changing the formal semantics. 

this is prohibited by using pseudo-value of type RealWorld which is
passed through entire action stream. actually, order of execution is
controlled by dependencies on this values

http://haskell.org/haskellwiki/IO_inside


-- 
Best regards,
 Bulatmailto:bulat.zigans...@gmail.com

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe