[Haskell-cafe] Formalizing lazy lists?

[Greg Woodhouse]

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


===
Gregory Woodhouse  <gregory.woodhouse at sbcglobal.net>


"Interaction is the mind-body problem of computing."

--Philip Wadler