categories: Re: A request for two references....

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

Steve Stevenson asks for

> 2. Any attempts to develop a computer language/system in which
>     categories are first class citizens.
> 

The constructor calculus is a variant of the lambda-calculus typed using
a functorial type sytem. The functoriality is captured by a program (not
a given constant) 

map : forall m. forall F::m->1, X::m,Y::m. 
	P(X->Y) -> FX -> FY

where F is a functor of m arguments, X and Y are m-tuples of types, P is
the product functor and P(X->Y) represents an m-tuple of functions from
the Xs to the Ys. The calculus supports functors for lists, all sorts of
trees, vectors, matrices, trees of matrices, etc. map can be specialised
to functors of one argument to get

map1 : forall F::1->1, X,Y. (X->Y) -> FX -> FY

or to functors of two arguments to get

map2 : forall F::2->1, X0,X1,Y0,Y1. (X0->Y0) -> (X1->Y1) -> F(X0,X1) ->
F(Y0,Y1)

In a similar way one can define functor-polymorphic functions for
folding, zipping, etc.
and also for numerical operations like

plus : forall X. X -> X -> X

The essentials of the system were presented at Typed Lambda-Calculi and
Applications in May this year (Springer LNCS 2044). A more comprehensive
account is available at 
www-staff.it.uts.edu.au/~cbj/Publications/constructors.ps

Both accounts are written for an audience familiar with polymorphically
typed lambda-calculi. An account for a general audience has yet to be
written (which is why I have not already announced to this list). Let me
add that we have developed a programming language FISh2 which embodies
all of these ideas, and may soon be stable enough for public release. 


Yours,
Barry Jay


-- 
 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