strict bits of datatypes

[Lennart Augustsson]

So we have an equation
   x = seq x foo
In Haskell recursive equations are solved and you get the smallest  
fix point.
The smallest solution to this equation is x = _|_, there are other  
solutions,
but why should we deviate from giving the smallest fix point for seq  
when we
do it for everything else?

	-- Lennart

On Mar 20, 2007, at 13:53 , 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.
>
> Regards,
>     Malcolm
> _______________________________________________
> Haskell-prime mailing list
> Haskell-prime at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime