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?

Jon AwbreyThere are some category/computation folk who “do it right”, Ernie Manes being a notable one. I once wrote a page somewhere on

Propositions As Types Done Rightand discovered how deadset some folks are on doing it, well, the other way.LikeLike

printhead1436My favorite sentence on the internet this week: “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. “

LikeLike

Trent KFYI, Learn You A Haskell for Great Good ( http://learnyouahaskell.com/chapters ) & Oregon Programming Languages Summer School videos ( https://www.cs.uoregon.edu/research/summerschool/summer15/ ) are both excellent resources if you’re curious to learn more about programming & how it interacts w/ type and category theory.

(& this twitter account is a hilarious take on how CEOs see programmers who are a little too obsessed w/ haskell & cat theory: https://twitter.com/HaskellCEO )

LikeLike

Franklin Chen“Why is the g on the left when the arrow representing g is on the right? Why indeed?”

I learned algebra in college from Herstein’s book, which insisted on using left-to-right composition rather than right-to-left. I still believe that is the “correct” order and prefer to use left-to-right composition in my code (whether it’s called “>>>” or “andThen” or any number of other variants common in various languages).

LikeLike