strict bits of datatypes

[Robert Dockins]

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