[Haskell-cafe] encoding for least fixpoint
duncan.coutts at worc.ox.ac.uk
Wed Mar 18 05:28:35 EDT 2009
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  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
More information about the Haskell-Cafe