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. One strand of the latter approach is to incorporate into programming the use of functors, and their associated operations, like mapping. This began with Charity (Cockett and Fukushima). Since then functors have been represented in Haskell using a type class, have appeared in the type system in Functorial ML (Belle, Jay and Moggi) and most recently the constructor calculus (Jay). In the latter all data structures, including those defined by users, can be represented using a fixed, finite set of constructors, derived from basic categorical concepts. Then polymorphic functions for mapping, folding etc. can be defined by pattern-matching over the basic constructors. Details can be found in my recent paper at Typed Lambda-Calculi and their Applications, or in the technical report at http://www-staff.it.uts.edu.au/~cbj/Publications/constructors.ps. These ideas have been realised in a new language FISh2 currently under development. Yours, Barry Jay Saul Youssef wrote:
Greetings to all,
I'm a big fan of category theory, but doesn't it seem strange that after all this time there is no programming language that let's you organize things around categorical ideas? I've semi-seriously tried to find out about this ( http://physics.bu.edu/~youssef/aldor/aldor.html ) but I basically don't have an answer. I'd be very interested to hear if anyone is working in this direction or comments about why this hasn't happened.
Saul Youssef http://physics.bu.edu/~youssef/
-- Associate Professor C.Barry Jay, Phone: (61 2) 9514 1814 Associate Dean (RPP), Faculty of IT www-staff.it.uts.edu.au/~cbj University of Technology, Sydney. CRICOS Provider 00099F