71
$\begingroup$

I'm wondering what the relation of category theory to programming language theory is.

I've been reading some books on category theory and topos theory, but if someone happens to know what the connections and could tell me it'd be very useful, as that would give me reason to continue this endeavor strongly, and know where to look.

Motivation: I'm currently researching undergraduate/graduate mathematics education, specifically teaching programming to mathematics grads/undergrads. I'm toying with the idea that if I play to mathematicians strengths I can better instruct them on programming and they will be better programmers, and what they learn will be useful to them. I'm in the process (very early stages) of writing a textbook on the subject.

YCor
66.9k5 gold badges201 silver badges298 bronze badges
asked Nov 5, 2009 at 9:38
$\endgroup$
4
  • 1
    $\begingroup$ This is very similar to another question about category theory and programming languages, but I changed it to reflect wanting to know some precise connections, rather than merely where to look. $\endgroup$ Commented Nov 5, 2009 at 13:04
  • 1
    $\begingroup$ Topoi are sort of on a different "branch" than programming languages. Their least common ancestor would probably be Lawvere's Hyperdoctrines or just Cartesian Closed Categories. Not to discourage you from learning about topoi (they're fascinating!), but they don't play a big role in programming languages. $\endgroup$ Commented Jan 18, 2010 at 23:28
  • 6
    $\begingroup$ Also, frankly, I think CS students would be far better off if we dragged them through a semester of set theory first. It would make a whole lot of other stuff easier; we could talk about "recursive sets of natural numbers" instead of decidable problems. But I don't think you'll be able to get enough category theory into an undergrad's head (even a math undergrad) in time to generate significant returns on the investment in terms of understanding PL. $\endgroup$ Commented Jan 18, 2010 at 23:31
  • 4
    $\begingroup$ "I think CS students would be far better off if we dragged them through a semester of set theory first" What a horrible thought! $\endgroup$ Commented Apr 26, 2015 at 14:24

10 Answers 10

92
$\begingroup$

The most immediately obvious relation to category theory is that we have a category consisting of types as objects and functions as arrows. We have identity functions and can compose functions with the usual axioms holding (with various caveats). That's just the starting point.

One place where it starts getting deeper is when you consider polymorphic functions. A polymorphic function is essentially a family of functions, parameterised by types. Or categorically, a family of arrows, parameterised by objects. This is similar to what a natural transformation is. By introducing some reasonable restrictions we find that a large class of polymorphic functions are in fact natural transformations and lots of category theory now applies. The standard examples to give here are the free theorems, see Philip Wadler's 1989 article Theorems for free!, in FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture.

Category theory also meshes nicely with the notion of an 'interface' in programming. Category theory encourages us not to look at what an object is made of, but how it interacts with other objects, and itself. By separating an interface from an implementation a programmer doesn't need to know anything about the implementation. Similarly category theory encourages us to think about objects up to isomorphism - it doesn't precisely proclaim which sets our groups comprise, it just matters what the operations on our groups are. Category theory precisely captures this notion of interface.

There is also a beautiful relationship between pure typed lambda calculus and cartesian closed categories (CCC). Any expression in the lambda calculus can be interpreted as the composition of the standard functions that come with a CCC: like the projection onto the factors of a product, or the evaluation of a function. So lambda expressions can be interpreted as applying to any CCC. In other words, lambda calculus is an internal language for CCCs. This is explicated in Lambek and Scott. This means for instance that the theory of CCCs is deeply embedded in Haskell, because Haskell is essentially pure typed lambda calculus with a bunch of extensions.

Another example is the way structural recursion over recursive datatypes can be nicely described in terms of initial objects in categories of F-algebras. You can find some details in Philip Wadler's note Recursive types for free! (dated originally to 1990, labelled "DRAFT DRAFT DRAFT DRAFT DRAFT").

And one last example: dualising (in the categorical sense) definitions turns out to be very useful in the programming languages world. For example, in the previous paragraph I mentioned structural recursion. Dualising this gives the notions of F-coalgebras and guarded recursion and leads to a nice way to work with 'infinite' data types such as streams. Working with streams is tricky because how do you guard against inadvertently trying to walk the entire length of a stream causing an infinite loop? The appropriate dual of structural recursion leads to a powerful way to deal with streams that is guaranteed to be well behaved. Bart Jacobs, for example, has many nice papers in this area.

David Roberts ♦
36.4k12 gold badges137 silver badges381 bronze badges
answered Nov 5, 2009 at 17:14
$\endgroup$
4
  • 3
    $\begingroup$ Awesome! This is EXACTLY what I was looking for! $\endgroup$ Commented Nov 5, 2009 at 18:27
  • 6
    $\begingroup$ And sigfpe is exactly the person to give such an answer! You should read his blog for nice examples of programming category theoretical notions: blog.sigfpe.com $\endgroup$ Commented Jun 10, 2010 at 20:59
  • $\begingroup$ Free theorems as I understand it were given based on logical relations not natural transformations (I'm aware of some work sort of relating the two). Do you have a reference for free theorems as natural transformations directly? $\endgroup$ Commented Apr 15, 2014 at 15:28
  • $\begingroup$ @sclv I looked for such papers myself a while back and didn't find them. $\endgroup$ Commented Apr 15, 2014 at 15:56
20
$\begingroup$

Lambek & Scott, "Introduction to higher order categorical logic" is one classic book on the subject.

What language are you (researching?) teaching to these math students? IMHO Haskell is easier to learn than close-to-the-metal languages for mathematically minded people without prior programming experience.

answered Nov 5, 2009 at 15:38
$\endgroup$
5
  • 2
    $\begingroup$ I'm currently looking at Haskell, ML, and Scala. I'm strongly inclined toward Haskell and ML. $\endgroup$ Commented Nov 5, 2009 at 16:35
  • 3
    $\begingroup$ I don't know much about Scala, but ML is a good choice too--it has many of the same advantages as Haskell (emphasis on values rather than computations, a sensible type system) while lacking some features (typeclasses, monadic IO) of Haskell which are extremely useful but require some abstraction cost up front (and if nothing else often lead to error messages which are baffling to beginners). $\endgroup$ Commented Nov 5, 2009 at 17:27
  • 2
    $\begingroup$ ML is a superb choice. Haskell is as well. I think the pedagogical material for ML is more developed, partly because the language hasn't changed much in quite a while. $\endgroup$ Commented Jan 18, 2010 at 23:33
  • 1
    $\begingroup$ Helium (cs.uu.nl/wiki/Helium) is a variant of Haskell developed for teaching – the goal of the project was to produce a subset of Haskell that would permit comprehensible error messages. I believe that Helium is still supported, if not actively developed. $\endgroup$ Commented Jun 10, 2010 at 20:40
  • $\begingroup$ Scala actually has all of the category theory goodness in it if you look at Scalaz, just without the enforced purity and (inevitably) incomplete type inference. It also compares favorably with ML, with some stuff missing but a more expressive type system according to some sources. $\endgroup$ Commented Apr 26, 2014 at 2:00
18
$\begingroup$

A lot of work has been done in this area. As mentioned above, there is an essential correspondence between the $\lambda$-calculus and Closed Cartesian Categories. Moggi's seminal work Notions of Computations and Monads developed a unified way of treating many computational effects. This of course inspired Haskell's current approach to dealing with IO, State, Concurrency and so forth. The dual approach, Comonadic Notions of Computation by Tarmo Uustalu and Varmo Vene, captures a other notions, such as stream based computation. Classes and object-oriented languages can be modelled using coalgebra (also mentioned above). A general reference to the coalgebraic approach is Universal Coalgebra: A Theory of Systems by Jan Rutten, and articles showing how to apply it to object-oriented languages include Reasoning about Classes in Object-Oriented Languages: Logical Models and Tools and Coalgebraic Reasoning about Classes in Object-Oriented Languages by Bart Jacobs and colleagues. Although these are aimed at reasoning about programs, they do give semantics for the relevant programming languages along the way.

Martin Sleziak
4,7734 gold badges38 silver badges42 bronze badges
answered Jun 10, 2010 at 15:01
$\endgroup$
12
$\begingroup$

John Baez and Mike Stay’s 2009 article Physics, Topology, Logic and Computation: A Rosetta Stone, the n-Category Café discussion New structures for physics III, and Yuri Manin’s 2009 article Renormalization and computation I: motivation and background are perhaps interesting for you.

Peter LeFanu Lumsdaine
23k2 gold badges80 silver badges137 bronze badges
answered Nov 5, 2009 at 10:09
$\endgroup$
0
10
$\begingroup$

The connections I have seen are in the area of denotational semantics and type theory. For example, the objects can be the types: Integer, List(Integer), Integer+List(List(Integer)), etc. Functions (in the language) are arrows between the objects. (So the successor function is an arrow from Integer to Integer.) Then categorical constructions translate into programming language constructs ("List" is an endo-functor, for example). The existence of recursive functions is guaranteed by certain categorical properties of the category, etc.

answered Nov 5, 2009 at 16:55
$\endgroup$
10
$\begingroup$

If you want to get your hands dirty, look into the programming language Haskell, which has functors and natural transformations.

Functors implement structure. For instance, consider the category of types T and a functor L that sends a type t to the type L(t), lists of t. This is somewhat similar to the functor on Set that sends a set X to the set of all finite lists on the set X (i.e. the underlying set of the free monoid on X). You could also consider a functor B that sends a type t to the type B(t) of a binary tree on t.

Now you can define a natural transformation from B(t) to L(t) such as flatten, which takes a binary tree and flattens it to a list. So as functors implement structure, natural transformations alter structure.

It gets interesting when you bring in monads. Using the list functor above, think about L(L(t)), lists of lists. You can concatenate a list of lists to a single list, which corresponds to the monad map L(L(t)) to L(t).

Check out this link for more.

Martin Sleziak
4,7734 gold badges38 silver badges42 bronze badges
answered Nov 17, 2009 at 21:44
$\endgroup$
6
$\begingroup$

You may enjoy The Algebra of Joy which "gives several analogues of concepts from category theory."

Martin Sleziak
4,7734 gold badges38 silver badges42 bronze badges
answered Dec 11, 2009 at 20:08
$\endgroup$
5
$\begingroup$

If you want a very basic, entry level description of category theory from a Haskell programming point of view (not exactly what the OP asked for),

is nice.

Martin Sleziak
4,7734 gold badges38 silver badges42 bronze badges
answered Feb 19, 2012 at 3:52
$\endgroup$
3
$\begingroup$

If you are teaching to undergrads and you are looking for a book which allows you a quick connection between category theory and programming, without the heaviness of the mathematical treatment, I suggest the works of Bartosz Milewski. He is a C++ and Haskell developer. I think "Category Theory for Programmers" is a great introduction to the topic for the non-mathematician. You can buy his book or read it on the blog.

https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/

answered Mar 16, 2023 at 15:49
$\endgroup$
2
  • $\begingroup$ I think the answer is clear enough to avoid the very last sentence (the one just above the link), since both the blog and the book are valuable sources that can be easily found by performing a standard search. $\endgroup$ Commented Mar 16, 2023 at 15:57
  • $\begingroup$ Removed the last sentence $\endgroup$ Commented Dec 9, 2024 at 11:36

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.