[Haskell-cafe] encoding for least fixpoint

[Duncan Coutts]

On Wed, 2009-03-18 at 03:22 -0400, Dan Doel wrote:
> 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).

You can explain it to yourself (not a proof) by writing out the example
for lists and co-lists along with fold for the list and unfold function
for the co-list. Then write conversion functions between them. You can
go from lists to co-lists using fold or unfold, but going from co-list
to list requires general recursion. And that's the key of course. In
Agda or something that distinguishes inductive and co-inductive types
you could do the first two conversions but not the conversion in the
other direction.

Duncan