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?

  • $\begingroup$ I think that question 2) is ill posed: lambda calculus cannot express the structure of a cartesian closed category. On the other hand you can interpret lambda calculus in a cartesian closed category. $\endgroup$ Apr 18 '16 at 10:29
  • $\begingroup$ Of course my previous comment applies if by lambda-calculus you mean the untyped lambda-calculus. Did you meant symply typed lambda-calculus instead? $\endgroup$ Apr 18 '16 at 11:05

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.


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 :-)

  • 1
    $\begingroup$ Thank you @Musa Al-hassy, that did reduce some of the confusion $\endgroup$ Feb 25 '16 at 8:11

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.