This is one of the last posts in my series on category theory; and it's a two parter. What I'm going to do in these two posts is show the correspondence between lambda calculus and the [cartesian closed categories][ccc]. If you're not familiar with lambda calculus, you can take a look at my series of articles on it [here][lambda]. You might also want to follow the CCC link above, to remind yourself about the CCCs. (The short refresher is: a CCC is a category that has an exponent and a product, and is closed over both. The product is an abstract version of cartesian set product; the exponent is an abstraction of the idea of a function, with an "eval" arrow that does function evaluation.)
Today I'm going to show you one half of the correspondence: how the lambda-theory of any simply typed lambda calculus can be mapped onto a CCC. Tomorrow, I'll show the other direction: how an arbitrary CCC can be mapped onto a lambda-theory.
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:
1. x = y if x=0 and y=0; and
2. 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 → 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**, including "unit", which is a special distinguished value used for an expression that doesn't return anything:
* ∀ A ∈ basetypes(**L**), [A] = AC ∈ C(**L**)
* [unit] = 1C
Next, we need to define the typing rules for complex types:
* [ A × B ] = [A] × [B]
* [ A → 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. Type derivations are done with a *context* containing a set of *type judgements*. Each type judgement assigns a type to a lambda term. We write type contexts as capital greek letters like Γ. There are two translation rules for contexts:
* [∅] = 1C
* [Γ, x : A] = [Γ] × [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 → AC.
And now the rest of the rules. Each of these is of the form [Γ :- x : A] = arrow, where we're saying that Γ 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 : Unit] = ! : [Γ] → [Unit] *(A unit expression is a special arrow "!" to the Unit object)*
* [Γ :- a : AC] = a º ! : [Γ] → [AC] *(A simple value expression is an arrow composing with ! to form an arrow from Γ to the type object of Cs type.)*
* [Γ x : A :- x : A] = π2 : ([Γ ] × [A]) → [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.)*
* [Γ, x:A :- x' : A'],x' ≠ x = [Γ :- x' : A'] º π1 where π1 : ([Γ] × [A]) → [A']. *(If the type rules of Γ plus the judgement x : A gives us x' : A', then the term x' : A' 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.)*
* [Γ :- λ x:A . M : A → B] = curry([Γ, x:A :- M:B]) : [Γ] → [B][A] *(A function typing rule: the function maps to an arrow from the type context to an exponential [B][A], which is a function from A to B.)*
* [Γ :- (M M') : B] = evalC,B º ([Γ :- M : C → B], [Γ :- M' : C]) : [Γ] → [B] *(A function evaluation rule; it 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 *is* the same as a function type; a function *value* is an arrow to the type. 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 like the NNO we showed yesterday in C(**L**), and the set of natural numbers is 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][cam]. The best performing lambda-calculus based programming language (and my personal all-time-favorite programming language), [Objective-CAML][caml] is based on the CAM. (CAML stands for categorical abstract machine language.)
This is great stuff you're posting on the lambda calculus and cartesian closed categories. Oh, if only I'd read it sooner, when it would have saved me years of confusion! Now it'll just save me months of confusion.
I came to the lambda calculus via cartesian closed categories and a general interest in categories and physics - not via computer science. So, it's taken me quite a while to figure out what computer scientists do with it, and in fact I'm still a bit puzzled about how much impact it has on the much-overrated "real world". Okay, so there are beautiful computer languages like Haskell, Scheme and (I'd never heard of it before!) Objective-CAML, based on the lambda calculus. But, what impact does the lambda calculus have on the average joe programmer? A subtle and indirect one, I presume. Is there some sort of complicated trickle-down effect going on, just like quantum physics is ultimately required to build lasers, but a check-out clerk can use a scanner without even knowing what that little red light is?
I'm writing a grant proposal trying to get some dough for a grad student of mine to have more free time to work with me on the "quantum lambda calculus", a generalization hopefully relevant to (so far mainly imaginary) quantum computers. The quantum lambda calculus is based on certain noncartesian closed categories, of which the category of Hilbert spaces is a key example. I'm more interested in the math and physics of this stuff than the practical applications, actually. But, I bumped into the "Wizard Book" used for teaching the introductory computer science at MIT. I noticed it has a big fat lambda on the cover, and noticed the credits to Haskell and Curry, and noticed they give homework in Scheme. I also noticed that over 100 schools use this book. So, the lambda calculus must be having some impact on the "real world".
Lambda calc actually does have a direct effect on many programmers, in several ways.
* Language constructs that are becoming increasingly common are lambda-based. For example, the generic type mechanism in Java is based on the generic type systems that originated in the lambda based languages; and Java uses Hindley-Milner lambda calculus type inference (that is, type inference based on CCCs) for type checking.
* Compilers use a lot of lambda-based techniques. Especially some of the ones for more recent languages. For example, some Java JITs use a linear lambda calculus based approach to determining when objects *don't* need to be dynamically allocated.
* The static analysis in many compilers is quite strongly based on lambda calculus - especially the ones built in Europe. There's a technique called abstract interpretation which is lambda calculus (or at least CCC) based.
* Every language which has a precise formal semantics expressed that semantics in lambda calculus form. Every language that I know of with a sound type system bases that type system on lambda calc, predicate logic, and CCCs.
I'm the grad student he's talking about. I've got a question about lambda theories. We can describe a structure like groups with a lambda theory L:
o a type G
o terms for multiplication, unit, and inverse, along with the ones we automatically have like duplication and deletion
o axioms that impose relations on the terms, like the right-inverse axiom:
mult(pi_1,inv(pi_2))(dup) = unit(del)
Objects in the category C(L) corresponding to this lambda theory are types generated from G under products and exponents; arrows are generated from the terms under products and composition. Diagrams are generated similarly from the axioms. A functor from this category into Set has as its image a group.
I don't see where S and K come into play here; there are no explicit descriptions of the terms mult or unit or inv, just axioms they have to satisfy. Also, I don't see how you get a family of expressions in the theory from an arrow in C(L); for example, I'd expect to get a single arrow m from GxG->G, another arrow pi_1 from GxG->G, as well as the product arrow pi_1 x m:GxGxGxG->GxG.
The best performing lambda-calculus based programming language (and my personal all-time-favorite programming language), Objective-CAML is based on the CAM. (CAML stands for categorical abstract machine language.)
I don't believe OCaml has been using CAM for at least a decade and a half. I think it was initially replaced by ZAM and later even more efficient andeffective abstract machine models. Xavier Leroy has an overview:
From Krivine's machine to the Caml implementations: http://pauillac.inria.fr/~xleroy/talks/zam-kazam05.pdf
Every language which has a precise formal semantics expressed that semantics in lambda calculus form.
Denotational semantics isn't the only game in town. Its compositionality is certainly very valuable but there is nothing inherently imprecise or informal about an operational semantics. Or axiomatic semantics for that matter.