Malcolm Wallace | 7 May 12:13 2007
Picon

Re: The Proper Definition of (evaluate :: a -> IO a)

Isaac Dupree <isaacdupree <at> charter.net> wrote:

> The obvious "evaluate x = x `seq` return x" fails one of the following
> laws for evaluate:
> 
> evaluate x `seq` y    ==>  y

I'm not sure why anyone thinks this "law" should hold, since it
completely changes the known semantics of `seq`.  A more accurate law
would be:

  evaluate x `seq` y    ==>  if x==_|_ then _|_ else y

Where did you find the erroneous version?

Regards,
    Malcolm
Nils Anders Danielsson | 7 May 17:19 2007
Picon
Picon

Re: The Proper Definition of (evaluate :: a -> IO a)

On Mon, 07 May 2007, Malcolm Wallace <Malcolm.Wallace <at> cs.york.ac.uk> wrote:

> Isaac Dupree <isaacdupree <at> charter.net> wrote:
>
>> The obvious "evaluate x = x `seq` return x" fails one of the following
>> laws for evaluate:
>> 
>> evaluate x `seq` y    ==>  y
>
> I'm not sure why anyone thinks this "law" should hold, since it
> completely changes the known semantics of `seq`.  A more accurate law
> would be:
>
>   evaluate x `seq` y    ==>  if x==_|_ then _|_ else y

You seem to be assuming that evaluate ⊥ = ⊥, which is not necessarily
the case.

> Where did you find the erroneous version?

Presumably he found it by reading the documentation for evaluate:

  http://haskell.org/ghc/docs/latest/html/libraries/base/Control-Exception.html#7

--

-- 
/NAD
Malcolm Wallace | 7 May 18:54 2007
Picon

Re: The Proper Definition of (evaluate :: a -> IO a)

Nils Anders Danielsson <nad <at> cs.chalmers.se> wrote:

> > Where did you find the erroneous version?
> Presumably he found it by reading the documentation for evaluate:
>   http://haskell.org/ghc/docs/latest/html/libraries/base/Control-Exception.html#7

Actually, I checked the source code for Control.Exception before asking
the question, and those laws definitely do not appear there.  So now I'm
kind of puzzled as to how Haddock managed to generate documentation for
them!

> >> evaluate x `seq` y    ==>  y
> >
> > I'm not sure why anyone thinks this "law" should hold,
> 
> You seem to be assuming that evaluate x = x, which is not
> necessarily the case.

Yes, I did make a mistake when I asked the question, in assuming some
intuitive semantics rather than the actually written ones.  So taking
the law at face value, it seems to say that 'evaluate' is supposed to
force its argument, yet the result should be guaranteed to be in WHNF,
even if the argument was in fact undefined.  Given that the result is in
the IO monad, it can only mean one of two things:

  (1) That 'evaluate' should _not_ force its argument when it is called,
      but that rather that the argument should be forced only when the
      resultant IO action is executed.  This conflicts with the
      documentation, which implies that the argument is forced _before_
      the IO action is created or executed.  But I guess this semantics
(Continue reading)

Isaac Dupree | 8 May 00:57 2007
Picon

Re: The Proper Definition of (evaluate :: a -> IO a)


Malcolm Wallace wrote:
> Nils Anders Danielsson <nad <at> cs.chalmers.se> wrote:
> 
>>> Where did you find the erroneous version?
>> Presumably he found it by reading the documentation for evaluate:
>>   http://haskell.org/ghc/docs/latest/html/libraries/base/Control-Exception.html#7
> 
> Actually, I checked the source code for Control.Exception before asking
> the question, and those laws definitely do not appear there.  So now I'm
> kind of puzzled as to how Haddock managed to generate documentation for
> them!

In the source code, grep found it at the end of
libraries/base/GHC/Exception.lhs

>   (1) That 'evaluate' should _not_ force its argument when it is called,
>       but that rather that the argument should be forced only when the
>       resultant IO action is executed.  This conflicts with the
>       documentation, which implies that the argument is forced _before_
>       the IO action is created or executed.

I didn't think so... though in most cases the IO action is only
scrutinized/created in order to immediately execute it.

> But I guess this semantics
>       accords with Isaac's suggested definition:
>           evaluate x = (x `seq` return x) >>= return

I think evaluate's non-strictness until the IO is executed
(Continue reading)

Stefan O'Rear | 8 May 01:11 2007
Picon
Picon

Re: The Proper Definition of (evaluate :: a -> IO a)

On Mon, May 07, 2007 at 06:57:51PM -0400, Isaac Dupree wrote:
> Malcolm Wallace wrote:
> > But I guess this semantics
> >       accords with Isaac's suggested definition:
> >           evaluate x = (x `seq` return x) >>= return

Let's try a little Equational Reasoning:

evaluate x = (x `seq` return x) >>= return

evaluate x = (>>=) (seq x (return x)) return

evaluate x = bindIO (seq x (returnIO x)) returnIO

evaluate x = IO (\st1 -> case unIO (seq x (returnIO x)) st1 of (# st2, a #) -> unIO (returnIO a) st2)

evaluate x = IO (\st1 -> case unIO (seq x (returnIO x)) st1 of (# st2, a #) -> (# st2, a #))

evaluate x = IO (\st1 -> case seq x (\st3 -> (# st3, x #)) st1 of (# st2, a #) -> (# st2, a #))

evaluate x = IO (\st1 -> case (case x of __DEFAULT -> (\st3 -> (# st3, x #))) st1 of (# st2, a #) -> (# st2, a #))

evaluate x = IO (\st1 -> case x of __DEFAULT -> case (\st3 -> (# st3, x #)) st1 of (# st2, a #) -> (# st2, a #))

evaluate x = IO (\st1 -> case x of __DEFAULT -> case (# st1, x #) of (# st2, a #) -> (# st2, a #))

evaluate x = IO (\st1 -> case x of __DEFAULT -> (# st1, x #))

evaluate x = IO (\st1 -> case x `seq` () of () -> (# st1, x #))

(Continue reading)

Simon Marlow | 8 May 10:12 2007
Picon

Re: The Proper Definition of (evaluate :: a -> IO a)

Malcolm Wallace wrote:
> Nils Anders Danielsson <nad <at> cs.chalmers.se> wrote:
> 
>>> Where did you find the erroneous version?
>> Presumably he found it by reading the documentation for evaluate:
>>   http://haskell.org/ghc/docs/latest/html/libraries/base/Control-Exception.html#7
> 
> Actually, I checked the source code for Control.Exception before asking
> the question, and those laws definitely do not appear there.  So now I'm
> kind of puzzled as to how Haddock managed to generate documentation for
> them!
> 
>>>> evaluate x `seq` y    ==>  y
>>> I'm not sure why anyone thinks this "law" should hold,
>> You seem to be assuming that evaluate x = x, which is not
>> necessarily the case.
> 
> Yes, I did make a mistake when I asked the question, in assuming some
> intuitive semantics rather than the actually written ones.  So taking
> the law at face value, it seems to say that 'evaluate' is supposed to
> force its argument, yet the result should be guaranteed to be in WHNF,
> even if the argument was in fact undefined.  Given that the result is in
> the IO monad, it can only mean one of two things:
> 
>   (1) That 'evaluate' should _not_ force its argument when it is called,
>       but that rather that the argument should be forced only when the
>       resultant IO action is executed.  This conflicts with the
>       documentation, which implies that the argument is forced _before_
>       the IO action is created or executed.  But I guess this semantics
>       accords with Isaac's suggested definition:
(Continue reading)

Ashley Yakeley | 9 May 02:47 2007

Re: The Proper Definition of (evaluate :: a -> IO a)

Simon Marlow wrote:
> That's exactly right.  Evaluate was introduced because it does something 
> different from (return $!).  We tried in the documentation to be clear 
> about its semantics, but perhaps we weren't clear enough.  I'll add 
> Isaac's suggested definition to the docs.

If Isaac's definition is accurate, we might as well generalise it to any 
Monad.

--

-- 
Ashley Yakeley
Stefan O'Rear | 9 May 02:50 2007
Picon
Picon

Re: The Proper Definition of (evaluate :: a -> IO a)

On Tue, May 08, 2007 at 05:47:27PM -0700, Ashley Yakeley wrote:
> Simon Marlow wrote:
> >That's exactly right.  Evaluate was introduced because it does something 
> >different from (return $!).  We tried in the documentation to be clear 
> >about its semantics, but perhaps we weren't clear enough.  I'll add 
> >Isaac's suggested definition to the docs.
> 
> If Isaac's definition is accurate, we might as well generalise it to any 
> Monad.

Isaac's definition is equivalent to the standard evaluate as I proved.
However, my proof could be using misfeatures of IO.

Stefan
Isaac Dupree | 10 May 22:51 2007
Picon

Re: The Proper Definition of (evaluate :: a -> IO a)


Stefan O'Rear wrote:
> On Tue, May 08, 2007 at 05:47:27PM -0700, Ashley Yakeley wrote:
>> If Isaac's definition is accurate, we might as well generalise it to any 
>> Monad.
> 
> Isaac's definition is equivalent to the standard evaluate as I proved.
> However, my proof could be using misfeatures of IO.

Monads like Maybe and [] have no definition of evaluate consistent with
all the laws, they only have (return) and (return $!) as distinct
possibilities. In which case my definition makes evaluate in those
monads be equivalent to (return $!).  Which might not be that bad.  For
monads such as Lazy ST, it is clear that (>>=) cannot be strict in its
first argument in order for the laziness to work, so evaluate can be
defined with all the laws.  In other function-based monads - including
IO - it is not so documented or necessary.

What is evaluate used for? Based on Google codesearch and my own
experiences:

In a forkIO for the sole purpose of parallel evaluation.  Could be
summarized by:
  forkEvaluate :: a -> IO a
  forkEvaluate a = forkIO (evaluate a >> return ())
Aren't there supposed to be more functional ways like `par` to achieve
this? Anyway, looks like that definition only works in the IO monad.

To immediately catch exceptions from it (Control.Exception.catch or
try).  This also only works in the IO monad (or derived monads that can
(Continue reading)


Gmane