---
title: Typed Lambda Calculus and CCCs
module: Cartesian Closed Categories and Typed Lambda Calculus
moduleNumber: 8
lessonNumber: 2
order: 802
summary: >
  The typed lambda calculus and the cartesian closed category are two
  presentations of the same theory. Types become objects, terms with one free
  variable become arrows, product types become products, and function types
  become exponentials, with abstraction matching currying and application
  matching evaluation. Building the category of a lambda theory and the internal
  language of a category are mutually inverse up to equivalence.
topics: [Cartesian Closed Categories and Typed Lambda Calculus]
sources:
  - book: Barr & Wells
    ref: "§6.3 Typed λ-calculus"
  - book: Barr & Wells
    ref: "§6.4 λ-calculus to category and back; §6.5 Arrows vs. terms"
draft: false
---

The [cartesian closed category](/category-theory/cartesian-closed-lambda/cartesian-closed-categories)
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.[^bw-equiv]

## 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.[^bw-tl]

> **Definition (Typed lambda calculus).** A **typed lambda calculus** consists of
> types, terms, variables, and equations subject to the following.
>
> **Type formation.**
> - **TL-1.** There is a type $1$.
> - **TL-2.** If $A, B$ are types, so are $A \times B$ and $[A \to B]$.
>
> **Term formation.**
> - **TL-3.** There is a term $\ast$ of type $1$.
> - **TL-4.** For each type $A$ there are countably many variables $x^A_i$ of
>   type $A$.
> - **TL-5.** If $a \in A$ and $b \in B$, then $(a, b) \in A \times B$.
> - **TL-6.** If $c \in A \times B$, then $\mathrm{proj}_1(c) \in A$ and
>   $\mathrm{proj}_2(c) \in B$.
> - **TL-7.** (Application) If $a \in A$ and $f \in [A \to B]$, then the term
>   $f\,{}^{\backprime}a \in B$.
> - **TL-8.** (Abstraction) If $x$ is a variable of type $A$ and $\varphi(x) \in
>   B$, then $\lambda_{x \in A}\varphi(x) \in [A \to B]$.

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

The equations have the form $a =_X a'$, where $a$ and $a'$ are terms of the same
type and $X$ is a finite set of variables containing every variable free in $a$
or $a'$. 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.

> **Definition (Lambda equations).** The characteristic equations of the calculus:
> - **TL-15.** $\mathrm{proj}_1(a, b) =_X a$ and $\mathrm{proj}_2(a, b) =_X b$.
> - **TL-16.** $c =_X (\mathrm{proj}_1(c), \mathrm{proj}_2(c))$ for $c \in A
>   \times B$ (surjective pairing).
> - **TL-17.** ($\beta$) $\lambda_x\varphi(x)\,{}^{\backprime}a =_X \varphi(a)$,
>   when $a$ is substitutable for $x$ in $\varphi$.
> - **TL-18.** ($\eta$) $\lambda_{x \in A}(f\,{}^{\backprime}x) =_X f$, provided
>   $x$ is not free in $f$.
> - **TL-19.** ($\alpha$) $\lambda_{x \in A}\varphi(x) =_X \lambda_{x' \in
>   A}\varphi(x')$ under safe renaming of the bound variable.

The equation $a =_X a'$ does not assert that $a$ and $a'$ 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})$.

> **Definition (Syntactic category).** For a typed lambda calculus $\mathcal{L}$,
> the category $\mathcal{C}(\mathcal{L})$ has:
> - **objects:** the types of $\mathcal{L}$;
> - **arrows** $A \to B$: equivalence classes of terms of type $B$ containing at
>   most one free variable, of type $A$ (the variable need not actually occur).
>
> Two terms $\varphi(x)$ and $\psi(y)$ name the same arrow when they have the same
> type, their free variables have the same type, and $\varphi(x) =_{\{x\}}
> \psi(x)$ after renaming $y$ to $x$.

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'$ 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 $\varphi(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(\varphi)$, the term obtained by substituting $\varphi$ for the
free variable $y$ of $\psi$. Substitution is associative and the variable-term is
a two-sided unit, so this is a category.

> **Proposition (Syntactic categories are cartesian closed).** For any typed
> lambda calculus $\mathcal{L}$, the category $\mathcal{C}(\mathcal{L})$ is
> cartesian closed. The product of $A$ and $B$ is the type $A \times B$ with the
> projection terms, and the exponential is the type $[A \to B]$.

The cartesian closed structure is the obvious one. Given a term $\varphi(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 $\varphi(z, y)$ with $z$ of type $C$ and $y$
of type $A$; then the transpose $\lambda f$ is the class of $\lambda_z
\varphi(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.

| Lambda calculus | Cartesian closed category |
| --- | --- |
| type $A$ | object $A$ |
| term $\varphi(x)$ of type $B$, one free $x \in A$ | arrow $A \to B$ |
| type $1$, term $\ast$ | terminal object $1$ |
| product type $A \times B$ | product $A \times B$ |
| pairing $(a, b)$ | pair arrow $\langle a, b\rangle$ |
| projections $\mathrm{proj}_1, \mathrm{proj}_2$ | product projections $p_1, p_2$ |
| function type $[A \to B]$ | exponential $[A \to B]$ |
| abstraction $\lambda_x \varphi$ | currying $\lambda f$ |
| application $f\,{}^{\backprime}a$ | $\mathrm{eval} \circ \langle f, a\rangle$ |
| $\beta$ (TL-17) | $\mathrm{eval} \circ (\lambda f \times A) = f$ |
| $\eta$ (TL-18) | $\lambda(\mathrm{eval}) = \mathrm{id}_{[A \to B]}$ |
| substitution | composition |

> **Worked example (The term $(x, x)$ is the diagonal).** The pairing rule
> applied to a single variable, $x \mapsto (x, x)$, is a term of type
> $A \times A$ with one free variable $x$ of type $A$, hence an arrow
> $A \to A \times A$. Its projections are $\mathrm{proj}_1(x, x) = x$ and
> $\mathrm{proj}_2(x, x) = x$ by TL-15, both the identity term. So the arrow is
> $\Delta = \langle \mathrm{id}, \mathrm{id}\rangle$, the unique arrow into
> $A \times A$ whose two projections are both $\mathrm{id}_A$.

$$
% caption: The term $(x,x)$ of type $A \times A$ in one variable $x \in A$ names the diagonal $\Delta = \langle \mathrm{id}, \mathrm{id}\rangle$, whose projections both return the identity.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\node (a)  at (0,2.1) {$A$};
\node (aa) at (0,0) {$A \times A$};
\node (l)  at (-3.0,-2.1) {$A$};
\node (r)  at (3.0,-2.1) {$A$};
\draw[->, acc, thick] (a) -- (aa) node[midway, right=1pt, black] {diag};
\draw[->, thick] (aa) -- (l) node[pos=0.45, above left, black] {$p_1$};
\draw[->, thick] (aa) -- (r) node[pos=0.45, above right, black] {$p_2$};
\draw[->, thick] (a) to[bend right=38] node[midway, left, black] {id} (l);
\draw[->, thick] (a) to[bend left=38] node[midway, right, black] {id} (r);
\end{tikzpicture}
$$

## 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.

$$
% caption: $\beta$ (left) says evaluating a curried arrow recovers it; $\eta$ (right) says currying evaluation returns the identity on the exponential.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\small]
\definecolor{acc}{HTML}{4A6FA5}
% beta triangle
\node (ca) at (0,2.0) {$C \times A$};
\node (ea) at (0,0) {$B^A \times A$};
\node (b)  at (3.0,0) {$B$};
\draw[->, acc, thick] (ca) -- (ea) node[midway, left, black] {$\overline{f} \times A$};
\draw[->, thick] (ea) -- (b) node[midway, below, black] {$\mathrm{ev}$};
\draw[->, acc, thick] (ca) -- (b) node[midway, above right, black] {$f$};
\node at (1.5,2.6) {beta};
% eta triangle
\begin{scope}[xshift=6.4cm]
\node (e1) at (0,2.0) {$B^A$};
\node (e2) at (0,0) {$B^A$};
\node (ev) at (3.0,0) {$B^A$};
\draw[->, acc, thick] (e1) -- (e2) node[midway, left, black] {$\mathrm{id}$};
\draw[->, thick] (e2) -- (ev) node[midway, below, black] {$\overline{\mathrm{ev}}$};
\draw[->, acc, thick] (e1) -- (ev) node[midway, above right, black] {$\mathrm{id}$};
\node at (1.5,2.6) {eta};
\end{scope}
\end{tikzpicture}
$$

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 \varphi$ to $a$ returns $\varphi(a)$. On the right, $\lambda(\mathrm{eval})
= \mathrm{id}$ is TL-18: the abstraction $\lambda_x (f\,{}^{\backprime}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.

> **Theorem (Language–category equivalence).** Let $\mathcal{C}$ be a cartesian
> closed category with internal language $\mathcal{L} = \mathcal{L}(\mathcal{C})$.
> Then $\mathcal{C}(\mathcal{L})$ is
> [equivalent](/category-theory/foundations/natural-transformations) to
> $\mathcal{C}$. Symmetrically, building the internal language of the category of
> a lambda theory returns a lambda theory equivalent to the original.

$$
% caption: The category of a lambda theory and the internal language of a category are mutually inverse up to equivalence, so CCCs and typed lambda theories present the same mathematics.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\node[draw, thick, minimum width=30mm, minimum height=12mm] (L) at (0,0) {lambda theory $\mathcal{L}$};
\node[draw, acc, thick, minimum width=30mm, minimum height=12mm] (C) at (6.6,0) {cartesian closed $\mathcal{C}$};
\draw[->, acc, thick] (L.north east) to[bend left=20] node[midway, above, black] {build the syntactic category $\mathcal{C}(\mathcal{L})$} (C.north west);
\draw[->, thick] (C.south west) to[bend left=20] node[midway, below, black] {read the internal language $\mathcal{L}(\mathcal{C})$} (L.south east);
\end{tikzpicture}
$$

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

$$
f(x, y) = x^2 + 3xy.
$$

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

$$
f = \lambda_{x \in \mathbf{N}}\,\lambda_{y \in \mathbf{N}}\; x^2 + 3xy,
$$

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

$$
f = p_1^2 + 3\,p_1 p_2,
$$

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.[^bw-arrterm]

> **Worked example (Wiring $x^2 + 3xy$ as arrows).** Fix the multiplication and
> addition arrows $m, s : \mathbf{N} \times \mathbf{N} \to \mathbf{N}$ and the
> constant $3 : 1 \to \mathbf{N}$. Each variable becomes a projection off
> $\mathbf{N} \times \mathbf{N}$:
> - $x^2$ is $m \circ \langle p_1, p_1\rangle$, the first coordinate multiplied
>   by itself;
> - $xy$ is $m \circ \langle p_1, p_2\rangle$;
> - $3xy$ is $m \circ \langle 3 \circ {!},\; m \circ \langle p_1, p_2\rangle\rangle$,
>   where $! : \mathbf{N} \times \mathbf{N} \to 1$ is the unique map to the
>   terminal object.
>
> Adding the two summands gives
> $$
> f = s \circ \bigl\langle\, m \circ \langle p_1, p_1\rangle,\;\; m \circ \langle 3 \circ {!},\; m \circ \langle p_1, p_2\rangle\rangle \,\bigr\rangle,
> $$
> the arrow named by $\lambda_x \lambda_y\, x^2 + 3xy$. No variable is mentioned,
> and the two multiplications $m \circ \langle p_1, p_1\rangle$ and $m \circ
> \langle p_1, p_2\rangle$ share no data, so they may be evaluated independently.

$$
% caption: The arrow behind $x^2 + 3xy$: projections copy the two inputs, one multiplier forms $x^2$ and another forms $xy$, a constant scales $xy$ by three, and the adder returns the result.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\node (in) at (0,0) {$\mathbf{N}^2$};
\node (m1) at (3.7,1.6) {mult};
\node (m2) at (3.7,-1.2) {mult};
\node (c3) at (3.7,-2.7) {const $3$};
\node (m3) at (6.6,-0.7) {mult};
\node (add) at (9.0,0.6) {add};
\node (out) at (11.4,0.6) {$\mathbf{N}$};
\draw[->, thick] (in) to node[midway, above left, black] {$p_1$, $p_1$} (m1);
\draw[->, thick] (in) to node[midway, below left, black] {$p_1$, $p_2$} (m2);
\draw[->, acc, thick] (m1) to node[midway, above right, black] {$x^2$} (add);
\draw[->, thick] (m2) -- (m3);
\draw[->, thick] (c3) -- (m3);
\draw[->, acc, thick] (m3) to node[midway, below right, black] {$3xy$} (add);
\draw[->, acc, thick] (add) -- (out) node[midway, above, black] {$f$};
\end{tikzpicture}
$$

The arrow form handles repeated variables explicitly. In the
term $\varphi = (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}\varphi(x) =
  \lambda_{y \in A}\varphi(y)$, hedged in the syntax by "provided $y$ is not free
  in $\varphi$," 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](/category-theory/cartesian-closed-lambda/fixed-points-and-recursion):
that turns on which arrows of a cartesian closed category admit fixed points.

[^bw-equiv]: **Barr & Wells**, _Category Theory for Computing Science_, §6.4 — the equivalence of typed lambda calculi and cartesian closed categories, following Lambek and Scott.
[^bw-tl]: **Barr & Wells**, §6.3.1–6.3.3 — the definition of a typed lambda calculus: type/term formation rules TL-1 through TL-8 and the equations TL-9 through TL-19, with free/bound variables and substitution.
[^bw-arrterm]: **Barr & Wells**, §6.5.1–6.5.3 — the $x^2 + 3xy$ example rendered as a term and as an arrow, the generalized diagonal for repeated variables, and the advantages of the variable-free categorical presentation.