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-ty... [3]http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt