Control.Exception.evaluate - 'correct definition' not so correct

[Bryan Donlan-5]

Hi all,

After some discussion on #haskell I decided to bring this issue to
haskell-cafe. GHC's documentation for Control.Exception.evaluate states:

        evaluate :: a -> IO a

        Forces its argument to be evaluated when the resultant IO action is
        executed. It can be used to order evaluation with respect to other IO
        operations; its semantics are given by

           evaluate x `seq` y    ==>  y
           evaluate x `catch` f  ==>  (return $! x) `catch` f
           evaluate x >>= f      ==>  (return $! x) >>= f

        Note: the first equation implies that (evaluate x) is not the same as
        (return $! x). A correct definition is

           evaluate x = (return $! x) >>= return

However, if >>= is strict on its first argument, then this definition is
no better than (return $! x). One might next consider:

        evaluate x = (return x) >>= (return $!)

However, according to the monad laws, this is equivalent to:

        evaluate x = return $! x

and we're back to where we started. Although GHC's implementation of IO
is somewhat more relaxed about this, there is no guarentee that this
will be the case in all IO implementations, or future versions of GHC,
or different optimization flags, or...

The best I've come up with so far is:

        evaluate x = newIORef (return $! x) >>= join . readIORef

In any case, if >>= is to be guarenteed lazy, this ought to be
documented somewhere (or is it?). Otherwise Control.Exception's docs
should be updated to provide a more correct example and/or the caveat
that >>= must not be left-strict for the example implementation to be
correct.

Thanks,

Bryan Donlan


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

[apfelmus]

Bryan Donlan wrote:
>
>   evaluate x = (return $! x) >>= return
>
> However, if >>= is strict on its first argument, then this definition is
> no better than (return $! x).

According to the monad law

   f >>= return = f

every (>>=) ought to be strict in its first argument, so it indeed seems
that the implementation given in the documentation is wrong.


Regards,
apfelmus

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

[Jules Bean]

apfelmus wrote:

> Bryan Donlan wrote:
>>
>>        evaluate x = (return $! x) >>= return
>>
>> However, if >>= is strict on its first argument, then this definition is
>> no better than (return $! x).
>
> According to the monad law
>
>   f >>= return = f
>
> every (>>=) ought to be strict in its first argument, so it indeed seems
> that the implementation given in the documentation is wrong.

But it is known that the monad laws only apply up to some weaker
equivalence than 'seq-equivalence'.

This has been discussed here countless times by people who understand it
better than me.

As I understand the summary the "=" sign in the monad laws mean
"represent identical actions, in terms of the effects produced and the
result returned". A kind of observational-equivalence for monad
execution, but weaker than direct equational equivalence in the presence
of seq.

(Some people view this as more of a bug in "seq" than in the monad laws)

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

[Iavor Diatchki]

Hello,

On Sat, May 3, 2008 at 3:56 AM, apfelmus <apfelmus@...> wrote:

> Bryan Donlan wrote:
>
> >
> >           evaluate x = (return $! x) >>= return
> >
> > However, if >>= is strict on its first argument, then this definition is
> > no better than (return $! x).
> >
>
>  According to the monad law
>
>   f >>= return = f
>
>  every (>>=) ought to be strict in its first argument, so it indeed seems
> that the implementation given in the documentation is wrong.

>From the monad law we can conclude only that "(>>= return)" is strict,
not (>>=) in general.
For example, (>>=) for the reader monad is not strict in its first argument:

m >>= f = \r -> f (m r) r

So, "(undefined >> return 2) = (return 2)"

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

[Ryan Ingram]

On 5/4/08, Iavor Diatchki <iavor.diatchki@...> wrote:
> >From the monad law we can conclude only that "(>>= return)" is strict,
> not (>>=) in general.
> For example, (>>=) for the reader monad is not strict in its first argument:
>
> m >>= f = \r -> f (m r) r
>
> So, "(undefined >> return 2) = (return 2)"

That's not even true here, though, with regards to seq.

undefined >>= return
= \r -> return (undefined r) r
= \r -> const (undefined r) r
= \r -> undefined r

But

seq undefined 0 = _|_
seq (undefined >>= return) 0
   = seq (\r -> undefined r) 0
   = 0

The monad laws just aren't true for many monads once seq is a possibility.

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

[apfelmus]

Iavor Diatchki wrote:

> apfelmus wrote:
>
>> According to the monad law
>>
>> f >>= return = f
>>
>> every (>>=) ought to be strict in its first argument, so it indeed
>> seems that the implementation given in the documentation is wrong.
>
> From the monad law we can conclude only that "(>>= return)" is
> strict, not (>>=) in general.

Yes, I was too eager :)

> For example, (>>=) for the reader monad is not strict in its first
> argument:
>
> m >>= f = \r -> f (m r) r
>
> So, "(undefined >> return 2) = (return 2)"

In other words, we have

   undefined >>= const (return x) = return x

in the reader monad.


Concerning the folklore that  seq  destroys the monad laws, I would like
to remark that as long as we don't apply  seq  to arguments that are
functions, everything is fine. When  seq  is applied to functions,
already simple laws like

   f . id = f

are trashed, so it's hardly surprising that the monad laws are broken
willy-nilly. That's because  seq  can be used to distinguish between

   _|_ :: A -> B    and   \x -> _|_ :: A -> B

although there shouldn't be a semantic difference between them.


But it's true that in the case of  evaluate , the monad laws are screwed
up. The third equivalence would give

   evaluate _|_ >>= return  ==> (return $! _|_) >>= return
                            ==> _|_ >>= return

and hence

   evaluate _|_ = _|_

which contradicts the first equivalence. In other words, it seems that
in the presence of  evaluate , the monad laws for  IO  are broken if we
allow  seq  on values of type  IO .


Regards,
apfelmus

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

[Luke Palmer-2]

On Tue, May 6, 2008 at 2:50 AM, apfelmus <apfelmus@...> wrote:

>  Concerning the folklore that  seq  destroys the monad laws, I would like
>  to remark that as long as we don't apply  seq  to arguments that are
>  functions, everything is fine. When  seq  is applied to functions,
>  already simple laws like
>
>   f . id = f
>
>  are trashed, so it's hardly surprising that the monad laws are broken
>  willy-nilly. That's because  seq  can be used to distinguish between
>
>   _|_ :: A -> B    and   \x -> _|_ :: A -> B
>
>  although there shouldn't be a semantic difference between them.

It seems that there is a culture developing where people intentionally
ignore the existence of seq when reasoning about Haskell.  Indeed I've
heard many people argue that it shouldn't be in the language as it is
now, that instead it should be a typeclass.

I wonder if it's possible for the compiler to do more aggressive
optimizations if it, too, ignored the existence of seq.  Would it make
it easier to do various sorts of lambda lifting, and would it make
strictness analysis easier?

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

[apfelmus]

Luke Palmer wrote:
> It seems that there is a culture developing where people intentionally
> ignore the existence of seq when reasoning about Haskell.  Indeed I've
> heard many people argue that it shouldn't be in the language as it is
> now, that instead it should be a typeclass.
>
> I wonder if it's possible for the compiler to do more aggressive
> optimizations if it, too, ignored the existence of seq.  Would it make
> it easier to do various sorts of lambda lifting, and would it make
> strictness analysis easier?

The introduction of  seq  has several implications.

The first problem is that parametricity would dictate that the only
functions of type

    forall a,b. a -> b -> b

are

    const id
    const _|_
    _|_

Since  seq  is different from these, giving it this polymorphic type
weakens parametricity. This does have implications for optimizations, in
particular for fusion, see also

   http://www.haskell.org/haskellwiki/Correctness_of_short_cut_fusion

Parametricity can be restored with a class constraint

   seq :: Eval a => a -> b -> b

In fact, that's how Haskell 1.3 and 1.4 did it.


The second problem are function types. With  seq  on functions,
eta-expansion is broken, i.e. we no longer have

   f = \x.f x

because  seq  can be used to distinguish

   _|_  and  \x. _|_

One of the many consequences of this is that simple laws like

   f = f . id

no longer hold, which is a pity.


But then again, _|_ complicates reasoning anyway and we most often
pretend that we are only dealing with total functions. Unsurprisingly,
this usually works. This can even be justified formally to some extend,
see also

  N.A.Danielsson, J.Hughes, P.Jansson, J.Gibbons.
  Fast and Loose Reasoning is Morally Correct.
http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/fast+loose.pdf


Regards,
apfelmus

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

[Abhay Parvate]

Just for curiocity, is there a practically useful computation that uses 'seq' in an essential manner, i.e. apart from the efficiency reasons?

Abhay

On Wed, May 7, 2008 at 2:48 PM, apfelmus <apfelmus@...> wrote:

Luke Palmer wrote:

It seems that there is a culture developing where people intentionally
ignore the existence of seq when reasoning about Haskell.  Indeed I've
heard many people argue that it shouldn't be in the language as it is
now, that instead it should be a typeclass.

I wonder if it's possible for the compiler to do more aggressive
optimizations if it, too, ignored the existence of seq.  Would it make
it easier to do various sorts of lambda lifting, and would it make
strictness analysis easier?

The introduction of  seq  has several implications.

The first problem is that parametricity would dictate that the only functions of type

  forall a,b. a -> b -> b

are

  const id
  const _|_
  _|_

Since  seq  is different from these, giving it this polymorphic type weakens parametricity. This does have implications for optimizations, in particular for fusion, see also

 http://www.haskell.org/haskellwiki/Correctness_of_short_cut_fusion

Parametricity can be restored with a class constraint

 seq :: Eval a => a -> b -> b

In fact, that's how Haskell 1.3 and 1.4 did it.


The second problem are function types. With  seq  on functions, eta-expansion is broken, i.e. we no longer have

 f = \x.f x

because  seq  can be used to distinguish

 _|_  and  \x. _|_

One of the many consequences of this is that simple laws like

 f = f . id

no longer hold, which is a pity.


But then again, _|_ complicates reasoning anyway and we most often pretend that we are only dealing with total functions. Unsurprisingly, this usually works. This can even be justified formally to some extend, see also

 N.A.Danielsson, J.Hughes, P.Jansson, J.Gibbons.
 Fast and Loose Reasoning is Morally Correct.
http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/fast+loose.pdf


Regards,
apfelmus

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

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

[apfelmus]

Abhay Parvate wrote:
> Just for curiocity, is there a practically useful computation that uses
> 'seq' in an essential manner, i.e. apart from the efficiency reasons?

I don't think so because you can always replace  seq  with  const id .
In fact, doing so will get you "more" results, i.e. a computation that
did not terminate may do so now.

In other words, we have

   seq _|_ = _|_
   seq x   = id    for  x > _|_

but

   (const id) _|_ = id
   (const id) x   = id   for  x > _|_

So, (const id) is always more defined (">") than  seq  .


For more about _|_ and the semantic approximation order, see

   http://en.wikibooks.org/wiki/Haskell/Denotational_semantics


Regards,
apfelmus


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

[Abhay Parvate]

Thanks both for the the explanation and the link. The wikibook is really growing fast!

Abhay

On Wed, May 7, 2008 at 5:05 PM, apfelmus <apfelmus@...> wrote:

Abhay Parvate wrote:

Just for curiocity, is there a practically useful computation that uses
'seq' in an essential manner, i.e. apart from the efficiency reasons?

I don't think so because you can always replace  seq  with  const id .
In fact, doing so will get you "more" results, i.e. a computation that
did not terminate may do so now.

In other words, we have

 seq _|_ = _|_
 seq x   = id    for  x > _|_

but

 (const id) _|_ = id
 (const id) x   = id   for  x > _|_

So, (const id) is always more defined (">") than  seq  .


For more about _|_ and the semantic approximation order, see

 http://en.wikibooks.org/wiki/Haskell/Denotational_semantics

Regards,
apfelmus


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

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

[Lennart Augustsson]

GHC already ignores the existence of seq, for instance when doing list fusion.
The unconstrained seq function just ruins too many things.
I say, move seq top a type class (where is used to be), and add an unsafeSeq
for people who want to play dangerously.

  -- Lennart

On Tue, May 6, 2008 at 3:27 PM, Luke Palmer <lrpalmer@...> wrote:

On Tue, May 6, 2008 at 2:50 AM, apfelmus <apfelmus@...> wrote:
>  Concerning the folklore that  seq  destroys the monad laws, I would like
>  to remark that as long as we don't apply  seq  to arguments that are
>  functions, everything is fine. When  seq  is applied to functions,
>  already simple laws like
>
>   f . id = f
>
>  are trashed, so it's hardly surprising that the monad laws are broken
>  willy-nilly. That's because  seq  can be used to distinguish between
>
>   _|_ :: A -> B    and   \x -> _|_ :: A -> B
>
>  although there shouldn't be a semantic difference between them.

It seems that there is a culture developing where people intentionally
ignore the existence of seq when reasoning about Haskell.  Indeed I've
heard many people argue that it shouldn't be in the language as it is
now, that instead it should be a typeclass.

I wonder if it's possible for the compiler to do more aggressive
optimizations if it, too, ignored the existence of seq.  Would it make
it easier to do various sorts of lambda lifting, and would it make
strictness analysis easier?

Luke

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

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

[askyle]

> >  According to the monad law
> >
> >   f >>= return = f
> >
[... snip ...]
>
> So, "(undefined >> return 2) = (return 2)"
>

*scratching head* I don't see how that's a counterexample of the monad law.
Instantiating the law for undefined would IMO yield something like:

(undefined >>= return) = \r -> return (undefined r) r
                                       = \r -> undefined r
                                       = undefined

(considering "undefined" as equivalent to "const undefined", which iirc was
the definition of _|_ for function types).

What am I missing?
--
Ariel J. Birnbaum
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Janis Voigtlaender]

Ariel J. Birnbaum wrote:
> (considering "undefined" as equivalent to "const undefined", which iirc was
> the definition of _|_ for function types).
>  
> What am I missing?

undefined /= const undefined

in Haskell, due to seq.

--
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt@...
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe