Re: Computing with Category Theory
Dear Saul: There are several category-based programming languages, but they may be a bit hard to find on first glance. Here are three that come to mind, but I'm sure you will hear about more: 1. The most famous is CAML, which stands for Categorical Abstract Machine Language, and is a variant of ML, a well-known and robust polymorphic functional language. The original implementations arose from work on categorical combinators, but now is an autonomous programming language by itself. http://caml.inria.fr/ 2. Two category theorists who have developped programming languages are: (i) Robin Cockett, with his language Charity: http://www.cpsc.ucalgary.ca/Research/charity/home.html (ii) Barry Jay, with his language FISh: http://www-staff.it.uts.edu.au/~cbj/FISh/ Philip Scott Dept. of Math & Stats U. Ottawa
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/
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
Saul, We've applied The Kestrel Institute's Specware package, which implements category-theoric constructs to derive software from knowledge structures. We've demonstrated that we can generate engineering design software. We've also applied Specware in an investigation of mathematically-defined ontologies as a language-neutral knowledge repository for knowledge-based systems. Some references to our work are [1] Unpublished paper describing systems synthesis (written by my colleague Keith Williamson), which can be found in the following page: http://www.kestrel.edu/home/techtransfer.html [2] Applied research with Specware in an industrial setting: K. Williamson, M. Healy and R. Barker (2001) "Industrial Applications of Software Synthesis via Category Theory-Case Studies Using Specware", Journal of Automated Software Engineering, vol. 8, no. 1, pp. 7-30. K. Williamson and M. Healy (2000) "Deriving engineering software from requirements", Journal of Intelligent Manufacturing, vol. 11, no. 1, pp. 3-28. M. Healy and K. Williamson (2000) "Applying Category Theory to Derive Engineering Software from Encoded Knowledge" (Invited Paper), in G. Goos, J. Hartmanis and J. van Leeuwen, ed., Algebraic Methodology and Software Technology, 8th International Conference, AMAST 2000, Iowa City, Iowa, USA, May 2000, Proceedings. Lecture Notes in Computer Science, Springer-Verlag:New York. pp. 484-498. Regards, Mike
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/
-- =========================================================================== e Michael J. Healy A FA ----------> GA (425)865-3123 | | FAX(425)865-2964 | | Ff | | Gf c/o The Boeing Company | | PO Box 3707 MS 7L-66 \|/ \|/ Seattle, WA 98124-2207 ' ' USA FB ----------> GB -or for priority mail- e "I'm a natural man." 2760 160th Ave SE MS 7L-66 B Bellevue, WA 98008 USA michael.j.healy@boeing.com -or- mjhealy@u.washington.edu ============================================================================
On Thu, 1 Nov 2001, 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.
This is actually quite feasible using existing tools. For instance, that we don't need to put the existence of exponentials in the definition of a topos (i.e. a terminal object, subobject classifier, power objects, and pullbacks suffice to construct exponentials) can be proved formally. see http://functor.org/math/cd01.ps. ---Jason
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
participants (5)
-
Barry Jay -
Jason C Reed -
mjhealy＠redwood.rt.cs.boeing.com -
Phil Scott -
Saul Youssef