Re: [Haskell-cafe] Detecting Cycles in Datastructures

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