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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
