[Math] Relation between Cartesian closed category and Lambda Calculus

cartesian-closed-categoriescategory-theorylambda-calculus

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?

Best Answer

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.

Related Question