2
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.