Control.Exception.evaluate - 'correct definition' not so correct
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
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
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
Hello, On Sat, May 3, 2008 at 3:56 AM, apfelmus <apfelmus@quantentunnel.de> 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
On 5/4/08, Iavor Diatchki <iavor.diatchki@gmail.com> 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
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
On Tue, May 6, 2008 at 2:50 AM, apfelmus <apfelmus@quantentunnel.de> 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
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
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@quantentunnel.de> 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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
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@quantentunnel.de> 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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@gmail.com> wrote:
On Tue, May 6, 2008 at 2:50 AM, apfelmus <apfelmus@quantentunnel.de> 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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
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@tcs.inf.tu-dresden.de
participants (10)
-
Abhay Parvate -
apfelmus -
Ariel J. Birnbaum -
Bryan Donlan -
Iavor Diatchki -
Janis Voigtlaender -
Jules Bean -
Lennart Augustsson -
Luke Palmer -
Ryan Ingram