Relation between Cartesian closed category and Lambda Calculus
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:
- 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)
- 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$
- 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:
- 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;
- 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
- 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.
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 :-)