In this video, category theory is explained to an audience of programmers. The speaker says that we can think of a category as a programming language, and of objects as types in that language, and morphisms as static methods from type to type.

To what extent is this perspective correct? Are there major issues with it?

ps. How does this relate to the curry howard lambek isomorphism?

  • 1
    $\begingroup$ Functional programming goes in this direction. $\endgroup$ – Wuestenfux Jan 27 '19 at 9:35
  • $\begingroup$ You could also explain category theory to a person having only a hammer by saying that objects are nails ... $\endgroup$ – Hagen von Eitzen Jan 27 '19 at 9:38

It would make more sense to say that categories are the semantic domains for denotational semantics for type theories (or rather, serve that function rather well). In other words, it would make more sense to say that if you were trying to understand the meaning of a program, you could interpret it into objects and arrows of a category with suitable structure, and then analyze the result mathematically. That said, you can formulate syntactic categories that, as the name suggests, are closer to "programming languages". Really, the best fit would be a presentation of a category (with suitable structure). We can talk about, e.g. the free cartesian closed category generated from a graph.

When we want to talk about cartesian closed categories in general, we typically work with some presentation of them. Usually this happens by asserting that not only do certain universal constructions, e.g. binary products, exist, but that they are chosen by which we mean we have a (bi)functor that actually picks out a specific object to be the binary product of two other objects. This chosen structure, particularly combined with a presentation for the underlying category, provides an abstract, syntactical way of referring to structure within an arbitrary cartesian closed category. It is possible to compile the simply typed lambda calculus (STLC) in terms of this structure in such a way as to validate the reduction rules of the STLC. We can go further and show that all that structure is expressible in terms of the syntax of the STLC in such a way as to validate the universal properties. Altogether this leads to the simply typed lambda calculus being the internal language of cartesian closed categories. This is indeed part of the Curry-Howard-Lambek correspondence.

I haven't watched the video you reference, but there's definitely a way it can be understood to be roughly true. Erik Meijer does know what he's talking about to a reasonable degree with regards to these topics. However, he's often talking to an audience where there's not much value in being very precise.


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.