[Haskell-cafe] I miss OO

Luke Palmer lrpalmer at gmail.com
Thu Dec 3 07:41:34 EST 2009


On Thu, Dec 3, 2009 at 4:09 AM, Peter Verswyvelen <bugfact at gmail.com> wrote:
> 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


More information about the Haskell-Cafe mailing list