20
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Do you consider monads as a part of the programming language or programs? Arrows? $\endgroup$ – Dave Clarke Aug 15 '13 at 9:32
  • 2
    $\begingroup$ This strikes me as a philosphical question, at least in part. I'm not sure there is a single correct answer. One adept of category theory will apply the intuition gained from it while programming, another will favor different ways of thinking. $\endgroup$ – Raphael Aug 15 '13 at 10:16
  • 2
    $\begingroup$ Most programs being written use programming languages not inspired by category theory. As far as I can tell, the average programmer is not aware of category theory, and so most programs (including your operating system and your browser) aren't inspired by higher mathematics. $\endgroup$ – Yuval Filmus Aug 15 '13 at 14:40
  • 1
    $\begingroup$ @YuvalFilmus: My question is targeted towards functional programming languages $\endgroup$ – Ankur Aug 15 '13 at 15:54
  • 1
    $\begingroup$ see also this question for some CS applications of monoids $\endgroup$ – vzn Aug 21 '13 at 21:56
13
+50
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ That's precisely my point. If I am designing accounting software, the type system will be my language for design. If I am designing a mathematical software even then I will use the type system to represent category theory concepts. Which basically indicates that type theory OR type systems are more general abstractions then category theory. $\endgroup$ – Ankur Aug 22 '13 at 8:08
  • 1
    $\begingroup$ That is a ridicolous statement. I think you should perhaps learn some more before you make sweeping statements like that. Perhaps you can start with existentialtype.wordpress.com/2011/03/27/the-holy-trinity $\endgroup$ – Andrej Bauer Aug 22 '13 at 9:01
  • $\begingroup$ I ain't a researcher, Phd guy, scientist, mathematician or category theorist, so don't get upset about my statements, they are not going to be published in some scientific journal or research papers. I am just a programmer who is trying to understand the other side of the coin. By the way, thanks for the link. $\endgroup$ – Ankur Aug 22 '13 at 9:54
  • 1
    $\begingroup$ I realize this, which is precisely why I am suggesting that you should be careful about drawing conclusions like you do: you simply do not have the information required to draw such conclusions. And this is also why I am referring you to a blog post by Bob Harpher rather than, say, some technical book about the relationship between type theory and category theory. I am trying to help, but I would expect in return a bit more reservation from you when it comes to making grand conclusions about the nature of a whole branch of mathematics. $\endgroup$ – Andrej Bauer Aug 22 '13 at 10:25
  • $\begingroup$ For instance you stated that "type theory is a more general abstraction than category theory". This is an example of a statement that you should know not to make based on little knowledge. I work professionally in this area and even I would be very careful to make such a conclusion, or the opposite one. $\endgroup$ – Andrej Bauer Aug 22 '13 at 10:27
6
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.