Re: [Haskell-cafe] Re: Control.Exception.evaluate - 'correct definition' not so correct
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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Control.Exception.evaluate - 'correct definition' not so correct
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 [EMAIL PROTECTED] wrote: On Tue, May 6, 2008 at 2:50 AM, apfelmus [EMAIL PROTECTED] 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 - Band \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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Control.Exception.evaluate - 'correct definition' not so correct
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 [EMAIL PROTECTED] 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 = idfor 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Control.Exception.evaluate - 'correct definition' not so correct
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 [EMAIL PROTECTED] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Control.Exception.evaluate - 'correct definition' not so correct
On 5/4/08, Iavor Diatchki [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Control.Exception.evaluate - 'correct definition' not so correct
Hello, On Sat, May 3, 2008 at 3:56 AM, apfelmus [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Control.Exception.evaluate - 'correct definition' not so correct
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
