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