categories: Re: Computing with Category Theory

[Saul Youssef <youssef@bu.edu>]

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