Typed Lambda Calculus and CCCs

The cartesian closed category was built to model functions of several variables: products for tupling, exponentials for currying, evaluation for application. The typed lambda calculus is a syntax for exactly the same operations, written with variables and binders instead of arrows and composites. The two are equivalent, and the equivalence is constructive: a lambda theory generates a category, a category has an internal language, and the two constructions undo one another.¹

The typed lambda calculus

A typed lambda calculus is a formal theory of four kinds of syntactic object: types, terms, variables, and equations. Every term $a$ has a type $A$, written $a\in A$. The type-forming and term-forming rules below are the minimum a typed lambda calculus must contain; a given theory may add further types, terms, and equations on top.²

The notation $\phi (x)$ marks a term that may contain the variable $x$; $\phi (a)$ is the result of substituting $a$ for every free occurrence of $x$. The application term $f{}^{‵}a$ is $f$ applied to $a$; the backtick is usually dropped, writing $fa$. A variable occurrence is bound in ${\lambda }_x\phi (x)$ and free otherwise; a term is closed if no variable is free in it.

The equations have the form $a{=}_X{a}^{\prime }$, where $a$ and $a^{\prime }$ are terms of the same type and $X$ is a finite set of variables containing every variable free in $a$ or $a^{\prime }$. The equality is a congruence (TL-9 through TL-14 make ${=}_X$ reflexive, symmetric, transitive, and compatible with pairing, projection, application, and abstraction). The content is in the last five rules.

The equation $a{=}_X{a}^{\prime }$ does not assert that $a$ and $a^{\prime }$ are identical strings; two terms are identical only if they are literally the same. It asserts that in every interpretation of the calculus the two terms must denote the same thing. The pair TL-15/TL-16 says the product type behaves like a product; the pair $\beta$/$\eta$ says the function type behaves like a space of functions.

The category of a lambda theory

From a typed lambda calculus $\mathcal{L}$ one builds a category $\mathcal{C}(\mathcal{L})$.

Equivalence classes are needed because any two variables of the same type must name the same arrow — the identity. A variable $x$ of type $A$, read as a term of type $A$ with one free variable $x$ of type $A$, is the identity arrow $A\to A$; choosing a different variable $x^{\prime }$ of type $A$ must not change the arrow, so the two terms are identified. Because a term of type $1$ is equated to $\ast$ by TL-10, the type $1$ becomes a terminal object.

Composition is substitution. If $\phi (x)$ of type $B$ names an arrow $A\to B$ and $\psi (y)$ of type $C$ names an arrow $B\to C$, their composite is the class of $\psi (\phi )$, the term obtained by substituting $\phi$ for the free variable $y$ of $\psi$. Substitution is associative and the variable-term is a two-sided unit, so this is a category.

The cartesian closed structure is the obvious one. Given a term $\phi (x)$ with $x$ of type $C\times A$ naming an arrow $f:C\times A\to B$, use TL-15 to substitute $(z,y)$ for $x$, getting $\phi (z,y)$ with $z$ of type $C$ and $y$ of type $A$; then the transpose $\lambda f$ is the class of ${\lambda }_z\phi (z,y)$. Uniqueness of the cartesian closed structure means no separate verification of the exponential is required beyond exhibiting it.

The construction turns each term-forming rule into a piece of categorical structure, and each characteristic equation into a categorical law.

Beta and eta as categorical equations

The two characteristic function-type equations are the two triangle-shaped laws of the exponential. The $\beta$ rule is the defining equation of currying, and the $\eta$ rule is its uniqueness clause stated backwards.

Here $\overline{f}$ again denotes the transpose $\lambda f$. On the left, $\mathrm{eval}\circ (\lambda f\times A)=f$ is TL-17: applying the abstraction ${\lambda }_x\phi$ to $a$ returns $\phi (a)$. On the right, $\lambda (\mathrm{eval})=\mathrm{id}$ is TL-18: the abstraction ${\lambda }_x(f{}^{‵}x)$ is $f$ itself. The $\alpha$ rule TL-19, renaming a bound variable, has no categorical content at all: after translation there are no variables to rename, so the two sides are literally equal.

The internal language and the round trip

The reverse construction reads a category as a syntax. Given a cartesian closed category $\mathcal{C}$ with chosen finite products, its internal language$\mathcal{L}(\mathcal{C})$ is the typed lambda calculus whose types are the objects of $\mathcal{C}$, with variables of each type, and with terms and equations generated by TL-3 through TL-19. The two constructions are inverse up to equivalence.

The equivalence is why either formalism may be used and translated to the other without loss. A construction that is awkward as syntax (substitution under binders, variable capture) may be clean as arrows (composition), and vice versa.

Arrows against terms

The two presentations describe the same function differently. Consider the polynomial $f:\mathbf{N}\times \mathbf{N}\to \mathbf{N}$ given by

In the typed lambda calculus this is written almost as in ordinary mathematics, with explicit variables and binders,

whereas categorically it is a composite of product projections, a diagonal to duplicate arguments, multiplications, and an addition, which condenses to

reading $p_1,p_2$ for the projections that the variables $x,y$ named. The only surface difference on this example is that the arrow form writes $p_1,p_2$ where the term form writes $x,y$. The deeper difference is emphasis: the term is a formula for the result, the arrow is a computation process, and the arrow form exposes that the two multiplications may run in parallel.³

The arrow form handles repeated variables explicitly. In the term $\phi =(a,b)$, a variable free in both $a$ and $b$ must not be duplicated into two independent inputs; the categorical translation inserts a generalized diagonal on the shared variables. The single-variable case is the diagonal above: $(x,x)$ is $\Delta$, not the identity on $A\times A$, whereas $(x,y)$ with distinct $x,y$ of type $A$ is the identity $A\times A\to A\times A$. Distinct variables of the same type stay distinct inputs; the same variable used twice is one input fed forward.

Strengths of each presentation

• The categorical form has no variables. There is nothing to rename, so the clash of variables — the source of the side conditions on $\alpha$, $\beta$, and $\eta$ — cannot arise. The rule ${\lambda }_{x\in A}\phi (x)={\lambda }_{y\in A}\phi (y)$, hedged in the syntax by "provided $y$ is not free in $\phi$," becomes the identically true $\lambda f=\lambda f$ once the variables are gone.
• Composition is built in. An arrow is a composite by construction, so the full apparatus of commutative diagrams and the theorems of category theory apply directly to programs written this way.
• The lambda form is closer to practice. Variables and binders match how functions are written and read, and substitution is the familiar operation of plugging in an argument.

The equivalence means neither presentation is primary. A cartesian closed category is a variable-free account of a typed functional language, and a typed lambda calculus is a syntax with variables for a cartesian closed category. Neither, on its own, provides recursion: that turns on which arrows of a cartesian closed category admit fixed points.