On Thu, Dec 3, 2009 at 4:09 AM, Peter Verswyvelen
Also Luke Palmer talked a couple of times about "co-algebraic" approaches, but not being a computer scientist, I never really understood what that meant ("just reverse all the arrows"?)
Disclaimer: I am not a category theorist. I think my intuition matches the terminology pretty well, but I would like to see someone who knows what they are talking about elaborate or correct me. The way I use the term, a coalgebraic data type is still very much functional in nature. Here's how I see it: An initial algebra focuses on the constructors. You see: data Nat = Zero | Succ !Nat Notice Zero :: Nat, Succ :: Nat -> Nat. We say that Nat is the smallest data type that supports both of those constructrs (because of Haskell's laziness, if I hadn't put the ! there, it wouldn't be the least). When you want to construct one, you use one of the constructors (because it is by def. just large enough to have those) When you want to destruct one, i.e. write a function f :: Nat -> A for some A, you say "well it had to have been made with Zero or Succ", so you pattern match on Zero and pattern match on Succ. A final coalgebra focuses on the projections. You might see: data Conat = Conat { proj :: Either () Conat } So proj :: Conat -> Either () Conat. But we can't say that it's the smallest data type that supports that projection, because that is a very small data type (it always projects to ()). Rather it is the *largest* data type that still supports that projection. When you want to destruct one, you just use one of the projection, because it is by def. still small enough to always have them. When you want to construct one, it is enough to specify the values for each of the projections, because the data type is large enough to hold any (well-defined) projection you can think of. See the dualities? The difference between Nat and Conat is that Conat has one additional element, fix (Conat . Right). Technically all the lazy data types are final coalgebras (just stated with focus on the constructors), because they have these infinite elements, but it is convenient to pretend that they don't sometimes. But go to any of the popular total dependently-typed languages and there are some differences (one of those differences being that none of them get final coalgebras right[1]). Luke [1] Conor McBride. Let's see how things unfold. http://strictlypositive.org/ObsCoin.pdf