strict bits of datatypes
robdockins at fastmail.fm
Tue Mar 20 10:50:41 EDT 2007
On Mar 20, 2007, at 9:53 AM, Malcolm Wallace wrote:
> Ian Lynagh <igloo at earth.li> 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
> 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
> 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
> 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
> `seq` does _not_ imply order of evaluation, so the objection is not
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.
Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
More information about the Haskell-prime