2
$\begingroup$
  1. Are there any historical connections between OOP (object oriented programming) and category theory?
  2. Could you provide some references (not necessarily historical) that link the two?

I finally got the concept of OOP when learning Python and have been reading Aodey's book on category theory. Both "feel" very similar. Thanks for any help.

$\endgroup$
1
  • $\begingroup$ I keep asking myself this. Lets see if anything pops up. $\endgroup$
    – goblin GONE
    Commented Dec 9, 2013 at 23:56

2 Answers 2

Reset to default
2
$\begingroup$

I'm surprised at the MathOverflow answer posted, as there are a ton of smart people on that site who know a lot, but it's pretty off on this.

There is a long history on the categorial analysis of programming languages and a huge literature. Much of the foundations of category theory overlaps with work in the semantics of formal languages, and people like Dana Scott contributed widely here.

The first correspondence that one should be familiar with here to associate programming language to categorial notions is found in the Curry-Howard isomorphism. In it's original form, this was an association between type theory and proof theory ("proofs as programs" is the informal association here), however much of the logical foundations of the correspondence were developed in the categorial language by Lawvere and others early on, and Lambek made the association explicit between the equational theory of typed lambda calculus and Cartesian closed categories.

In this association, the objects of the CCC are the types and terms are morphisms. Polymorphism is represented in second-order logic.

Per Martin-Löf has developed this type theory as a rigorous semantic foundation for computer science and shown how it can also be used in foundations of mathematics. Unsurprising to those who work in these areas but possibly to those who are being introduced, this is a constructivist foundation. This is because a rigorous semantics that attempts "realisable meaning" usually ends up being intuitionist, for all of the classical constructivist arguments.

For some more background and extensive bibliographies, see "Types and Programming Languages" by Benjamin Pierce or "Lectures on the Curry-Howard isomorphism" by Sørensen and Urzyczyn.

$\endgroup$
1
  • $\begingroup$ And just a brief more on why the objects of a CCC are types and not "objects" (or instances) in computer science: look at functions. E.g. the "int max(int first, int second)" maximum function is a morphism of types because it can take any instance of int x int and map it to an instance of int. Category theory has a mechanism for identifying logical "elements" through the maps from the terminal object, but we really want to talk more generically. When we compose functions, we aren't composing instances of application, we are creating a new function that operates on all instances. $\endgroup$
    – ex0du5
    Commented Dec 10, 2013 at 17:40
1
$\begingroup$

See this MathOverflow discussion. There is also this interesting discussion.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .