Category theory in design

I have seen mentioned in this site that category theory is useful in clarifying the design process. I am wondering if the categorical approach would be any different from a purely functional approach. My reasoning is that in category theory, objects (states and data) are not important, if not almost entirely dismissable. What is of importance to the categorists is the relationships between objects, the functions, the way the structures work. It seems to beg the question, is category theory an abstraction of functional programming (not in an intuitive manner, but in the strict sense) and is there anythings that would be explanable in category theory that would not be in a functional language and the converse?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


What we are probably seeking is a "purer" view of functions: a theory of functions in themselves, not a theory of functions derived from sets. What, then, is a pure theory of functions? Answer: category theory.

                                                                                Dana S. Scott, Relating theories of the λ-calculus

I agree. Then would you

I agree. Then would you agree, that it would be worthwhile to come up with a categorically oriented programming language?

My original question remains: how would a categorically oriented programming language differ from a functional one?

My opinion is that in a categorically oriented language, it may be fine to think of functors, transformations, and maybe even use parts of categorical logic in a first class manner. I just cannot think of a reason that would be different from higher order functions.

This previous post will be

This previous post will be of interest. Particularly the thesis mentioned.

José Luiz Fiadeiro's book

José Luiz Fiadeiro's book Categories for Software Engineering applies categorical concepts to computing in a very different way from the usual type-theoretic, functional programming point of view where morphisms in Cartesian closed categories represent computations. The basic idea (although I can't claim to have done anything other than skim the book) seems to be to use categories to describe aspects of software components and component engineering, e.g. modularity, refinement relationships, composition, features, etc.

To the best of my limited knowledge these approaches haven't yet precipitated into any actual programming languages, but perhaps they point to at least one sense in which a "categorically-oriented programming language" might differ from a language like Haskell.

Could you name some of the

Could you name some of the books, online readings where the usual type-theoretic point is discussed, please?


Previously on LtU

A discussion on introductory category theory for CS folk.

Goguen school

Judging from his worshop slides (for "Categorical Structures for System Modelling", available as ZIPped pdf & quicktime from his homepage), his general approach follows that of Joseph Goguen's approach to algebraic datatypes, which uses various sorts of reasoning with limit and colimit constructions over cartesian categories, which are usually not closed, and which provide good algebraic structures for modelling equational logics. There are quite a lot of programming languages based on this; probably the first places to look at are Goguen's OBJ3 language, based on order-sorted cartesian categories, and Maude, which is based on rewriting logic.

Joseph Goguen put up a page on the OBJ family of languages.

Postscript: I see that Fiadeiro's CommUnity language, which is used in his book, has its operational semantics based on rewriting logic.

System specification

The best example of category theory being used for something in CS design that isn't immediately obviously reducible to something based in a functional language would be specifying systems, particularly system configuration. Mostly here I'm thinking in terms of things like presheaves as configured specifications, presheaf models for concurrency, coalgebraic class specification, and coalgebra in general as a theory of systems.

Now all of those are not strictly pure category theory, but are ultimately best understood from a categorical framework. Nor am I sure that they are not expressible in a functional language -- it just doesn't seem immediately obvious to me how to do so (or even why you would want to). A final proviso: I am a mathematician, not a computer scientist, so my understanding of the CS aspects of this is somewhat limited.


Pure category theory might not even be practical in the areas above, yet this is the kind of thing I was talking about. Those articles show ways that using category theory can help design, even to the point of making system specification and design mechanical and provable. Perhaps it would be worthwhile to utilize these ideas in a generic sense and create CASE tools that explicitly make use of the patterns found in category theory.

I believe there is a point here outside of design that I am addressing though. Many, if not most of the ideas of categories where examining a single category can be expressed using higher order functions, such as map, and beyond that relationships of functors between more than one category can be expressed with higher-order functions as well.

However, it is not clear that (the main purpose of category theory) natural transformations and adjoints would have an easy or intuitive specification in a primitive recursion or second order recursion. I think that designing a language that can handle natural transformations and adjoints in a first class way, so that the programmer could just use them, has the potential to make algorithm specification a bit easier. Instead of utilizing two functors say F and G and a two functors that map F onto G and G onto F; one could just call { nTrans args } and not worry about it. I am just not sure how much this would be useful outside of technical math work and/or theorem proving, or if there is a subtlety about how to simply do it in a functional language that I have missed.

See above

If you haven't yet, you should definitely look at the thread linked by naasking earlier. And you should definitely look at Tatsuya Hagino's thesis.

For an alternative view

For an alternative view of the role of category theory in design take a look at the work of Doug Smith and his colleagues. E.g. A rather shallow summary of the idea, as i understand it, is software design by refinement. Given a pre-existing taxonomy of refinements (morphisms) in a library, if a match between your problem spec and a library component can be found (another morphism), then the required refinement of your spec is the pushout of the two morphisms. Once the particular library refinement has been identified, the pushout can be mechanically computed.