9

Category theory has applications in theoretical computer science and obviously is central to abstract mathematics. I have heard that it also has direct practical applications in programming and software development.

What type of programming is practical category theory necessary for? What do programmers use category theory to accomplish?

Please note my use of "necessary" and "require" in this post. I realize that in some sense most programmers will benefit from having experience in different types of theories, but I am looking for direct applications where the usage of category theory is essential, i.e. if you didn't know category theory, you probably couldn't do it.

Also, I'd like to clarify that by "what type of programming," I am hoping less for a broad answer like "functional programming," and more for specific applications like "writing bank software" or "making operating systems."

4
  • 2
    I think one of the best (but not easy if you're new to FP) explanations of the reasons why category theoretical thinking in programming is highly beneficial is stackoverflow.com/questions/16015020/…: Apr 26, 2014 at 1:34
  • 2
    This is a good excerpt: "[...] just a common pattern in mathematics that's been "factored out", just like we do with code. People noticed that a whole bunch of interesting things—the aforementioned monoids, groups, lattices and so on—all follow a similar pattern, so they abstracted it out. The advantage of doing this is the same as in programming: it creates reusable proofs and makes certain kinds of reasoning easier." Apr 26, 2014 at 1:35
  • "soft", and conceptual. I don't have the heart to vote to close the question myself, 'cause I kinda like it, but if you wanted to, yeah, you could flag for migration. Probably easier to just delete it and ask over on Programmers, though. Apr 26, 2014 at 1:41
  • 1
    @MichaelPetrotta I'll flag it so that Erik's comments aren't lost.
    – Alexander Gruber
    Apr 26, 2014 at 1:43

2 Answers 2

3

The question is asking about an abstract mathematical concept (category theory) while hoping for a very practical answer (specific applications). With all due respect, I think this is unrealistic expectation.

Abstract mathematical concepts are part of the fundamentals of programming languages, not applications. For instance, data types are central to programming. Every language has some form of data types and implements a type system -- whether static or dynamic, strong or weak, explicit or implicit, etc. However, there is no standard.

Therefore, many computer scientists have attempted to use category theory to define a unified type system. See for instance Hagino's Categorical Programming Language (1987) and Charity (1996), then ML (2003) and CAML, and Haskell of course, which defines a "Haskell category" of types, and Haskell functions are morphisms on types...

This is the case because type theory is closely related to category theory. To quote JL Bell: "Categories can themselves be viewed as type theories of a certain kind... Thus type theory is much more closely related to category theory than it is to set theory... Roughly speaking, a category may be thought of as a type theory shorn of its syntax." It has been shown that, for instance, Cartesian closed categories correspond to typed λ-calculus and C-monoids correspond to untyped λ-calculus...

I don't think category theory is necessary for any type of programming, but it is a very useful tool in the design and implementation of programming languages, and esp. those which are inherently mathematical. That is why Functional Programming is often cited as a categorical programming, and all the programming languages mentioned above are FP languages.

A recommended introduction to the topic is "A taste of category theory for computer scientists" by BC Pierce (1988). This and other useful info was found on a similar discussion on mathoverflow.

2
  • "With all due respect, I think this is unrealistic expectation.": Why? There are other examples of very practical applications of abstract mathematical concepts, e.g. for cryptography in online-banking.
    – Giorgio
    Jun 28, 2014 at 6:43
  • 1
    Cryptography isn't an abstract mathematical concept. It's very concrete: stopping some people from understanding your communications to others.
    – occulus
    Sep 22, 2017 at 9:09
-1

It's like org-mode for banks.

I realise that's vague but you did say you wanted a practical answer..

Categories are all about duality (or at least that's how I see it) because of the axiom of choice, so personally I'd say it'd be a silly way to induct a unified type system although a type itself (an instance of a type) is basically a category.

Simply typed lambda calculi don't have an axiomatic type system, which is why they are said to be the foundation for type theory. This is different from lambda calculi that use a proper type system.

Simply typed lambda calculus strongly normalizes and although matching types is pretty boring, the logic is sound.

Also infinite/dependently typed lambda calculus (or purely typed) does not normalize properly as it has a type for all types, which is basically a church encoded type system.

Categories are everywhere but are by very nature almost impossible to see straight away.

1
  • 1
    "It's like org-mode for banks." I chuckled, but I don't get it.
    – abstracted
    Apr 8, 2015 at 17:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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