One of the books I’d set aside until the main work on IFL2 was done and dusted is Brendan Fong and David Spivak’s An Invitation to Applied Category Theory (CUP, 2019 — there’s a late version freely available here). I’ve now had a first proper look. I can’t say that the book overall works very well for me. When the authors are talking about things I already know a fair bit about, I find there are indeed interesting approaches and illuminating comparisons. But when they are introducing new-to-me material it, all goes by too fast to be very helpful. That could of course just be a comment on my inadequacies as a reader! — but I’d be quite surprised if mine weren’t a common reaction. Chapter 7 on sheaves and toposes, for example, is surely going to pretty impenetrable to someone who doesn’t already have some handle on this stuff.
However, there are obviously lively minds at work here, and so I’m encouraged to take a look at another of their projects — an MIT course of lectures with the estimable Bartosz Milewski (whose Category Theory for Programmers I think is terrific). The course, Programming for Categories, has a web page here with planned links to videos of each lecture and also links to lecture notes. The lectures are just starting, and new videos/notes should appear five times a week for four weeks. I’ll hope to learn a lot!
I have been keeping up with the class online and I have to say that overall I am disappointed but with some slight hope for the future.
I have been programming in Haskell for about 7 years now, and learning category theory has been on my list of things to do for a while (my background is analytic philosophy and mathematical logic and programming is how I pay for school) so I thought this would be a great way to do it. Unfortunately, I’ve found both subjects to be presented in muddled ways so far.
It is always a tall order to try and start a subject from the ground up, which this class purports to do with both category theory and programming. From the webpage: “We will assume no background knowledge on behalf of the student, starting from scratch on both the programming and mathematics.” If this class was my first introduction to programming and I went solely based on the lectures, I would be hopelessly lost. The lecture notes, which have been referred to as “the book” so I’m assuming (and hoping) they’ll eventually be refined into a full book. They do go into some basic Haskell syntax in the beginning of the notes, which is nice, but if this is supposed to be someones first introduction to *programming*, not just to *Haskell*, they will end up feeling clueless about what programming is, why we do it, what you’re even able to do with a computer, what every day programmers do, etc. I assume that Milewski specifically wrote the introduction to Haskell section, and he speaks of a “conceptual debt” that needs to be built up and paid later: “This is how we are going to learn Haskell. We’ll be using things, from day one, without fully understanding their meaning, thus constantly incurring a conceptual debt. Some of this debt will be paid later. Some of it will stay with us forever.” This is, in no uncertain terms, a horrible way to teach a subject, and is unfair to the students who are going into this thinking that they will get an introduction to programming as well as category theory. I can understand, since I have a background in programming, that the conceptual debt that they’re discussion has to do with Haskell being a purely functional language, as evidenced by “This is something you will have to get used to, but it will make a lot of sense later, when we talk about partial application and currying (that’s the kind of conceptual debt we were talking about).” The ‘conceptual debt’ of not understanding why Haskell sugars away lambda expressions and currying is something that could carefully be explained to someone who already has a semester or so’s worth of programming in a more traditional language, but could even more easily be explained to someone who is just being introduced to programming, because you can just tell them that’s what programming is in the first place! The jump to functional languages from the perspective of people who started out with something like C++ or Java is jarring, and obviously the lecturers are aware of that, but they are treating the students, who are not supposed to have a background in programming, as if they are making that jump. Why not explain to the students what currying is right away? In the lectures, they sped past lambdas at lightning speed without explaining why or how they work, just showing what they do. If this is someones first introduction to programming, then they don’t have C++ syntax built into their minds, so you don’t need to be careful to unwind that intuition. Just explain what lambdas are, what currying is, how Haskell sugars them away, and how you can unsugar them to use Haskell to its fullest. There does not need to be a conceptual debt at all.
This highlights my main personal sources of frustration with the course so far. Because I know enough about the programming side of things, I know exactly what and how much is not being said to find the whole thing frustrating when thinking of the new students to the subject. There is a perfect example during the third lecture when Bartosz Milewski is discussing lambda calculus and then briefly mentions partial functions, vaguely talks about the halting problem without ever mentioning the name ‘halting problem’, doesn’t explain why programs that don’t terminate are partial in the sense of recursion theory, doesn’t explain how partial and total functions are related, and just generally glosses over the real connections to recursion theory. He sounded like someone who only partially understands these points and recounted them in a way that someone does to other people who already know them (“which is a partial function, right? And we want total functions, because they’re total, right?”). Again, I know enough about the background to be angry for the people who don’t, because their confusion must be massive at this point. If this is someones first introduction to programming, and your overview of the halting problem consists of saying “well, we would like to be able to tell when a program terminates, but we can’t do that, there is not an algorithm for that, if you say you have one I can construct a program that will not terminate from your algorithm, it’s sort of a diagonal argument, okay?” that student has the right to ask for an entire lecture’s worth of time of you explaining what you just said. Are these students with no background in programming supposed to know what a diagonal argument is, and recognize the unsolvability of the halting problem without you explicitly mentioning that’s what you’re talking about? I don’t know the details, but I know that Andrej Bauer has been vehemently opposed to the idea that Haskell forms a category, and from what I’ve read and from the vague things Milewski said, I think it has something to do with the classical results that not all general recursive functions are total. But with the idea of Haskell forming a category being *central* to this class, how could we brush those details under the rug, as Milewski explicitly said? How can we be comfortable encurring that type of conceptual debt, which I can only presume will never be paid given the way we glossed over the halting problem?
So then we get to the category theory. I will be more brief, because I have less to say, and most of it can be summed up by saying “okay, but so what?” I am in less of a position where I can tell how much I don’t know, but when it comes to some things, like sets, I can, and in those terms I can see how much the lecturers aren’t saying. For example, during the brief discussion of sets and the shunning of axiomatic set theory, instead we are told to think of sets as “bags of dots, the dots being things we don’t care about”. I have enough of a background in the category vs set theory foundation debate to understand what they’re doing and why they’re doing it, but their definitions are inconsistent and without the real motivation behind why we don’t care about the dots in these bags, it just seems pointless. Then, I apologize for not being able to find the quote but I believe it was from a reddit comment (although maybe it was someone commenting on this or another blog, I was reading a lot of online discussions the day I saw this, perhaps it was even in your book?), someone summed up exactly how I feel (paraphrasing): “A lot of people, when they first learn category theory, find themselves saying ‘okay, but so what? Yes, I understand how an anomalous object, the natural numbers as morphisms, 0 as identity, and composition as addition form a monoidal category. But so what? What does this tell us about structure? Yes, addition is associative and 0 is the additive identity, but why do we need category theory to tell us that?” and that is the position I am in after the first 6 lectures. I am in this position with category theory: everything seems so trivial and simple that I do not see the point. Yes, objects can have morphisms between them and morphisms are associative, and we can form functors that take categories to categories preserving associativity and unity. But so what? Why is this any more foundational than abstract algebra? We can come up with axioms and then find structures that obey those axioms, why are the category theoretic axioms so groundbreakingly elucidating to the whole of mathematics?
The reason that I am interested in learning category theory is because I am currently working on the semantic paradoxes and the graph theoretic work that has been done to understand self reference. In the category theoretic foundational world, it has been proposed by many people that *the reason* for self referential paradoxes, and all incompleteness results that in some way involve diagonal arguments, is because of Lawvere’s Fixed Point theorem. They argue that even semantic paradoxes such as The Lair are *a result* of a theorem from category theory. I don’t find this argument compelling in the slightest in terms of philosophically elucidating *why* the paradoxes exist. But be that as it may, my goal with this course was to finally familiarize myself with category theory in such a way that I could do fully understand the proof of the theorem and then have the technical background to start working on learning topos theory and understanding the category theoretic perspective from a technical level. At this point, I don’t think I’ll make it to the end of this course and will be looking elsewhere.
Lastly, I mentioned hope. This course is obviously their first attempt at teaching this material as is, and any class that is this experimental is going to be rough the first few goes. I have respect for all three of the lecturers, I know that they know what they’re talking about, and although I am frustrated at how they are teaching it now, I am hopeful that after a few passes and after refining the lecture notes into the complete book, this becomes a great way for people to learn category theory (but I would urge people to stay away from this as an introduction to programming in general). Unfortunately, I can’t wait that long to learn category theory, so perhaps I’ll go back to Awodey’s Category Theory.
What do you find terrific about Category Theory for Programmers?
The category-theoretic approach to programming seems designed to make writing and understanding programs as difficult as possible, preferably so that only someone with a maths PhD can do it.
Taking it the other way around — so that some things that can be done in some programming languages help you to understand some category theory — is not so bad, but since it would be taken up only by those with a prior interest in category theory, it can’t be imposed on nearly so many people and doesn’t excite hegemonic ambitions.
And so it’s not surprising to see that CTfP is strongly ideological.
Look, for instance, at this from the book:
Ok, “can be thought”, and maybe it’s interesting as a concrete example of something category-theoretic. If I want to learn category theory, I might appreciate having some examples like that.
But that’s not enough for the ideological category theorists, for soon we see:
Now we’re not just being shown something that can be looked at in a category-theoretic way. No, now that’s what it really is, and the ordinary way of looking at the length function “hides” that “fact”.
Ok … in fact I’m probably with you on “ideological category theorists”. There seems quite a bit of muddled thinking about. Witness, indeed, the lecture 1 in the series linked to in the post, where we are told in short order that “a set is a bag of dots”, and a prime example will be the set of natural numbers. So numbers are dots? Really??
What I so much liked about Bartosz Milewski blog-posts-wrapped-up-into-a-book was the expositional clarity: I learnt a lot from them, a while back.