Relation between Cartesian closed category and Lambda Calculus

Question

I am programmer (from the object oriented world) and currently getting my head around functional programming. I was looking to get some basics right.

I understand what category theory and lambda calculus try and tell . I did read that lambda calculus can be modelled in any Cartesian closed category. and this is the how the 2 ideas can combine. But this is where i lost my way.

1) What is a Cartesian closed category ? (dint understand the mathematical semantics given , so wanted to know in simple English with some examples if possible). 2) How can Lambda calculus express this Cartesian closed category?

Answer 1

In imperative programming there is a tendency to distinguish between data and methods, whereas in functional programming, for example, they are identical. A closed category is a category that makes this identification: hom-sets (methods) correspond to certain objects (data). More concretely, the category is closed if it has a binary operation on objects $(X,Y) \mapsto Y^X$ such that it is actually the data version of methods: $$∀ X, Y, Z \;\;•\;\; (Z ⊕ X ⟶ Y) ≅ (Z ⟶ Y ^ X) \;\text{ natural in } Z, Y$$

The Cartesian part says that we can form any finite record ---in the programming sense. That is, if we have $n$ records of interest $R_1, \ldots, R_n$ then we can amalgamate them into one record $\Pi_{i \in 1..n} R_i$ and that this is their product means that any function/method to it is precisely $n$ methods to the individual factors! $$ \forall X \;\bullet\; (X \to \Pi_{i \in 1..n} R_i) \cong \Pi_{i \in 1..n} (X \to R_i) $$ The left-hand $\Pi$ is the object in the category, while the right-hand $\Pi$ is the usual set-theoretic. The case $n = 0$ gives us the empty-tuple aka the terminal object. With this and the ability to construct a product of two records, we can construct all finite products ---this is the usual presentation of cartesian.

Defining type := object, these together say that: if a,b are types then (a -> b), a x b, and 1 are all types, which are the usual type-constructions expected when working in type theory.

Hope this help :-)

Answer 2

I see that this question has an already accepted answer. Nonetheless I would like to give an alternative answer: sometimes seeing things from different perspective can help getting a better understanding of the subject.

There are many possible definitions/characterization of cartesian closed category (CCC in what follows), one of them is the following.

A CCC is a category $\mathbf C$ with:

1. an object $1 \in \mathbf C$ such that for each object $X \in \mathbf C$ there is one and only one morphism $t \colon X \to 1$ (you can think of $1$ as a generalization of the singleton set, the set with only one element)
2. for every pair of object $X$ and $Y$ you have an object $X \times Y$ with two projection morphisms $$\pi_X \colon X \times Y \to X \ \pi_Y \colon X \times Y \to Y$$ and an operation, called pairing, that for every pair $(f,g) \in \mathbf C[T,X] \times \mathbf C[T,Y]$ gives you a morphism $$\langle f,g \rangle \in \mathbf C[T,X \times Y]$$ with the requirement that $\pi_X \circ \langle f,g\rangle=f$ and $\pi_Y \circ \langle f,g \rangle=g$
3. for each pair of objects $X$ and $Y$ an object $Z^Y \in \mathbf C$ with a morphism $\epsilon \colon Z^Y \times Y \to Z$ such that the mapping $$\mathbf C[T,Z^Y] \to \mathbf C[T \times Y,Z]$$ $$f \colon T \to Z^Y \mapsto \epsilon \circ (f\circ \pi_T, \pi_Y) \colon T \times Y \to Z$$ is a bijection.

If you reguard a category as some sort of generalized system of types and function between them then:

1. the object $1$ become the unit type, the type with only one element, and the unique function $t \colon T \to 1$ is the constant function;
2. for each pair of objects/types $X$ and $Y$, the object $X \times Y$ is nothing but the product type (the type of tuples) with projections $\pi_X$ and $\pi_Y$ playing the role of ...... well projections and the pairing $\langle,\rangle$ generalizing the pairing constructor for ordered pairs
3. the object $Z^Y$ is the type of functions from $Y$ to $Z$, the morphism $\epsilon \colon Z^Y \times Y \to Z$ is the evaluation, and the mapping $$\mathbf C[X,Z^Y] \to \mathbf C[X \times Y,Z]$$ is the uncurrying.

This parallelism makes arise a notion of interpretation of simply typed $\lambda$-calculus in cartesian closed categories: where an interpretation is nothing but a way to associate objects of a CCC to types and morphisms to $\lambda$-terms (functions).

Giving the details of this construction would be very long so I would rather avoid to give it here, by the way I think you can find different references on the subject: try googling categorical semantics of simply typed lambda-calculus.

I hope this helps.