[Haskell-cafe] encoding for least fixpoint
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  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  and from there
over an article of Wadler , 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
Could somebody give some explanation or a pointer to a place where I can
Thanks a lot in advance,
More information about the Haskell-Cafe