𝝀 Categorical Semantics of Type Theory

• Categories with structures
• Universal properties
• Principle of duality

• Syntax and Semantics
• Categorical logic

• Cartesian closed categories
• Categorical semantics

Introduction

As software grows in size, programmers are looking for more disciplined software development methods. The research community has developed many useful tools to ensure program correctness. Model checking, static analysis, deductive verification based on program axiomatic semantics, etc. Although these techniques have been very successful in a variety of applications, most programmers do not benefit from them. The main reason is that programmers are unaware of these tools, and even if they do, they do not necessarily use them.

In contrast, type systems provide an easy way to think about programs and are widely supported by many languages. Using types has inherent advantages. First, types just reflect people's intuition about data structures. Second, types are a built-in feature of many programming languages that programmers have to deal with. A type checker checks for type consistency based on information gathered by the program. If an inconsistency occurs, the compiler will stop compiling at this point and print error.

Internally, however, exploring the underlying foundations of the type system is much more complex. Addressing this complexity requires a unified way to discuss different type theories and reveal their mathematical structures and internal relationships. In this article, we consider a common and effective method, categorical semantics.

Basic category theory

Formally, a definition in category theory consists of two parts: data and axioms. Data records what to manipulate and axioms record how to manipulate.

Definition 1 : A category $\mathcal{C}$ consists of :

• a collection of objects $Obj(\mathcal{C})$
• a collection of morphisms $Hom_\mathcal{C}(A, B)$, whose members denoted by $f : A \to B$, with $A, B \in Obj(\mathcal{C})$
• for morphisms $f : X \to Y$ and $g : Y \to Z$, the compopsed morphism $g \circ f : X \to Z$ (composition is also associative)
• an identity morphism $1_A : A \to A$ which satisfies that for any mprhism $f : X \to Y$ \[ 1_Y \circ f = f = f \circ 1_X \]

We can spot various categories by identifying their corresponding objects and morphisms and proving the axioms. For example, given any preorder set $P$, we let each $x \in P$ be an object and for each $x, y \in P$ such that $x \leq y$, is defined as a unique morphisme between them. Thus, the identity morphism corresponds to reflexivity of the preorder and composition corresponds to transitivity. The axioms are satisfied trivially: betwen any pair of objects, there is at most one morphism. Therefore all preorder sets form categories.

In the case of natural numbers, we have the following diagram (where nodes are objects and edges morphisms) :

So far, we are only concerned about sets and categories. Nonetheless, we can already build up a fair amount of complexity. Since category theory is constructed to study structures and a category is itself a structure, we can define the category of all small categories, $Cat$.

Definition 2 : A functor $F : \mathcal{C} \to \mathcal{D}$ from a category $\mathcal{C}$ to $\mathcal{D}$ has the following data:

• a mapping $F_0$ from objects in $\mathcal{C}$ to those in $\mathcal{D}$
• for $A, B \in \mathcal{C}$, a mapping $F_1$ from $Hom_\mathcal{C}(A, B)$ to $Hom_\mathcal{D}(F_0(A), F_0(B))$

Functors between small categories are morphisms in $Cat$. One example, is the identity functor: given a category $\mathcal{C}$, both $F_0$ and $F_1$ map an input to itself. Functor composition is done by composing $F_0$ and $F_1$. By letting the categories to be objects, we see the generality of category theory: it simply provides a common language for discussing various structures. We can push this idea further by considering functors as objects.

Given two functors $F, G : \mathcal{C} \to \mathcal{D}$, a natural transformation $\alpha : F \implies G$ between them has components as data, which map each object $X \in Obj(\mathcal{C})$ to a morphism $F(X) \implies G(X)$ in $\mathcal{D}$, denoted by $\alpha_X$, so that for each morphism $f : X \to Y$ in $\mathcal{C}$, the following diagram commutes (naturality condition) :

Here, we use a commutative diagram. When a diagram commutes, morphisms composed by different paths with the same end points are equal. In this case, the diagram represents the following equality:

It is quite easy to show that functors with natural transformations as morphisms do form a category. Identity morphisms are identity natural transformations, and the composition is the composition of components. Given three functors $F, G, H$ and two natural transformations $\alpha : F \implies G$ and $\beta : G \implies H$, the naturality of composition holds due to the outermost rectangle :

Two squares commute due to the naturality of $\alpha$ and $\beta$, and the rectangle commutes simply by composing the squares.

Categories with structures

Very often, we would want to know a little more about the category that we are working with. This is usually achieved by requiring some additional structures. For example, we can characterize cartesian producsts based on the following definition :

Definition 3 : A category $\mathcal{C}$ has binary cartesian products if it is equipped with additional data:

1. a mapping $\times$ from two objects to one
2. a mapping $\langle –, – \rangle$ of two morphisms, so that for each $f : X \to Y$ and $g : X \to Z$, $\langle f, g \rangle : X \to Y \times Z$
3. two morphisms $\pi_1 : X \times Y \to X$ and $\pi_2 : X \times Y \to Y$

which requires commutativity, i.e., for any morphism $f, g, \pi_1 \circ \langle f, g \rangle = f$ and $\pi_2 \circ \langle f, g \rangle$ and uniqueness, i.e., for any morphism $h : X \to Y \times Z, h = \langle \pi_1 \circ h, \pi_2 \circ h \rangle$

In a category with binary products, we obtain a product of any number of objects. It is then natural ot ask what can serve as a nullary product and this concept is precisely characterized by terminal objects. A terminal object in a category is a special object $\top$ so that for any object $X$, there must be a unique morphism $X \xrightarrow{!} \top$. With a terminal object, we are able to characterize a product of any number of objects.

A cartesian category is a category with a terminal object and all binary products. For example, for any object $X$, we have an isomorphism: \[ X \simeq X \times \top \] That is, there exists two morphisms $f : X \to X \times \top$ and $g : X \times \top \to X$, such that for $f \circ g = 1_{X \times \top}$ and $g \circ f = 1_X$.

$Cat$ and $Set$ (the category of sets) are examples of cartesian categories. It remains to show they both have terminal objects. The terminal object of $Set$ is the singleton set $\{ * \}$ for any element $*$. The terminal object of $Cat$ is the category $1$: a category with only one object and one morphism (which is necessarily the identity morphism of the only object).

Universal properties

In the previous section, we introduced tow structures: products and terminal obejcts. Both structures share a similar pattern in their definitions: a morphisms exsits uniquely for all morphisms (potentially with some conditions). This pattern is called a universal mappting property. Consider natural numbers as a preorder category. Given two numbers $m$ and $n$, $m \times n$ must be the « best » number which has morphisms into $m$ and $n$. Recall that $a \to b$ in a preorder category denotes $a \leq b$. That means $m \times n$ has to be the largest number that is smaller that both $m$ and $n$ and thus $\text{min}(m, n)$ ; otherwise, $m \times n$ would be a number $l > \text{min}(m, n)$ and smaller than both $m$ and $n$ which is impossible.

Every number must have a morphism into a terminal object, meaning that it is the biggest number of all, which does not exist for natural numbers. If we consider only natural numbers up to a fixed number $u$, then a terminal object does exist and it is $u$. Previously we showed the isomorphism $X \simeq X \times \top$, which corresponds to $m = \text{min}(m, u)$ in this case.

Using universal properties of products and terminal objects, we obtain a fact about many preorder categories without considering them specifically.

The principle of duality

When making mathematical statements, we often encounter terminologies that are somewhat the opposite to another: a set and its complement, maximum and minimum, supremum and infimum, and so on. In category theory, this phenomenon is captured by the principle of duality which is derived in the opposite category.

Definition 4 : The opposite category of a category $\mathcal{C}$, denoted by $\mathcal{C}^{op}$ has the same objects as $\mathcal{C}$. Morphisms in $\mathcal{C}^{op}$ are defined by flipping the directions of those in $\mathcal{C}$.

By applying duality to the diagram of a product, we obtain of the diagram in the opposite category, defining a coproduct. The definition of coproducts is also a universal property, whcih asserts the unique existence of a morphism $[f, g] : Y + Z \to X$ for $f : Y \to X$ and $g : Z \to X$.

Logic, Types and Categories

One important principle in type theory is perhaps the Curry-Howard isomorphism, which describes a connection between two previously separated field : logic and types. In logic, people think about what and how facts are concluded, while types are a concept in computer science, which emerges much later and naturally carries the notion of computation. It recently appeared that both areas are tightly connected: a program can represent a logical argument, and operations in logic find meaningful correspondences in program executions.

Syntax and Semantics

Generally, there are two approaches to understand or design a type system: the syntactic point of view and the semantic point of view. In the syntactic point of view, we inherit methods from logic and proof theory which focusd our attention on the syntactic structure of a type system. We study many important properties like subject reduction, cut elimination, subformula property, and many others, simply by looking at the syntax. One advantage of syntactic approaches is that the study is usually more direct and easier to understand semantic approaches as it is usually conducted via induction on some syntactic structures.

Semantic approaches in general are more powerful because they base the discussion of a type system on some mathematical models wich exhibits many useful properties. Thus one usually obtains more structures to work with than the mere syntax. One of the most impactful results from categorical semantics is probably monads which generalize many computations (including side-effectul ones).

Definition 5 : A monad of a category $C$ is an endofunctor $M : C \to C$ with two natural transformations $\eta : 1_C \to M$ and $\mu : M \circ M \to M$ such that the following axioms (that expresses identity and associativity) hold :

The following computations can be modelled by monads among others :

1. Stateful computations : We can consider a program states captured by a set of states $S$. In a stateful programming language like C or C++, a function receiving $A$ and returning $B$ implicitly involves a global state. This function can be modelled by \[ \begin{align*} \small M(A \to B) &= \small S \to ((A \to B) \times S) \\ & = \small (S \to (A \to B)) \times (S \to S) \end{align*} \] Namely, a stateful function has two parts, first computing $B$ based on the state and $A$ and second transforming the state.


2. Exceptions : Some programming languages like Java and C# implement exception mechanisms which allow programmers to introduce abrupt breaks of executions at any point of a program. This is again captured by monads by considering a set of exceptional states $E$. A function $A \to B$ with potential exceptions is modelled as $A \to M(B)$ where $M(B) = B + E$ and $+$ denotes disjoint unions. That is, this function either returns $B$ in a normal execution, or throws an exception by returning $E$.

Monads as a concept have been ubiquitous in functional programming community and adapted by languages like Haskell as a basic design principle for encapsulating computations. Indeed, it serves as a framework for functionnal programming languages to handle side effects while stay as pure as possible.
We can then imagine a type system in which monads are used to separate nonterminating computations from the terminating ones.

$\Gamma \vdash t : T$ is a judgement for a term which must reduce to a value and $\Gamma \vdash m \div T$ is for one representing a general computation. These judgements are represented by the following rules :

In this type system, the type former $C$ can be regarded as a monad. The required natural transformations can be defined as follows :

$C$ as a monad can be considered as a segregation of two different kinds of computations and provide a mathematical handle for investigation of this type system.

Categorical Logic

Compared to the long history of mathematical study of logic, categotical logic is relatively new but quite illuminating. In particular, it appears that logical constructs are fundamentally just adjoint functors. This result allows us to capture many constructs by using only one categorical concept.

Definition 6 : A pair of functors $L : \mathcal{C} \to \mathcal{D}$ and $R : \mathcal{D} \to \mathcal{C}$ are adjoint, written as $L \dashv R$, when the following isomorphism $X \in C$ and $Y \in \mathcal{D}$ \[ \mathcal{D}[L(X), Y] \simeq \mathcal{C}[X, R(Y)] \] is natural in $X$ and $Y$. Naturally in $X$ and $Y$ means that the following diagram commutes given $f : X' \to X$ and $g : Y \to Y'$ :

Consider the introduction rule of conjunctionsin natural deduction shown in Propositions as types, i.e., having $P \land Q$ is equivalent to having $P$ and $Q$. Consider now a category $\mathcal{C}$ where we regard $\Gamma \vdash P\ \texttt{true}$ as a morphism $\Gamma \implies P$ in the category. This allows to transform the introduction rule :

into:

The second formulation finds a pair of adjoint functors formulating logical conjunctions. Specifically, the adjunction is between $\mathcal{C} \times \mathcal{C}$ and $\mathcal{C}$. The left adjoint $L$ is defined by $L(X) = (X, X)$. The right adjoint $R$ is defined by conjunctions $R(P, Q) = P \land Q$. Thus, logical conjunctions are modelled by one pair of functors $L \dashv R$.

Another reason why we use adjoint functors to capture logical constructs to capture logical constructs is that adjoint functors provide a very strong correctness guarantee.

• Given two pairs of functors $L \dashv R$ and $L \dashv R'$, then $R$ and $R'$ are isomorphic functors.
• Given two pairs of functors $L' \dashv R$ and $L \dashv R$, then $L$ and $L'$ are isomorphic functors.

That is, fixing one side of the adjoint funcotrs, if the other side exists, it is uniquely determined up to isomorphism. That means first and foremost, that there is only one set of correct formulations of a logical construct, and all correct formulations can be shown equivalent. Second, no matter what formulation we pick at the end, the mathematical denotation of the logical cosntructs remains the same (up to isomoprhism).

Simply typed lambda calculus

Due to the principle of Propositions as types, we know that simply typed $\lambda$-calculus corresponds to intuitionistic logic. Essentially, it is defined by its syntax and judgements. Its syntax defines what items compose the language and the judgements specify what items are meaningful. The syntax is extremely easy: there are types, terms and contexts defined as follows.

We assume $\alpha$-equivalence which regards terms equal if they only differ by variable names. Whenever we refer to a name, we silently assume that the name is different from all used names. Contexts bind variables to types and the set of all variables in a context $\Gamma$ is its domain. A typing judgement has the form $\Gamma \vdash t : T$, meaning that the term $t$ has the type $T$ in the context $\Gamma$.

Following the style of natural deduction, there are two kinds of typing rules: introduction and elimination. The former describes how to construct a term of a type while the latter describes how to use a term of a type. Interpreting the unit type (the type having a unique element) as the trivial truth, the product types as conjunctions, and function types as implications, we can see that simply typed $\lambda$-calculus does correspond to propositional logic.

Cartesian closed categories

We have already discussed cartesian categories, which generally characterize finite products. In order to fully characterize simply typed $\lambda$-calclulus, we need an additional structure, exponentials:

Definition 7 : A cartesian category $\mathcal{C}$ has exponentials, if it has the following data:

1. for objects $X$ and $B$, an object $X^B$ as their exponential,
2. for any morphism $f : A \times B \to X$, a morphism $\tilde{f} : A \to X^B$
3. an evaluation morphism $\epsilon : X^B \times B \to X$

such that the following axioms hold :

1. commutativity : for $f : A \times B \to X$, $\epsilon \circ (\tilde{f} \times 1_B) = f$
2. uniqueness: for $g: A \to X^B$, $\epsilon \circ (g \times 1_B) = g$

Exponentials are used to characterize functions. The idea is to consider $X^B$ as an internal representation of a morphism $B \to X$. A cartesian closed category is a cartesian category with exonentials. One example of cartesian closed category is $Set$. We have already shown $Set$ is cartesian, so we just need to to show $Set$ has exponentials. With no suprise, given two sets $X$ and $B$, $X^B$ is the set of all functions from $B$ to $X$.

For $f : A \times B \to X$, $\tilde{f}$ is currying, defined where $a \in A$ and $b \in B$ as:

Finally, the evaluation morphism $\epsilon$ simply evaluates a function with an argument :

Categorial semantics

One crucial observation that can be made is that given a cartesian closed category $\mathcal{C}$, one can interpret typing judgements as its morphisms and equivalence judgements as equality between the morphisms.

More concretey, we can define an interpretation function from $\llbracket – \rrbracket$ from STLC to $\mathcal{C}$ so that :

• If $\Gamma \vdash t : T$, then there is a morphism $\llbracket \Gamma \vdash t : T \rrbracket : \llbracket \Gamma \rrbracket \to \llbracket T \rrbracket$

From this interpretation, we see that the types become corresponding categorical structures as promised by the semantics. Contexts are modelled by products of types. We then porceed to interpreting the well-formed types introduced earlier:

This interpretation ensures that the interpreted morphisms live in the Hom-set $\llbracket \Gamma \rrbracket \to \llbracket T \rrbracket$.