# Mapping a free variable of type A to a cartesian closed category

In From Lambda Calculus to Cartesian Closed Categories, the author explains the interpretation of lambda calculus in cartesian closed category and at one point he explains how a term representing a free variable of type A is mapped to the cartesian closed category as follow:

 [Γ x:A :- x:A] = π2 : ([Γ ] × [A]) → [A]

(A term which is a free
variable of type A is an arrow from the product of Γ and the type object A to A;
That is, an unknown value of type A is some arrow whose start point will be
inferred by the continued interpretation of gamma, and which ends at A.
So this is going to be an arrow from either unit or a parameter type to A -
which is a statement that this expression evaluates to a value of type A.)


I appreciate if someone can elaborate further on what the author means, perhaps with an example, since I am a newbie to category theory.

It's not clear exactly what your confusion is, so I'll try to explain the example more clearly, and you reply in the comments if something's still not apparent.

In the interpretation of the simply-typed $$\lambda$$-calculus in a cartesian-closed category, contexts $$\Gamma$$ and types $$A$$ are interpreted as objects $$⟦\Gamma⟧$$ and $$⟦A⟧$$ (types being equivalent to one-variable contexts), while a term $$\Gamma \vdash t : A$$ is interpreted as a morphism $$⟦t⟧ : ⟦\Gamma⟧ \to ⟦A⟧$$.

Context extension is represented by taking the product in the cartesian-closed category, that is: $$⟦\Gamma, x : A⟧ = ⟦\Gamma⟧ \times ⟦A⟧$$. We want to form the projection of the variable $$x : A$$, which is represented by a morphism $$⟦x⟧ : ⟦\Gamma, x : A⟧ \to ⟦A⟧$$, which by definition is a morphism $$⟦x⟧ : ⟦\Gamma⟧ \times ⟦A⟧ \to ⟦A⟧$$. There's one obvious choice here: to project the second component of the product. Taking $$⟦x⟧ = \pi_2$$ gives us a term of the correct type and it satisfies the expected properties.

In general, contexts (represented by lists of variables in the type theory) are represented by products of types in the cartesian-closed category, and the term corresponding to the $$i^\text{th}$$ variable is given by the $$i^\text{th}$$ projection from the product, $$\pi_i$$.

It might help to see explicit algorithms to compile the Lambda calculus to Cartesian closed categories.

A simple algorithm threads an environment through and looks up variables using a sequence of fst and snd

1. Start with an expression such as [lam f. lam x. f x] and an empty stack of variables.
2. When you reach a binder turn it into a currying combinator and add the variable to a stack curry [lam x. f x] and [f] and then curry (curry [f x]) and [f, x]
3. Function application is compiled to uncurry f . (fanout id x) so we get curry (curry (uncurry [f] . fanout id [x]))
4. When you reach a variable look it up in the stack. f is the zeroth variable here.
5. Replace the nth variable with a sequence of fst and n snds referring to the variable. So we get curry (curry (uncurry fst . fanout id (fst . snd)))

This works for cs theory but is suboptimal and unreadable.

More practically one iteratively removes variable bindings without passing through an environment or first compiles to a form intermediate between closed Cartesian categories and the lambda calculus.