Hi Ben,
But this definition coincides with his definition of the greatest fixpoint
In Haskell the least and greatest fixed points coincide. (Categorically, this is called "algebraically compact" I think). You can still "fake" coinductive types to some degree by consistently using unfolds rather than folds.
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.
So here's my attempt at an explanation. For every least fixed point of a functor: data Mu f = In (f (Mu f)) you can define a fold: fold :: forall a . (f a -> a) -> Mu f -> a fold algebra (In t) = algebra (fmap (fold algebra) t) Now your definition of Lfix above basically identifies the data type with all possible folds over it. (I suspect you will need some parametricity result to show that this is really an isomorphism) For codata, instead of having a fold you get an unfold: unfold :: forall a . (a -> f a) -> a -> Nu f unfold coalg x = In (fmap (unfold coalg) (g x)) And your Gfix type above identifies every codata type with its unfold. To see this, you need to realise that: forall a . (a -> f a) -> a -> Nu f is isomorphic to: forall a . (a -> f a , a) -> Nu f is isomporphic to: (exists a . (a -> f a, a)) -> Nu f which gives you one direction of the iso. Now in case you think this is all airy-fairy category theory, there's a really nice paper "Stream fusion: from lists to streams to nothing at all" that shows how to use this technology to get some serious speedups over all kinds of list-processing functions. Hope this helps, Wouter