A request for two references....
Good afternoon, I'd like references on these two subjects: 1. The relationship between categories and Martin-Löf types. 2. Any attempts to develop a computer language/system in which categories are first class citizens. Thanks in advance.... best steve
----- Original Message ----- From: "Steve Stevenson" <steve@cs.clemson.edu> To: <categories@mta.ca> Sent: Thursday, August 02, 2001 11:21 AM Subject: categories: A request for two references....
2. Any attempts to develop a computer language/system in which categories are first class citizens.
I do not know whether this is what you are want, but you might consider the IFF Category Theory Ontology -- part of the IFF Foundation Ontology that I am developing. This is logically coded in a new version of KIF [see http://suo.ieee.org/Kent-IFF.pdf]. Robert E. Kent rekent@ontologos.org
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
participants (3)
-
Barry Jay -
Robert E. Kent -
Steve Stevenson