In category theory, you often think something is a certain type of thing but actually it turns out to also be a different type of thing. In a first introduction, it appears that functors are somehow one level higher than morphisms, because functors map morphisms to morphisms. Similarly, natural transformations should be one level higher than functors because they map functors to functors. This is true if you want to be closed-minded and sad. But it ignores a beautiful thing about category theory: it is so abstract and general that it can do category theory about itself.

As math gets more advanced, the things you prove get dumber and dumber. In Calculus, you prove really cool things like “This sum of infinitely many real numbers equals a finite number!” Then you take Analysis where you have to explain “What is infinity?” and “What is a real number?” and “What is equals?”

The answer to the last question, as it turns out, is, “Nobody knows.”

Word to the Wise

The secret to PL theory is that we take a collection of very common symbols, strip them of their meaning entirely, and then build it back from the ground up. For the rest of this post, to protect your sanity, kindly forget everything you think you know about $\equiv$ and $=$. We may as well use 🐒 and 🪕.

Call-by-push-value (CBPV) is a programming language that subsumes call-by-name (CBN) and call-by-value (CBV) semantics, making it useful to reason about effectful computations. But why is it called that?

Call-by-name and call-by-value

First, we should motivate CBPV by explaining what CBN and CBV are. To start out with, we will only consider the basic lambda calculus with no effects. The important rule here when expressing the lambda calculus’s semantics is $\beta$-reduction: How do we apply a function?

There are two important aspects in the study of programming languages as formal mathematical objects: syntax (or statics) and semantics (or dynamics). The syntax specification includes an (often inductive) definition of well-formed terms in the language, as well as, in typed languages, a specification of the typing judgment. There is plenty of interesting stuff to study in syntax, but this blog post is about semantics. Semantics is about assigning actual meaning to terms in the language. This is important for reasoning about, for example, correctness, equivalence, or termination. Depending on your language and use case, there are many different ways to specify the semantics. This post is a survey of what I have experienced to be the most common ones.

The problem with being self-taught in PLs is that I sort of learned everything at the same time, which means I did not get a good sense of what things fall in what categories. In this post I seek to determine, once and for all, what is type theory and what is not. To do that, we’re going to back it way up and start at the very beginning.

Logic

It’s easier to begin to answer this question with what is not type theory. In other words, some of the things that I know about typing systems are just true of logic in general.

I recently began re-reading Gödel, Escher, Bach and was intrigued by the MU puzzle, which is Hofstadter’s introduction to formal systems. The puzzle is this: the MIU language consists of the “axiom” MI as well as all strings constructed according to the following four rules.

1. If you have the string xI, then you can construct the string xIU (where x is any string of any length).
2. If you have Mx, then you can construct Mxx.
3. If III appears anywhere in a string, you can replace it with U.
4. If UU appears anywhere in a string, you can remove it.

Can you ever construct the string MI?