[Haskell-cafe] encoding for least fixpoint

ben benedikt.ahrens at gmx.net
Tue Mar 17 19:36:21 EDT 2009


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,

[1] http://www.cs.ut.ee/~varmo/papers/thesis.pdf

More information about the Haskell-Cafe mailing list