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