(Part 1 of a series.)
Category theory is treated with mysticism in much of the programming languages community. Functional programmers tout the relationship between categories and their favorite languages, but fail to explain its utility. Type theorists wonder why mathematicians prefer categories to types. Everyone else wonders what categories are.
There are many good texts on category theory (Mac Lane, Awodey, Adamek et al) and type theory (Pierce, Harper); there are also many texts relating the two (Crole, Pitts, Lawvere).
What’s lacking, I think, is motivation. It’s hard to excitedly explain the relationship between two complex frameworks, without first explaining where either comes from. I would like to approach them simultaneously and organically, in an attempt to motivate both, and describe why they comprise a very useful view of the world (of mathematics and logic—is there another one?).
To vastly oversimplify, my main point is that both espouse representation independence: they encourage us to understand structures through, and define them by, their interactions with other structures, not by their internal workings.
In the case of mathematics, we typically choose a particular kind of structure (sets, groups, topological spaces, etc.) and then study instances of that structure, and the structure-preserving maps between them (functions, group homomorphisms, continuous functions). Then,
- by defining structures by their interfaces, not their representations, we can easily rule out constructions which don’t respect an interface.
- by abstracting away from one particular kind of structure, we can seamlessly port some constructions to other, entirely different structures.
- by considering structure abstractly, we have a natural language for discussing (structure-preserving map)-preserving maps between different kinds of structures.
(Perhaps I got carried away at the end there.) In the case of programming languages, we often seek these same properties, approximately in the guise of polymorphism, abstraction, and higher-order functions.
In an indefinite series of blog posts starting here, I will try to explain the high points of the categorical and type-theoretic Weltanschauung, starting from the most basic case, and gradually filling in more details until I give up.
I have no intention of being thorough in either content or rigor; instead, I hope to convince you that these abstractions, while complex at first sight, are in fact quite natural and universal. This tale, as I tell it, was first observed by Lawvere, and has since been elaborated by many categorical logicians and type theorists.