categories: Re: Computing with Category Theory

[Barry Jay <cbj@it.uts.edu.au>]

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