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
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
