Interpreting Lambda Calculus using Closed Cartesian Categories

Today I’m going to show you the basic idea behind the equivalency of closed cartesian categories and typed lambda calculus. I’ll do that by showing you how the λ-theory of any simply typed lambda calculus can be mapped onto a CCC.

First, let’s define the term “lambda theory”. In the simply typed lambda calculus, we always have a set of base types – the types of simple atomic values that can appear in lambda expressions. A lambda theory is a simply typed lambda calculus, plus a set of additional rules that define equivalences over the base types.

So, for example, if one of the base types of a lambda calculus was the natural numbers, the lambda theory would need to include rules to define equality over the natural numbers:

x = y if x=0 and y=0; and
x = y if x=s(x’) and y=s(y’) and x’ = y’

So. Suppose we have a lambda-theory $L$ . We can construct a corresponding category $C(L)$ . The objects in $C(L)$ are the types in $L$ . The arrows in $C(L)$ correspond to families of expressions in $L$ ; an arrow
$f : A \rightarrow B$ corresponds to the set of expressions of type $B$ that contain a single free variable of type $A$ .

The semantics of the lambda-theory can be defined by a functor; in particular, a cartesian closed functor $F$ that maps from $C(L)$ to the closed cartesian category of Sets. (It’s worth noting that this is completely equivalent to the normal Kripke semantics for lambda calculus; but when you get into more complex lambda calculi, like Hindley-Milner variants, this categorical formulation is much simpler.)

We describe how we build the category for the lambda theory in terms of a CCC using something called an interpretation function. It’s really just a notation that allows us to describe the translation recursively. The interpretation function is written using brackets: $[A]$ is the categorical interpretation of the type $A$ from lambda calculus.

So, first, we define an object for each type in $L$ . We need to include a special
type, which we call unit. The idea behind unit is that we need to be able to talk about “functions” that either don’t take any real paramaters, or functions that don’t return anything. Unit is a type which contains exactly one atomic value. Since there’s only one possible value for unit, and unit doesn’t have any extractable sub-values, conceptually, it doesn’t ever need to be passed around. So it’s a “value” that never needs to get passed – perfect for a content-free placeholder.

Anyway, here we go with the base rules:

$\forall A \in \mbox{basetypes}(L), [A] = A_C \in C(L)$
$[\mbox{unit}] = 1_C$

Next, we need to define the typing rules for complex types:

$[ A \times B] == [A] \times [B]$
$[A \rightarrow B] = [B]^{[A]}$

Now for the really interesting part. We need to look at type derivations – that is, the type inference rules of the lambda calculus – to show how to do the correspondences between more complicated expressions. Just like we did in lambda calculus, the type derivations are done with a context $Gamma$ , containing a set of type judgements. Each type judgement assigns a type to a lambda term. There are two translation rules for contexts:

$[ \emptyset ] = 1_C$
$[\Gamma, x: A] = [\Gamma] \times [A]$

We also need to describe what to do with the values of the primitive types:

For each value $v : A$ , there is an arrow $v : 1 \rightarrow A_C$ .

And now the rest of the rules. Each of these is of the form $[\Gamma :- x : A] = \mbox{arrow}$ , where we’re saying that $\Gamma$ entails the type judgement $x : A$ . What it means is the object corresponding to the type information covering a type inference for an expression corresponds to the arrow in $C(L)$ .

Unit evaluation: $[ \Gamma :- \mbox{unit}: \mbox{Unit}] = !: [\Gamma] \rightarrow [\mbox{Unit}]$ . (A unit expression is a special arrow “!” to the unit object.)
Simple Typed Expressions: $[\Gamma :- a: A_C] = a \circ ! : [\Gamma] \rightarrow [A_C]$ . (A simple value expression is an arrow composing with ! to form an arrow from Γ to the type object of Cs type.)
Free Variables: $[\Gamma x: A :- x : A] = \pi_2 : ([\Gamma] \times [A]) \rightarrow [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.)
Inferred typed expressions: $[\Gamma, x:A :- x$ , where $\pi_1: ([\Gamma] \times [A])\rightarrow [A']$ (If the type rules of Γ plus the judgement $x : A$ gives us $x$ , then the term $x$ is an arrow starting from the product of the interpretation of the full type context with $A$ ), and ending at $A'$ . This is almost the same as the previous rule: it says that this will evaluate to an arrow for an expression that results in type $A$ .)
Function Abstraction: $[\Gamma :- \lambda x:A . M : A \rightarrow B] = \mbox{curry}([\Gamma, x:A :- M:B]) : [\Gamma] \rightarrow B^{[A]}$ . (A function maps to an arrow from the type context to an exponential $[B]^{[A]}$ , which is a function from $A$ to $B$ .)
Function application: $[\Gamma :- (M M'): B] = \mbox{eval}_{C, B} \circ ([\Gamma :- M: C \rightarrow B]$ , $[\Gamma :- (M M'): B] = \mbox{eval}_{C,B} \circ ([\Gamma :- M : C \rightarrow B]$ , $[\Gamma :- M': C]): [\Gamma] \rightarrow [B]$ . (function evaluation takes the eval arrow from the categorical exponent, and uses it to evaluate out the function.)

There are also two projection rules for the decomposing categorical products, but they’re basically more of the same, and this is already dense enough.

The intuition behind this is:

arrows between types are families of values. A particular value is a particular arrow from unit to a type object.
the categorical exponent in a CC is exactly the same thing as a function type in λ-calculus; and an arrow to an exponent is the same thing as a function value. Evaluating the function is using the categorical exponent’s eval arrow to “decompose” the exponent, and produce an arrow to the function’s result type; that arrow is the value that the function evaluates to.
And the semantics – called functorial semantics – maps from the objects in this category, $C(L)$ to the category of Sets; function values to function arrows; type objects to sets; values to value objects and arrows. (For example, the natural number type would be an object in $C(L)$ , and the set of natural numbers in the sets category would be the target of the functor.)

Aside from the fact that this is actually a very clean way of defining the semantics of a not-so-simply typed lambda calculus, it’s also very useful in practice. There is a way of executing lambda calculus expressions as programs that is based on this, called the Categorical Abstract Machine. The best performing lambda-calculus based programming language (and my personal all-time-favorite programming language), Objective-CAML had its first implementation based on the CAM. (CAML stands for categorical abstract machine language.).

From this, you can see how the CCCs and λ-calculus are related. It turns out that that relation is not just cool, but downright useful. Concepts from category theory – like monads, pullbacks, and functors are really useful things in programming languages! In some later posts, I’ll talk a bit about that. My current favorite programming language, Scala, is one of the languages where there’s a very active stream of work in applying categorical ideas to real-world programming problems.

3 thoughts on “Interpreting Lambda Calculus using Closed Cartesian Categories”

Joe July 5, 2012 at 10:32 am

A lot of the equations disappeared. On all posts in the lambda series and possible others too.

Can you fix it? Thanks 🙂

Loading...

Reply ↓
1. MarkCC Post authorJuly 5, 2012 at 2:13 pm
  
  I’m trying to figure out what’s wrong.. Local tests, it works fine. Some browsers, it’s fine. Other, blooie. As soon as I figure out what’s wrong, I’ll fix in. Anything you can tell me about your browser, might help.
  
  Loading...
  
  Reply ↓
  1. Joe July 6, 2012 at 6:22 am
    
    It works again! Thank you.
    
    I have been using Chrome 20.
    
    Loading...
    
    Reply ↓