Monthly Archives: March 2012


What’s a subset? That’s easy: if we have two sets A and B, A is a subset of B if every member of A is also a member of B.

We can take the same basic idea, and apply it to something which a tad more structure, to get subgroups. What’s a subgroup? If we have two groups A and B, and the values in group A are a subset of the values in group B, then A is a subgroup of B.

The point of category theory is to take concepts like “subset” and generalize them so that we can apply the same idea in many different domains. In category theory, we don’t ask “what’s a subset?”. We ask, for any structured THING, what does it mean to be a sub-THING? We’re being very general here, and that’s always a bit tricky. We’ll start by building a basic construction, and look at it in terms of sets and subsets, where we already understand the specific concept.

In terms of sets, the most generic way of defining subsets is using functions. Suppose we have a set, A. How can we define all of the subsets of A, in terms of functions? We can do it using injective functions, as follows. (As a reminder, a function from X to Y where every value in X is mapped to a distinct function in y.)

For the set, A, we can take the set of all injective functions to A. We’ll call that set of functions Inj(A).

Given Inj(A), we can define equivalence classes over Inj(A), so that f: X \rightarrow A and g: Y \rightarrow A are equivalent if there is an isomorphism between X and Y.

The domain of each function in one of the equivalence classes in Inj(A) is a function isomorphic to a subset of A. So each equivalence class of injective functions defines a subset of A.

And there we go: we’ve got a very abstract definition of subsets.

Now we can take that, and generalize that function-based definition to categories, so that it can define a sub-object of any kind of object that can be represented in a category.

Before we jump in, let me review one important definition from before; the monomorphism, or monic arrow.

A monic arrow is an arrow f : a \rightarrow b such that
\forall g_1, g_2: x \rightarrow a: f \circ g_1 \ge f \circ g_2 \Rightarrow g_1 = g_2 (That is, if any two arrows composed with f in f \circ g end up at the same object only if they are the same.)

So, basically, the monic arrow is the category theoretic version of an injective function. We’ve taken the idea of what an injective function means, in terms of how functions compose, and when we generalized it, the result is the monic arrow.

Suppose we have a category C, and an object a in \mbox{Obj}(C). If there are are two monic arrows f : x \rightarrow a and g : y \rightarrow a, and
there is an arrow h such that g \circ h = f, then we say f \le g (read “f factors through g”). Now, we can take that “≤” relation, and use it to define an equivalence class of morphisms using f \equiv g \Leftrightarrow f \le g \land g \le f.

What we wind up with using that equivalence relation is a set of equivalence classes of monomorphisms pointing at A. Each of those equivalence classes of morphisms defines a subobject of A. (Within the equivalence classes are objects which have isomorphisms, so the sources of those arrows are equivalent with respect to this relation.) A subobject of A is the sources of an arrow in one of those equivalence classes.

It’s exactly the same thing as the function-based definition of sets. We’ve created a very general concept of sub-THING, which works exactly the same way as sub-sets, but can be applied to any category-theoretic structure.

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:

  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 \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: , where (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 . 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: , , . (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.

Obama Campaign Lies with Bad Math

This post is a bit of a change of pace for me.

As you all know, when it comes to politics, I’m a hardcore lefty liberal type. And lots of annoying people like to claim that the reason I write more critical posts about right-wing politicians than left-wing ones is because I’m hopelessly biased. I definitely do end up writing more posts critical of RW than LW politicians, but I believe that that’s because in modern day america, the right wing has completely lost touch with reality. They’re just far more likely to regurgitate long-disproven lies, or to use specious, unsupportable, or just plain pig-ignorant reasoning.

But a reader sent me a copy of a recent fund-raising letter from the Obama campaign, and it’s pissed me right off. I probably actually received a copy of it myself, but I’ve got my spam filters set to throw away anything from the Obama campaign, so I didn’t see it until it was pointed out to me.

When it comes to bad math, in my opinion, there are two main kinds. There’s ignorant bad math, and there’s dishonest bad math. In the former, the people pushing it don’t understand what they’re talking about. They’re saying something that they actually believe. It’s hopelessly wrong, and if they made any effort to learn something about what they’re babbling about, they’d see how wrong they are. In the latter kind, the people pushing it are deliberately trying to deceive their readers/listeners. They know that they’re doing something wrong, and they’re hoping that you are stupid enough to not catch on.

The latter kind of bad math is far worse than the former.

And this Obama campaign fundraising letter is very firmly in the latter camp.

I’m not going to post the entire thing, and I’m not going to provide a link. That would be giving them publicity for this despicable, dishonest effort, which is exactly what they want, and I will not reward them for this.

The letter starts by complaining about a Romney campaign fundraiser, saying:

It may not take the Romney camp very long to get to a million — they announced today that just 9 percent of their money comes from donors giving less than $200.

Take note of the fundamental point there. Of the money collected, 9% came from small donors.

Then they attempt to contrast themselves against Romney:

Our campaign is different. It’s about bringing people together to protect the progress we’ve made and make a lot more in a second term. And 98 percent of the donations people like you make to this campaign are $250 or less.

The main point: of the people donating, 98% were small donors.

You’re supposed to look at that, and say “90% of the donors to Romney are big-money people, but just 2% of the donors to Obama are.”

But they’re not comparing the same thing. One is a percentage of money, and the other is a percentage of people. Let’s take a quick look at an example, to show how this works.

Suppose we’ve got just ten donors. They gave 200, 200, 200, 100, 100, 100, 50, 50, 50, and 1,000,000 dollars, respectively. Obviously, 90% (9 out of 10) donors gave $200 or less. And if you work it out, more than 99% of the money came from donations of $1,000,000 or more.

What does the Obama campaigns actual donor distribution look like? I don’t know. But I’d guess that it’s actually pretty similar to the Romney campaign. Politics in America is, very much, a rich persons sport. Both campaigns are absolutely relying on huge donations from people with lots and lots of money. The Obama campaign wants to trick us into believing that they’re different. But all they’re doing is proving that they’re not. They’re lying to us, and hoping that we’re too stupid to notice.

(There’s another level of dishonesty there, but it’s far more trivial. In the Romney campaign figure, they talk about the percentage of donotions smaller than $200; for the Obama campaign figure, they use $250. Why? Probably because they wanted a number for the Romney campaign where they could say that more than 90% came from big donors. And hell, once they were lying, what’s another lie?)