[Haskell-cafe] Formalizing lazy lists?

[Lennart Augustsson]

Greg Woodhouse wrote:
> 
> --- Lennart Augustsson <lennart at augustsson.net> wrote:
> 
> 
>>How about:
>>
>>nil = \ n c . n
>>cons x xs = \ n c . c x xs
>>
>>zero = \ z s . z
>>suc n = \ z s . s n
>>
>>listFromZero = Y ( \ from n . cons n (from (suc n))) zero
>>
>>(Untested, so I might have some mistake.)
>>
>>	-- Lennart
>>
> 
> 
> Okay, I see what you mean here. What I was thinking is that repeatedly
> unfolding Y give us kind of an algorithm to extract initial segments of
> the list (like "from"), but there's something disquieting about all of
> this.

Unfolding Y is indeed part of the algorithm to generate the list.
The lambda calculus is "just" another programming language, so
why does this disturb you?


  Maybe it's just my lack of familiarity with lambda calculus, but
> I think one thing I got used to as a student was the idea that if I
> started peeling back layers from an abstract defintion or theorem, I'd
> end up with something that looked familiar. Now, to me a list
> comprehension is something like an iterative recipe. Maybe [0, 1, ..]
> is something "primitive" that can only really be understood
> recursively, and then a comprehension like
> 
> [ x*x | x <- [0, 1..] ]
> 
> is something easily built from that (or itself defined as a fixed
> point), but it would be nice to see the iterative recipe somehow "fall
> out" of the more formal definition in terms of Y.

List comprehensions are just a different way of writing concats
and maps, both of which have recursive definitions.

What is an "iterative recipe"?

	-- Lennart