[Haskell-cafe] encoding for least fixpoint

[Dan Doel]

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 [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?).

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 [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?

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 
operation:

  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.

Cheers,
-- Dan