strict bits of datatypes

[Claus Reinke]

    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