1
$\begingroup$

I've only learned bit of category theory, but so far its relation to type systems seems mostly descriptive. For example, you really don't need to know about coproducts to come up with the idea of union types.

I'm looking for references to ideas in computer science that were arrived at due to results in category theory. I'd be especially interested in results in areas other than PL such as machine learning.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
2
$\begingroup$
  • Categories can be used to model databases, and have been used for data integration. See also this paper. There's a pretty gentle introduction in chapter 3 of Seven Sketches in Compositionality.
  • Coalgebras are a generalization of automata, and have provided insight into notions of bisimulation. I saw a talk about this, but also found this paper
  • Closed symmetric monoidal categories have been used to model linear logic, but also to model quantum computation (which is itself related to linear logic). There's a Rosetta Stone paper that discusses this.
  • CRDTs are a cornerstone of distributed computing, and while I don't understand it myself, it looks like there is some connection to category theory
  • Guarded recursion and the Topos of Trees generalize step-indexing, which has been used to model higher-order separation logic. This is a tool for verifying programs with heap memory and/or concurrency, and has been applied in Iris.

I think it's also worth mentioning that the Programming Language concepts are not exactly isolated or esoteric. Monads originated in Category theory: my understanding is that Moggi (a category theorist) first applied them, and they were brought into Haskell by Philip Wadler.

But, monadic interfaces are everywhere. Errors in Rust are monadic, as are basically any langage's Option type. Promises in Javascript are monads. Using monads gives a beautiful implementation of Software Transactional Memory, a lock-free approach to concurrency.

And, of course, category theory is basically at the heart of modern logic research, which underlies most CS theory.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ The work on algebraic effects that people are abuzz about also traces back to Gordon Plotkin and John Power trying to model effects using Lawvere theories (one of the ways of doing algebra categorically). $\endgroup$
    – Dan Doel
    Sep 16, 2020 at 22:54
  • 1
    $\begingroup$ Also homotopy/cubical type theory has applications to computation, but it seems highly unlikely it would have been worked out without the connection to homotopy theory via infinity groupoids. Bernardy's work on internal parametricity uses a framework that is suspiciously close to cubical type theory, and although it predates the publication of the latter, it thanks Coquand, so I wouldn't be surprised if Coquand were already working on cubical type theory and suggested similar ideas for parametricity (and Cavallo/Harper presented a more integrated treatment since). $\endgroup$
    – Dan Doel
    Sep 16, 2020 at 22:59
  • 1
    $\begingroup$ I feel I should add: I don't mean anything negative about Bernardy by my use of "suspicious." I just mean it is very similar to cubical ideas, and I wouldn't be surprised if he were inspired by ideas that were 'in the air' at the time, borrowed from categorical treatments of topology. Working through the details is still seriously non-trivial even in that light. $\endgroup$
    – Dan Doel
    Sep 16, 2020 at 23:16
  • 1
    $\begingroup$ @jmite if you get a chance, would you mind updating the pointer to the paper about coalgebras and bisimulation. Seems very interesting, but the link's broken. Even just a title and author would help! $\endgroup$
    – Robert P. Goldman
    Mar 23 at 1:10
1
$\begingroup$

Not what you are hoping for, but:

An early version of the OCaml language was based on the idea of a categorical abstract machine "represented by Cartesian closed category".

Haskell's monad classes "are based on the monad construct in category theory".

Improve this answer
$\endgroup$
2
  • $\begingroup$ Were monads in Haskell their first use in programming, or was the idea used earlier and given a name by category theory? $\endgroup$
    – Davis Yoshida
    Sep 16, 2020 at 21:48
  • $\begingroup$ The Monads Wikipedia pages gives the answer, which I'll summarize as "It's complicated" :-) . $\endgroup$
    – Mars
    Sep 16, 2020 at 22:49

Your Answer

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

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