A Categorical Programming Language
http://www.tom.sfc.keio.ac.jp/~hagino/thesis.pdf
by Tatsuya Hagino
http://www.tom.sfc.keio.ac.jp/~hagino/index.html.en
Abstract: A theory of data types and a programming language based on category theory are presented.
Data types play a crucial role in programming. They enable us to write programs easily and elegantly. Various programming languages have been developed, each of which may use different kinds of data types. Therefore, it becomes important to organize data types systematically so that we can understand the relationship between one data type and another and investigate future directions which lead us to discover exciting new data types.
There have been several approaches to systematically organize data types: algebraic specification methods using algebras, domain theory using complete partially ordered sets and type theory using the connection between logics and data types. Here, we use category theory. Category theory has proved to be remarkably good at revealing the nature of mathematical objects, and we use it to understand the true nature of data types in programming.
We organize data types under a new categorical notion of F,G-dialgebras which is an extension of the notion of adjunctions as well as that of T-algebras. T-algebras are also used in domain theory, but while domain theory needs some primitive data types, like products, to start with, we do not need any. Products, coproducts and exponentiations (i.e. function spaces) are defined exactly like in category theory using adjunctions. F,G-dialgebras also enable us to define the natural number object, the object for finite lists and other familiar data types in programming. Furthermore, their symmetry allows us to have the dual of the natural number object and the object for infinite lists (or lazy lists).
We also introduce a functional programming language in a categorical style. It has no primitive data types nor primitive control structures. Data types are declared using F,G-dialgebras and each data type is associated with its own control structure. For example, natural numbers are associated with primitive recursion. We define the meaning of the language operationally by giving a set of reduction rules. We also prove that any computation in this programming language terminates using Tait's computability method.
A specification language to describe categories is also included. It is used to give a formal semantics to F,G-dialgebras as well as to give a basis to the categorical programming language we introduce.
CHARITY
http://pll.cpsc.ucalgary.ca/charity1/www/home.html
Charity is a categorical programming language
Computational Category Theory
http://www.cs.man.ac.uk/~david/categories/
Computational Category Theory is an implementation of concepts and constructions from category theory in the functional programming language Standard ML. The original ideas are due to R.M. Burstall, and it was developed by D. Rydeheard, with help from D.T. Sannella and others in the University of Edinburgh theoretical computer science community.
Prospects for Category Theory in Aldor
by Saul Youssef, 2004.
http://atlas.bu.edu/~youssef/papers/math/aldor/aldor.pdf
and the following slides:
http://atlas.bu.edu/~youssef/homepage/talks/categories/categories.html
The Microcosm Principle and Concurrency in Coalgebra
http://www.kurims.kyoto-u.ac.jp/~ichiro/papers/microcosm.pdf
by Ichiro Hasuo, Bart Jacobs and Ana Sokolova
http://www.kurims.kyoto-u.ac.jp/~ichiro/papers.html
Abstract
Coalgebras are categorical presentations of state-based systems. In investigating parallel composition of coalgebras (realizing concurrency), we observe that the same algebraic theory is interpreted in two different domains in a nested manner, namely: in the category of coalgebras, and in the final coalgebra as an object in it. This phenomenon is what Baez and Dolan have called the microcosm principle, a prototypical example of which is “a monoid in a monoidal category.” In this paper we obtain a formalization of the microcosm principle in which such a nested model is expressed categorically as a suitable lax natural transformation. An application of this account is a general compositionality result which supports modular verification of complex systems.