How to convert lambda expressions into morphisms in a Cartesian Closed Category?

Question

I'm trying to understand how named variables relate to function composition.

So, in a program, it's useful to have named intermediate variables, so you can use them multiple times in the future:

int x = 0;
int y = g(x);
int z = h(x, y);
return bar(x, y, z);

It's straightforward to convert this to a lambda expression:

$$\lambda x[\lambda y[\lambda z[bar\ x\ y\ z] (h\ x\ y)] (g\ x)]\ 0$$

My question: Simply typed lambda calculus is just a notation for Cartesian Closed Categories right? It's an internal language?

If so then there should be a way to convert the lambda expression into an expression for a morphism in a Cartesian Closed Category right? If that's all true, how do I do that?

Answer 1

Yes, this is correct. The general construction is: the intermediate terms in the abstract syntax tree are simply typed lambda calculus terms with some free variables of predetermined types $x_1 : X_1, \ldots, x_n : X_n$. If this term $\varphi$ is a valid expression with result type $Y$, then we can form an interpretation $[\varphi] \in \operatorname{Hom}(X_1 \times \cdots \times X_n, Y)$. This interpretation is defined recursively as follows:

• For a term which is one of the free variables $x_i$, the interpretation is the projection $\pi_i \in \operatorname{Hom}(X_1 \times \cdots \times X_n, X_i)$.
• For a term which is an application $f \, x$ where $f$ has result type $Y^X$ and $x$ has result type $X$, we form the morphism $([f], [x]) \in \operatorname{Hom}(X_1 \times \cdots \times X_n, Y^X \times X)$ and then compose with the evaluation morphism $\operatorname{ev} \in \operatorname{Hom}(Y^X \times X, Y)$.
• For a term which is an abstraction $\lambda (x : X) . \psi$ where $\psi$ has result type $Y$, then $[\psi] \in \operatorname{Hom}(X \times X_1 \times \cdots \times X_n, Y)$. We use the exponential object adjunction to get a morphism in $\operatorname{Hom}(X_1 \times \cdots \times X_n, Y^X)$.
• For a pair term $(x, y)$ where $x$ has result type $X$ and $y$ has result type $Y$, the interpretation is $([x], [y]) \in \operatorname{Hom}(X_1 \times X_n, X \times Y)$.
• For a projection term $\operatorname{fst}(p)$ or $\operatorname{snd}(p)$ where $p$ has result type $X \times Y$, the interpretation is $\pi_1 \circ [p]$ respectively $\pi_2 \circ [p]$. (Alternately, if your version of the language has a destructuring let term $\mathbf{let}~(x,y) := p~\mathbf{in}~\psi$ as the fundamental notion of breaking down an ordered pair, where $[p] \in \operatorname{Hom}(X_1 \times \cdots \times X_n, X \times Y)$ and $[\psi] \in \operatorname{Hom}(X_1 \times \cdots \times X_n \times X \times Y, Z)$, then the interpretation of that destructuring let will be formed by composing $[\psi]$ with $(\operatorname{id}, p) \in \operatorname{Hom}(X_1 \times \cdots \times X_n, X_1 \times \cdots \times X_n \times X \times Y)$.)
• For the term $()$ with result type 1, the interpretation is the unique morphism in $\operatorname{Hom}(X_1 \times \cdots \times X_n, 1)$.

In your example, based on the pseudocode given, I will assume that the free variables are of type $0 : \mathbb{Z}$, $g : \mathbb{Z}^{\mathbb{Z}}$, $h : (\mathbb{Z}^{\mathbb{Z}})^{\mathbb{Z}}$, $bar : ((\mathbb{Z}^{\mathbb{Z}})^{\mathbb{Z}})^{\mathbb{Z}}$. (Although, presumably you are thinking of the predefined element $0 \in \mathbb{Z}$, which at least in $\mathbf{Set}$ is equivalent to a morphism in $1 \to \mathbb{Z}$ sending the unique element of 1 to 0. Similarly, you might be thinking of $h$ as a morphism $\mathbb{Z} \to \mathbb{Z}^{\mathbb{Z}}$, which is equivalent to a morphism $1 \to (\mathbb{Z}^{\mathbb{Z}})^{\mathbb{Z}}$. For these cases, you can either do the above construction and then at the end, compose with the morphism $(g,h,bar,0) \in \operatorname{Hom}(1, \mathbb{Z}^{\mathbb{Z}} \times \cdots \times \mathbb{Z})$. Or, you can consider an extended version of the internal language with constant symbols for these objects, whose interpretations are formed by composing the unique morphism in $\operatorname{Hom}(X_1 \times \cdots \times X_n, 1)$ with the corresponding morphism in $\operatorname{Hom}(1, ?)$.)

So in your example, let us take the option of extending the internal language with constant symbols for $g,h,bar,0$. Then one of the innermost terms will be $bar\,x$ where the free variables are $x, y, z : \mathbb{Z}$. Now $[bar] \in \operatorname{Hom}(\mathbb{Z}^3, ((\mathbb{Z}^{\mathbb{Z}})^{\mathbb{Z}})^{\mathbb{Z}})$ and $[x] = \pi_1 \in \operatorname{Hom}(\mathbb{Z}^3, \mathbb{Z})$. We combine those as above to get a morphism in $\operatorname{Hom}(\mathbb{Z}^3, (\mathbb{Z}^{\mathbb{Z}})^{\mathbb{Z}})$. Similarly, we can combine this with $[y] = \pi_2 \in \operatorname{Hom}(\mathbb{Z}^3, \mathbb{Z})$ to get $[bar\,x\,y] \in \operatorname{Hom}(\mathbb{Z}^3, \mathbb{Z}^{\mathbb{Z}})$; and also similarly, we form $[bar\,x\,y\,z] \in \operatorname{Hom}(\mathbb{Z}^3, \mathbb{Z})$. Then $[\lambda (z : \mathbb{Z}) | bar\,x\,y\,z]$ is the corresponding morphism in $\operatorname{Hom}(\mathbb{Z}^2, \mathbb{Z}^{\mathbb{Z}})$; and so on.