[Haskell-cafe] Category theory as a design tool

[wren ng thornton]

On 6/22/11 3:59 PM, Arnaud Bailly wrote:
> Hello Greg and Alexander,
> Thanks for your replies. Funnily, I happen to own the 3 books you
mentionned
> :-) My interest in category theory is a long standing affair...
>
> Note that owning a book, having read (most of) it and knowing a theory (or
> at least its principles and main concepts) is really quite a different
thing
> from being able to apply it.

One of the big benefits I see to using category theory for dealing with
programming languages comes from using CT as a generalized logic for
equational reasoning. In particular, making use of the ideas of (co)limits
and adjunctions in order to prove that something must behave in a
particular way. This requires a bit of work to contort your thinking into
the patterns of CT, but it means that once you can prove that something is
a foo, then all the theorems about foos will apply.

Just having a diagram and knowing it commutes doesn't tell you a whole
lot, it just says that one particular equation holds. The real power comes
from looking at diagrams that are parametric (since then proving it holds
will mean it holds for all parameter valuations), or looking at diagrams
where one of the arrows is (essentially) unique (since then you can show
things that look like foos actually are foos). That is, the real power of
diagrams comes from the quantifiers, which are explained in the text
rather than shown in the diagram itself.

As an example of this approach, see my comments in the thread about
anonymous sum types. For something to be a product means that a particular
diagram commutes: namely, a product is the limit of the two point category
(and coproducts are the colimit). One of the many things this tells us is
that if we posit that A*A ~ A in a category that "has products", we must
infer that the category is a meet-(pre)semilattice[1].


[1] Or a really goofy structure where for every A and B there are at most
two A->B, with a canonical way of distinguishing them. Of course, for this
to be a category we need to define a composition operator, which will take
the four compositions into the two possible arrows, which is where it gets
strange.

-- 
Live well,
~wren