strict bits of datatypes
Lennart Augustsson
lennart at augustsson.net
Tue Mar 20 16:25:12 EDT 2007
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
More information about the Haskell-prime
mailing list