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
On 6/22/11 3:59 PM, Arnaud Bailly wrote: 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