Re: strict bits of datatypes
On Mon, Mar 19, 2007 at 03:22:29PM +, Simon Peyton-Jones wrote: | This reminds me of something I discovered about using strict fields in | AVL trees (with ghc). Using strict fields results in slower code than | doing the `seq` desugaring by hand. That is bad. Can you send a test case that demonstrates this behaviour? | If I have.. | | data AVL e = E | | N !(AVL e) e !(AVL e) | .. etc | | then presumably this.. | | case avl of N l e r - N (f l) e r | | desugars to something like .. | | case avl of N l e r - let l' = f l | in l' `seq` r `seq` N l' e r | | but IMO it should desugar to.. | | case avl of N l e r - let l' = f l | in l' `seq` N l' e r I agree. If it doesn't please let me know! Although I have not looked into this much, My guess is it is an issue in the simplifier, normally when something is examined with a case statement, the simplification context sets its status to 'NoneOf []', which means we know it is in WHNF, but we don't have any more info about it. I would think that the solution would be to add the same annotation in the simplifier to variables bound by pattern matching on strict data types? Just a theory. I am not sure how to debug this in ghc without digging into it's code. John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: strict bits of datatypes
On Mar 20, 2007, at 9:53 AM, Malcolm Wallace wrote: Ian Lynagh [EMAIL PROTECTED] wrote: data Fin a = FinCons a !(Fin a) | FinNil w = let q = FinCons 3 q in case q of FinCons i _ - i is w 3 or _|_? Knowing that opinions seem to be heavily stacked against my interpretation, nevertheless I'd like to try one more attempt at persuasion. The Haskell Report's definition of `seq` does _not_ imply an order of evaluation. Rather, it is a strictness annotation. (Whether this is the right thing to do is another cause of dissent, but let's accept the Report as is for now.) So `seq` merely gives a hint to the compiler that the value of its first argument must be established to be non-bottom, by the time that its second argument is examined by the calling context. The compiler is free to implement that guarantee in any way it pleases. So just as, in the expression x `seq` x one can immediately see that, if the second x is demanded, then the first one is also demanded, thus the `seq` can be elided - it is semantically identical to simply x Now, in the definition x = x `seq` foo one can also make the argument that, if the value of x (on the lhs of the defn) is demanded, then of course the x on the rhs of the defn is also demanded. There is no need for the `seq` here either. Semantically, the definition is equivalent to x = foo I am arguing that, as a general rule, eliding the `seq` in such a case is an entirely valid and correct transformation. The objection to this point of view is that if you have a definition x = x `seq` foo then, operationally, you have a loop, because to evaluate x, one must first evaluate x before evaluating foo. But as I said at the beginning, `seq` does _not_ imply order of evaluation, so the objection is not well-founded. I just want to say that the argument I find most convincing is the 'least fixpoint' argument, which does not at all require assumptions about order of evaluation. I see your arguments as something along the lines the non-bottom answer is a fixpoint of the equations, and therefore it is the correct answer. And, it is in fact _a_ fixpoint; but it is not the _least_ fixpoint, which would be bottom. To recap, the equation in question is: q = seq q (RealFinCons 3 q) It is not hard to see that q := _|_ is a fixpoint. Also, we have that q := LUB( _|_, RealFinCons 3 _|_, RealFinCons 3 (RealFinCons 3 _|_), ... ) is a fixpoint and is _|_. But that doesn't matter since _|_ is the least element of the domain and must therefore be the least fixpoint. Regards, Malcolm Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: strict bits of datatypes
Malcolm wrote: The Haskell Report's definition of `seq` does _not_ imply an order of evaluation. Rather, it is a strictness annotation. That is an important point. Now, in the definition x = x `seq` foo one can also make the argument that, if the value of x (on the lhs of the defn) is demanded, then of course the x on the rhs of the defn is also demanded. There is no need for the `seq` here either. Semantically, the definition is equivalent to x = foo I am arguing that, as a general rule, eliding the `seq` in such a case is an entirely valid and correct transformation. I think it is possible that both camps are right on this issue, as far as Haskell 98 stands. We can translate the definition of x into: x = fix (\y - seq y foo) Isn't it the case that, denotationally, _|_ and foo are valid interpretations of the rhs? If we want to choose between them then we need something extra, such as an operational semantics, or a rule saying that we prefer the least solution. Perhaps I am just re-stating what Ian wrote in the beginning :) Cheers, Bernie. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: strict bits of datatypes
Simon Peyton-Jones wrote: | strict fields have no effect on deconstructing data types. That's GHC's behaviour too. I think it's the right one too! (It's certainly easy to explain.) This reminds me of something I discovered about using strict fields in AVL trees (with ghc). Using strict fields results in slower code than doing the `seq` desugaring by hand. If I have.. data AVL e = E | N !(AVL e) e !(AVL e) .. etc then presumably this.. case avl of N l e r - N (f l) e r desugars to something like .. case avl of N l e r - let l' = f l in l' `seq` r `seq` N l' e r but IMO it should desugar to.. case avl of N l e r - let l' = f l in l' `seq` N l' e r which is what I ended up writing by hand all over the place (dropping the strictness annotation in the data type). That is, variables that have been obtained by matching strict fields (r in the case) should not be re-seqed if they are re-used in another strict context. Now this explanation for the slow down I observed is just speculation on my part (I don't actually know what ghc or any other compiler does). But on modern memory architectures, forcing the code to inspect heap records that it shouldn't have to inspect will be a bad thing. So semantically I agree with strict fields have no effect on deconstructing data types, but they should have an effect on the code that an optimising compiler generates IMO. Regards -- Adrian Hey ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: strict bits of datatypes
| This reminds me of something I discovered about using strict fields in | AVL trees (with ghc). Using strict fields results in slower code than | doing the `seq` desugaring by hand. That is bad. Can you send a test case that demonstrates this behaviour? | If I have.. | | data AVL e = E | | N !(AVL e) e !(AVL e) | .. etc | | then presumably this.. | | case avl of N l e r - N (f l) e r | | desugars to something like .. | | case avl of N l e r - let l' = f l | in l' `seq` r `seq` N l' e r | | but IMO it should desugar to.. | | case avl of N l e r - let l' = f l | in l' `seq` N l' e r I agree. If it doesn't please let me know! Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: strict bits of datatypes
[EMAIL PROTECTED] writes: Jón Fairbairn wrote: [EMAIL PROTECTED] writes: Besides, having let q = FinCons 3 q in q not being _|_ crucially depends on memoization. Does it? PS: Your derivations are fine in the case of a non-strict FinCons. But the point is to make in strict. Yes, I was trying to be subtle but was too sleepy and lost the plot. -- Jón Fairbairn [EMAIL PROTECTED] ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
strict bits of datatypes
Hi all, A while ago there was a discussion on haskell-cafe about the semantics of strict bits in datatypes that never reached a conclusion; I've checked with Malcolm and there is still disagreement about the right answer. The original thread is around here: http://www.haskell.org/pipermail/haskell-cafe/2006-October/018804.html but I will try to give all the relevant information in this message. The question is, given: data Fin a = FinCons a !(Fin a) | FinNil w = let q = FinCons 3 q in case q of FinCons i _ - i is w 3 or _|_? -- The _|_ argument -- (Supporters include me, ghc and hugs) q = FinCons 3 q === (by Haskell 98 report 4.2.1/Strictness Flags/Translation q = (FinCons $ 3) $! q === (by definition of $, $!) q = q `seq` FinCons 3 q === (solution is least fixed point of the equation) q = _|_ Thus w = case _|_ of FinCons i _ - i so w = _|_. -- The 3 argument -- (Supporters include Malcolm Wallace, nhc98 and yhc) Here I will just quote what Malcolm said in his original message: The definition of seq is seq _|_ b = _|_ seq a b = b, if a/= _|_ In the circular expression let q = FinCons 3 q in q it is clear that the second component of the FinCons constructor is not _|_ (it has at least a FinCons constructor), and therefore it does not matter what its full unfolding is. and in his recent e-mail to me: Yes, I still think this is a reasonable interpretation of the Report. I would phrase it as After evaluating the constructor expression to WHNF, any strict fields contained in it are also be guaranteed to be in WHNF. This also makes q a fixpoint of q = q `seq` FinCons 3 q, but not the least fixed point. -- So I think it would be good if we can all agree on what the meaning should be, and then to clarify the wording in the report so that future readers understand it correctly too. Thanks Ian ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: strict bits of datatypes
On Fri, Mar 16, 2007 at 05:40:17PM +0100, [EMAIL PROTECTED] wrote: The translation q = FinCons 3 q === (by Haskell 98 report 4.2.1/Strictness Flags/Translation q = (FinCons $ 3) $! q is rather subtle: the first FinCons is a strict constructor whereas the second is the real constructor. In other words, the translation loops as we could (should?) apply FinCons = \x y - FinCons x $! y = \x y - (\x' y' - FinCons x' $! y') x $! y = ... ad infinitum. Yes, perhaps that ought to be fixed. But even so, this clearly implies that FinCons 3 _|_ = _|_ and thus that q is _|_ and nhc98/yhc have a bug. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
