[Haskell-cafe] encoding for least fixpoint
dan.doel at gmail.com
Wed Mar 18 03:22:56 EDT 2009
On Tuesday 17 March 2009 7:36:21 pm ben wrote:
> I am trying to understand the definition of (co)inductive types in
> Haskell. After reading the beginning of Vene's thesis  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?).
This is true in a categorical semantics where initial algebras and final
coalbebras are distinct, like in a total language that gets its semantics from
sets and total functions thereon. However, Haskell gets its semantics (modulo
some potential weirdness in IO that people have been discussing lately) from
categories of partial orders and monotone functions. It turns out that you can
show that initial algebras and final coalgebras coincide in such a category,
and so least and greatest fixed points are the same in Haskell (I don't know
how to demonstrate this; my fairly cursory searching hasn't revealed any very
good online references on DCPO categories and algebraic semantics), which is
why there's no distinction in the data declaration (as opposed to, say, Agda).
> Then I stumbled over a blog entry of Shin-Cheng Mu  and from there
> over an article of Wadler , 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?
You can glean some of this from the initial algebra/final coalgebra
definitions of (co)data. The least fixed point Mu F of F is an F-algebra,
which means there's an operation:
in : F (Mu F) -> Mu F
And Mu F is initial in the category of F-algebras, which means that for any
other F-algebra (X, f : F X -> X), there's a unique algebra homomorphism:
cata_f : Mu F -> X
such that: cata_f . in = f . map cata_f. And you can finesse that in Haskell
and with higher order functions and make it:
cata :: forall x. (F x -> x) -> Mu F -> x
And, I suppose, since initial algebras Mu F correspond uniquely with such
parameterized algebra homomorphisms, you're safe in *representing* them as
such, which gives you:
Mu F ~ forall x. (F x -> x) -> x
which is what the Lfix equation gets you above.
In the other case you have final coalgebras Nu F, which come with a coalgebra
out : Nu F -> F (Nu F)
and for any other F-coalgebra (X, f : X -> F X), a unique homomorphism:
ana_f : X -> Nu F
which, parameterizing by f in the same way gets us:
ana :: forall x. (x -> F x) -> x -> Nu F
Which results in a Nu F this time. So suppose we took the definition:
ana = C
for some Haskell constructor C. Well, that means we need a constructor with
the type of ana, and that is exactly the existential:
data Nu f = forall x. C (x -> f x) x -- exists x. (x -> F x) * x
which gets you the Gfix equation above.
I realize some of that was hand-wavey, and maybe someone with more expertise
could flesh it out a bit, but hopefully that helps.
More information about the Haskell-Cafe