OCaml’s Categorical Origins

OCaml is an interesting language, to say the least. It’s a strongly-typed strictly-evaluated functional language with some object-oriented features. I had read Real World OCaml¹ but haven’t really used the language in practice, so my knowledge is a bit shaky. I did know, however, that the “O” in “OCaml” had something to do with objects. What I didn’t know was the origin of the “Caml” bit.

Before OCaml there was Caml, created in the mid 80s. “Caml” is an acronym for “Categorical Abstract Machine Language”. This parses as [categorical abstract machine] [language], rather than [categorical abstract] [machine language].

Abstract machines are useful models of computers, but they’re allowed to have non-realistic characteristics. For example, Turing machines, one of the most commonly used kind of abstract machine, are assumed to have infinite memory. The categorical abstract machine (CAM) is a special kind of these abstract machines, roughly separated by its basis on the confluence of category theory and lambda calculus.

Let’s try to break down the following paragraph to better understand how CAMs help us bridge the gap from mathematical constructions to code we can run on a real computer. The definitions I give won’t be rigorous, but should give a better understanding of how this all works. For rigorous definitions, please see the footnotes.

One of the most widely cited connections between category theory and computer science is the correspondence between Cartesian closed categories and typed λ-calculi.²

Category theory is the study of mathematical objects called (unsurprisingly) “categories”. A category has the following:

• A collection of mathematical objects
• A collection of morphisms (also called “arrows”) between those objects
• Identity morphisms for each object in the category (identity roughly meaning we get back what we put in)
• Morphism composition (for each pair of morphisms X and Y, there is another morphism that represents first applying morphism X, then Y, kind of like a shortcut arrow)
• A way to get the domain and codomain from each morphism

Even more roughly, you can think of a category as a collection of objects with arrows between them, where each object has an arrow to itself (identity) and each pair of arrows suggests a third arrow (composition).

Because of the status of categories as a bunch of objects with a bunch of arrows between them, it’s easy and useful to draw pictures (“diagram schemes”) for them. There’s even some special language (“the diagram commutes”) that ostensibly relates more directly to the diagrams than the underlying category!³

If we say that categories have composition and identity, then “Cartesian categories” are categories with some additional features, loosely:

• A way to create a pair (or tuple) of objects (,)
• A way to get the first element of a pair. This can be called fst in OCaml, or in math, \(\pi_1\). We can also say we perform the projection \(\pi_1 : (A, B) \to A\)
• A corresponding way to get the second element of a pair, called snd or \(\pi_2 : (A, B) \to B\)

Finally, “Cartesian closed categories” also give us:

• Currying, which you can think of as a way to transform a function \(f : (A, B) \to C\) into a function \(f' : A \to (B \to C)\). That is, it lets us apply the first argument separately to get back a new function with that argument “pre-applied”.
• Application, which gives us a programmatic notion of functions very similar to the meat of the lambda calculus

“typed λ-calculi” refers to a lambda calculus, a sort of abstract programming language where we do our computations as reductions of terms and as applications of terms to other terms. “Typed” means much what it usually does in programming: each value (or “term”) has some type associated with it. For example, if the type of 5 is “integer”, we can say \(5 : \mathbb{Z}\), or in OCaml, 5 : int.

The specific typed λ-calculus in question has many of the same constructions as we just talked about with Cartesian closed categories. It has product types, or pairs of A and B written \(A \times B\). It has function types, analogous to morphisms in our categories. There is indeed a correspondence here, which I haven’t proven in detail, but maybe you can begin to see the outlines.

In short, we’ve just given a birds-eye overview of the connections between Cartesian closed categories and a specific kind of lambda calculus. How does this help us build our CAM?

Because of the correspondence, we can think about CAMs as both category theoretical constructions, or as operating with pieces of lambda calculus. We need some minimal structure to begin with, and the structure used for a CAM looks like “a term (rather a graph in an actual implementation), which is a structured value, a code, and a stack (or dump).”⁴

Eliding a whole lot of possible optimizations, and background information about previous kinds of abstract machines well-suited to functional programming, a CAM uses these basic structures to perform “categorical combinatory logic”. Even more simply, it uses rewrite rules to evaluate terms in the context of a stack. It does things like pushing a term to the stack, replacing the current term with the term on top of the stack, and popping the stack. Reduction of terms follows rules much like those in our λ-calculus, where we perform applications when we can. The most important feature at such a low level is to avoid name clashes, which there are rules for as well.

This kind of low-level CAM code, once optimized, can then be transformed into typical machine code and run on a real computer with a real stack, and real registers to hold the terms. Even coming from a very different viewpoint, theoretically, it’s still possible and desirable to run your code on a real machine! CAMs act as the intermediary between categories/λ-calculi and a real machine, and are thus a valuable model in kind of the same way Turing machines are valuable even if we can’t ever build one directly.

This is all just to say that “OCaml” is one of the most jam-packed acronyms I’ve ever come across, and we haven’t even touched the “Objective” part yet! Like its fellow languages in the ML family, you can interpret it on a low-ish level via lambda calculus, or you can just use it as a programming language and never worry about what’s going on under the hood at all (but that’s no fun)! Even though CAMs are used in real applications (namely, the creation of Caml) it can’t hurt to try on a new way of thinking, and because CAMs provide a different model of thinking about how computers operate, they’re valuable in and of themselves.