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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
