[Haskell-cafe] Formalizing lazy lists?

Maybe this is old hat, but the question about detecting loops in data structures got me thinking about this. I know you can encode the cons operator (and ordinary lists) in pure lambda calculus, but how could you possibly represent something like [0, 1..]? One thought that occurss to me is to treat it ass a kind of direct limit, but of course, the essence of a structure like this is that the ith entry is computable in a natural way, and it seems that an algebraic limit couldn't really capture this intuition unless we were to introduce some sort of higher order structure (which may be what we want, anyway). === Gregory Woodhouse "Interaction is the mind-body problem of computing." --Philip Wadler