[Haskell-cafe] encoding for least fixpoint

[Wouter Swierstra]

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