# strict bits of datatypes

Claus Reinke claus.reinke at talk21.com
Tue Mar 20 11:37:16 EDT 2007

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

```

More information about the Haskell-prime mailing list