On Fri, Mar 16, 2007 at 05:00:15PM +0000, Jón Fairbairn wrote:

Does it? Mentally I translate that as

let q = Y (\q -> FinCons 3 q) in q

but it would actually translate to

let q = Y (\q -> q `seq` FinCons 3 q) in q

for strict fields, whenever a constructor appears, it is translated to one which seq's its strict fields before creating the constructor. so, FinCons 3 q desugars to q `seq` FinCons 3 q wherever it appears, strict fields have no effect on deconstructing data types. John -- John Meacham - ⑆repetae.net⑆john⑈

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

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?

OK, I'll try to put something reasonably simple together to test this again. Last time I tested it was a probably a couple of years ago so what I said might not be true of current ghc. The effect wasn't huge in any case (using strict constructors was about 5% slower). Regards -- Adrian Hey

| 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? Indeed! GHC already does this. That's why I am surprised that adding seq improves things. Adrian has helpfully sent a test case, but I have not examined it yet S

apfelmus@quantentunnel.de writes:

...

apfelmus@quantentunnel.de 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

Jón Fairbairn wrote: 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 Jon.Fairbairn@cl.cam.ac.uk

Hello, I also think that the first version is the correct one (i.e., the result is _|_). -Iavor On 3/16/07, Ross Paterson wrote:

On Fri, Mar 16, 2007 at 05:40:17PM +0100, apfelmus@quantentunnel.de 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

On Mar 20, 2007, at 9:53 AM, Malcolm Wallace wrote:

Ian Lynagh 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

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.

x `seq` x === x and so x = x `seq` x === x = x but, in general, x = x `seq` foo =/= x = foo consider x = x `seq` ((1:) x) x = x `seq` ((1:) (x `seq` ((1:) x))) x = x `seq` ((1:) (x `seq` ((1:) (x `seq` ((1:) x))))) .. ignoring evaluation order, partially unrolling/substituting x also unrolls/substitutes applications of seq (in proper call-by-need, we couldn't even do the substitution until after the evaluation, so we'd never get this far). no part of the right-hand side is defined unless x is - that is what seq is about, isn't it? i do like the argument about different fixpoints - does that correspond to inductive vs coinductive definitions which are so often mixed in haskell? when working with cyclic structures, we often are quite happy without a base case. so instead of the inductive f 0 = True f n = f (n-1) -- provided that (f (n-1)) is defined, (f n) is defined we have things like nats = 1:map (+1) nats -- nats is partially defined if we just assume that nats is partially defined and it is nice to have both available, if not all that well separated. whether we're talking co-recursion or recursion seems to depend entirely on whether the recursive references are in a non-strict or strict context (so that the definitions are productive or not). so it seems to me that adding seq to a (co-)recursion is precisely about resolving this ambiguity and forcing induction nats = (1:) $! map (+1) nats -- nats is defined if we can prove that nats is defined, which we can't anymore and saying that we can get back to co-induction by eliding the seq may be correct, but irrelevant. and the same reasoning ought to apply to strict fields in data constructors. sorry for waving about precisely defined terms in such a naive manner. i hope it helps, and isn't too far of the mark!-) claus

On Tue, Mar 20, 2007 at 01:53:47PM +0000, Malcolm Wallace wrote:

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.

You're talking about demand, WHNF, etc, but the Report doesn't; it gives a simple denotational semantics for seq and recursive definitions, according to which the first definition is equivalent to x = _|_.