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 Greg Woodhouse wrote:

--- Lennart Augustsson wrote:

...

What do you mean by represent? It's easy enough to write down the lambda term that is the encoding of [0..].

-- Lennart

You mean like \x -> x ? If I apply it to the Church numeral i, I get i in return. But that hardly seems satisifying because infinite lists seem to be a wholly different type of object.

=== Gregory Woodhouse

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

--Philip Wadler

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Greg Woodhouse wrote:

--- Lennart Augustsson 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

Greg Woodhouse wrote:

Well...think about this way. The function

f i = [1, 1 ..]!!i

is just a constant function expressed in a complicated way. Can I algoritmically determine that f is a constant function?

In general, no. Even in this case I'm pretty sure you'll need induction somewhere.

I suppose the big picture is whether I can embed the theory of finite lists in the theory of infinite lists, preferably in such a way that the isomorphism of the theory "finite lists" with the embedded subtheory is immediately obvious.

I don't think you'll find such an embedding that is "satisfying", i.e., that gives you much insight. Reasoning about total functions on finite lists can be done with sets (and set theory), reasoning about partial functions and/or lazy lists needs domains. An example reverse . reverse = id is true for all finite lists, but not true for any infinite lists (nor any partial lists). (What remains true for all lists is that reverse . reverse <= id where <= is the usual domain ordering.) -- Lennart