Hi Barry & Phil, Thanks for the answers. I knew about Charity and ML but not Fish & Fish2 or CAML (the word "category" does not appear on either the Fish or CAML web pages!). Barry Jay wrote:
Dear Saul,
I can envisage at least two distinct ways of computing with categories. One is for category theorists to use computers to do their calculation or perhaps even provide formal proofs of theorems. The second is to use ideas from category theory as a guide to the design of programming languages. For example, the use of monads to control computational effects.
I didn't explain what I'm interested in very well, but I don't think that it's either of your distinct ways above. I'm not thinking about automatic diagram chasing or proof assistance or something like that. I'm also don't have in mind regular functional languages that are defined using category theory (although I can see that these things are quite neat). Maybe it's best if I put it this way. There are lots of people around doing mathematical software in, say, C++, Maple or Mathematica or home grown systems. These systems are fine for, say, defining integers or functions or vector spaces or groups, but are essentially hopeless for categories, functors, adjoints, etc. Even the most basic constructions of category theory are very awkward to deal with at best. This, it seems to me, is a crippling limitation of these systems compared to what would be possible if you could only define categories and functors with the ease that you define matrices and functions. I guess I'm asking for a language where you could mix "regular math stuff" and category theory with ease as is done in mathematics on paper. A language or system suitable for writing large general purpose math libraries, say, that use category theory concepts at least as the high level organizing principles. Wouldn't that be nice? This wasn't a problem before, but now that I know some category theory, it pains me greatly! I also find it strange that this isn't a big priority, in, for instance, the CS community. I'll have a look at your technical report too. Cheers, Saul Youssef