Category theory (not) for Programming?

Question

After learning Haskell and other not so pure FP languages I decided to read about Category theory. After gaining good understanding of Category theory I started thinking about how the concepts of category theory can be used to think about designing programs but no matter how hard I tried it seems this is not the way to go.

After spending many unsuccessful attempts to relate category theory to designing programs I came to the conclusion that:

• Category theory is useful when designing a programming language.
• Category theory is not something that you use when designing programs (even when using a language which was designed based on category principles). For example: When programming in Haskell you will use types, types constructor, functions, higher order functions etc to design your program, not category theory concepts.

In summary we have below layer system (order is low to high):

Category theory -> Programming language -> Program

At a particular layer you use the concepts of the immediate underlying layer.

Is this understanding correct? If not and you believe that in designing programs we can directly use category theory concepts, please refer some articles or blog posts where it is being demonstrated.

NOTE: By designing programs I mean designing programs based on different concepts, like concurrency, parallelism, reactive, message passing etc.

Answer 1

Well, that of course depends on what sort of program you are trying to design.

If you are designing an accounting program for your aunt's chocolate shop, I very much doubt category theory will be of much use.

But there are of course situations in which category theory is enormously useful in design of programs (by which I also mean data structures, libraries, and so on). Such situations occur mostly when the programs involved are of a mathematical nature.

If you want to write programs that compute with exact real numbers and other structures occurring in mathematical analysis, the first question you need to answer is what it means to correctly implement a complicated mathematical object (such as a differentiable function, a manifold, etc.). Here it helps very much to know some category theory and logic, because they give you a systematic way of translating definitions of mathematical structures to specifications and implementations of corresponding data structures. The buzzword you should look for is realizability theory. But this is just one example.

The best way to see how category theory comes in handy is to look at programs written by people who know a lot of category theory (and mathematics in general). An obvious example of this is Martín Escardó and his impossible functionals, for instance:

M. Escardó and P. Oliva: What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common, Mathematically Structured Functional Programming 2010, ACM Press. (with companion Haskell and Agda files)

You may complain that this is not just category theory but also logic and topology. Such complaints would be severely misguided. The best category theory is always mixed with other things.

Lastly, I would advise against drawing grand conclusions about nature of things based on a bit of self-assigned reading.

Answer 2

People used to use CT to describe data types.

1. The data type was defined by a particular category whose objects are finite sequences of (specification language) types, and whose arrows were projections or else compositions of the data type operations. For example, the object is the domain and is the codomain of the push operation of stacks. This gives you syntax, but you still don't have a notion of semantics.
2. An algebra, which is to say, an instance of the type, is a functor from the theory to Ens, the category of (small) sets. (We use "small" to avoid Russell's paradox, but it doesn't mostly matter.)
3. It turns out that closure properties of the categories correspond to families of logical theories. For example, if the theory category is closed under products, the data type can be axiomatized by equations. If the theory category is closed by taking pullbacks, then the data type can be axiomatized by Horn sentences.

I'm not completely sure anybody pays attention to this any more. I would think that this, and the links there, would explain it in more detail.