[Haskell-cafe] encoding for least fixpoint
ben
benedikt.ahrens at gmx.net
Tue Mar 17 19:36:21 EDT 2009
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
More information about the Haskell-Cafe
mailing list