Lately, I have heard an interesting idea on theoretical computer science from a Chinese speaking chat group. The two tracks focus on different aspects of computer programming:
- Track A studies computation, which is a process happened between terms (it maps terms to terms). This can be viewed as a category, where objects are terms with morphisms interpreted as computation.
- Track B studies semantics of programs and types. There are well-established categorical semantics (for instance, the relationship between STLC and CCC, or MLTT and C-systems) which claims that types are objects of a category, where morphisms are interpreted as terms. One may argue that objects in C-systems are contexts, but we can imagine working in a democratic setting.
From that we can see a definition of a 2-category! The 2-category (denoted $\textsf{PL}$) has the following data:
- Objects (0-cells) $X\in \textsf{PL}$ are types.
- 1-morphisms (1-cells) $u\in \textsf{PL}(X, Y)$ are terms – think of it as $X \vdash u : Y$. Composition at this level corresponds to substitutions.
- 2-morphisms (2-cells) $f\in \mathcal C(u, v)$ (suppose $\mathcal C=\textsf{PL}(X, Y)$ to be a hom-category) are computations between terms. Composition at this level corresponds to – big step semantics maybe?
The coherence theorems follow very naturally from our intuition on programming languages! So, instead of studying the two layers separately, we may study it as a whole, and the 2-categorical point of view provides a suitable categorical framework.
Now, we can think about many 2-categorical constructions, such as pseudofunctors and 2-functors – translation between programming languages can be viewed as some of these functors, which preserves computation at different levels of precision.
For example, lax 2-functors from the terminal 2-category to $\textsf{PL}$ corresponds to (1-)monads. Since computation can be viewed as monads (but instead of “computation types”, our construction is on terms), we may think of computation as a lax 2-functor from the terminal 2-category.
Another example I can think of is that some compilers insert some simple coercions, such as erasure of generics, which is translated to non-generic code with safe casts inserted by compiler (I’m unsure about the validity of this particular example, though). These casts can be viewed as some sort of 1-cells, and maybe the translation can be defined as a lax 2-functor.
Studying programming languages from this perspective can be a good motivation to learn some 2-category theory.
