Red-blooded programmers with deadlines and bosses

The title “Category theory Lulz” grabbed my attention, especially in view of the (possibly obsolete) NY Times definition of “lulz”:

the joy of disrupting another’s emotional equilibrium…

Can that really be done with category theory, and how does the joy it procures compare with the pleasure of a non sequitur?

The answer is in Ken Scambler’s two-hour course on YouTube.  It’s probably a sign of the times that this and similar courses were posted at roughly the same time as the long exchange on HoTT and Univalent Foundations was taking place on this blog, and that Bartosz Milewski decided just over a year ago to write a book, apparently one online chapter at a time, entitled Category Theory for Programmers, even though functional programming has been using category theory for decades.  But it’s no longer only relevant to theoretical computer scientists.  Over the last few years, especially, “red-blooded programmers with deadlines and bosses,” as Scambler puts it, have been reading articles on whether “category theory [will] make you a better programmer” and tuning in to online courses like Scambler’s.

It can’t be a coincidence that so many computer scientists are attending year-long or semester-long programs on Univalent Foundations and/or HoTT while a growing number of programmers are trying to learn category theory.  Milewski himself mentions Voevodsky briefly in his fourteenth chapter:

For all intents and purposes isomorphic sets are identical. Before I summon the wrath of foundational mathematicians, let me explain that the distinction between equality and isomorphism is of fundamental importance. In fact it is one of the main concerns of the latest branch of mathematics, the Homotopy Type Theory (HoTT). I’m mentioning HoTT because it’s a pure mathematical theory that takes inspiration from computation, and one of its main proponents, Vladimir Voevodsky, had a major epiphany while studying the Coq theorem prover. The interaction between mathematics and programming goes both ways.

I won’t speculate on the reasons for this synchronicity because I don’t know anything about programming and I discovered this literature less than an hour ago.  But I’m ready to believe that the interaction goes both ways and I suspect I’ll learn more about programming by watching Scambler’s course and reading Milewski’s book than I would by following the traditional route.

P.S.  Confusion goes both ways too.  The “red-blooded programmers” seem to be having trouble with the notation g°f for composition at around 13’40” of Scambler’s course:  why is the g on the left when the arrow representing g is on the right?  Why indeed?