Ex 9.9 in Paul Hudak's book

[Ludovic Kuty]

At 10:41 1/04/2002 -0500, Paul Hudak wrote:
>It's really not as obscure as it first seems.  A fixpoint of a function
>foo is a value x such that foo x = x.  The fix operator tells us one way
>(not the only way) to generate such a fixpoint:
>
>  fix foo = foo (fix foo)
>
>Note from this equation that (fix foo) is, by definition (!), a fixpoint
>of foo, since foo (fix foo) is just (fix foo).

Thanks for the explanations.
I still have difficulties to understand the equation but i thought about it
a long time and here are my thoughts.

I consider the following line as a function definition in Haskell:
        fix foo = foo (fix foo)
That is, a simple rule for rewriting the term to the left of the equal sign.
It is Haskell (syntactic), not mathematic (from my point of view which is maybe wrong).

Not all mathematical functions have a fixpoint. So the "fix" function can only
be used with haskell functions that have a fixpoint, and i think those are the ones
that have a base case (for the recursive ones).
So one can think of the fix function as a fixpoint finder (or just searcher if there is no
base case in the recursion).

Generally speaking, if you take any mathematical function that has a fixpoint,
the function "fix" will only lead to the fixpoint if the function converges to the
fixpoint from the chosen start point.

But thanks to the mechanism of lazy evaluation, the argument "(fix foo)"
in "foo (fix foo)" is not evaluated before it is needed, that is, before we know
we are in the inductive case.

The fix function can also be viewed as a way to provide as many
functions as needed. Infinitely many in fact.

I was wondering if i am right or not ?

Ludovic