My simple-mindness and naïveté begin to bother me. I begin to get lost,
and I don't know anymore what is the problem...
Greg Woodhouse a écrit:
--- Paul Hudak <[EMAIL PROTECTED]> wrote:
...
The important property of Y is this:
Y f = f (Y f)
Right. This is just a formal statement of the property thaat f fixex Y
f. I'm with you so far.
No, not exactly. This *may be* the *definition* of Y in a typed system
(Haskell). On the other hand you cannot make Y as a self-applying lambda
construct for obvious reasons, and still you can sleep well...
...
Now note that if we define g as (\ones. cons 1 (cons 1 ones)), we
get:
Y g ==> g (Y g) ==> cons 1 (cons 1 (Y g))
Now, this is where things get a little mysterious. Where did g come
from?
I understand that the "x x" om formal definition of Y is what makes
everything work (or, at least I think I do).
Not exactly. Let's do it in Haskell, without this (x x) stuff...
My `g`means something different, though.
fix f = f (fix f) -- Here you have your Y. No typeless lambda.
g f n = n : f n -- This is a generic *non-recursive* `repeat`
ones = fix g 1 -- Guess what.
Now (take 30 ones) works perfectly well. 'ones' is a piece of co-data, or a
co-recursive stream as many people, e.g., David Turner would say. It has
no finite form. Yet, we live happy with, provided we have a normal
reduction scheme (laziness).
Why do you want (in a further posting) to have a "real thing" which for you
means a finite list? Are you sure that everybody needs the LEAST fixed
point? The co-streams give you something different...
Frankly, I don't know what is the issue...
Jerzy Karczmarczuk
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
