Homotopy Type Theory
I’ve recently been pointed to the Homotopy Type Theory book. It focuses on an extremely interesting research area, namely the connection between homotopy theory and type theory. Type theory is something that most programmers should have at least heard about. Recent developments, such as Idris, have probably brought type theory and especially dependently typed languages into attention.
Homotopy theory, on the other hand, seems to be something rather unrelated: it studies homotopy, which originates from topology. Topology is about things like shapes and spaces, about connections between points, deforming objects and related ideas.
The Homotopy Type Theory book draws a number of beatiful and interesting connections between these fields. It immediately reminded me of “Seemingly impossible functional programs” (here and here), which is also absolutely recommended to read. However, Homotopy Type Theory goes much deeper than this. The book describes an alternative way of providing foundations for mathematics (such as Zermelo–Fraenkel set theory). Now you might ask: why do we need that? The answer is: Homotopy Type Theory can be interpreted constructively. You could use ZFC (i.e., Zermelo-Fraenkel + the axiom of choice) to prove some proposition. But that proof wouldn’t necessarily be constructive. That is, you can proof the existence of some mathematical object but at the same time you might still be unable to actually compute that object. Whan you program something, you are however interested in actually constructing a mathematical object (such as, say, a red-black tree). Doing constructive proofs enables you to verify the correctness of your algorithm and at the same time to extract running code out of that proof.
If you are interested in type theory (or homotopy theory), I’d recommend that book to you. If you’re not, I’d still recommend it. Oh, and did I mention that you can get the PDF version for free?