[Haskell-cafe] encoding for least fixpoint

[ben]

Hello,

I am trying to understand the definition of (co)inductive types in
Haskell. After reading the beginning of Vene's thesis [1] I was happy,
because I understood the definition of the least fixpoint:

newtype Mu f = In (f (Mu f)).

But this definition coincides with his definition of the greatest fixpoint

newtype Nu f = Wrap (f (Nu f)),

which in reality is not true
(e. g. for
f x = a * x    -- the 'stream functor'
the type Mu f should be empty, isn't it?).

Then I stumbled over a blog entry of Shin-Cheng Mu [2] and from there
over an article of Wadler [3], where the least fixpoint is encoded as

Lfix X. F X  =  All X. (F X -> X) -> X.

and the greatest fixpoint as

Gfix X. F X  =  Exists X. (X -> F X) * X.

I would like to understand these definitions, or get an intuition about
their meaning.
Could somebody give some explanation or a pointer to a place where I can
find one?

Thanks a lot in advance,
ben


[1] http://www.cs.ut.ee/~varmo/papers/thesis.pdf
[2]
http://www.iis.sinica.edu.tw/~scm/2007/encoding-inductive-and-coinductive-types-in-polymorphic-lambda-calculus/
[3]http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt