An Elementary Introduction to Curry Howard de Bruijn Correspondence

Logic

As a part of honing my logical skills, I was working through the introductory book How Logic Works by Harold Halvorson when I noticed the equivalence between the following formulae:

This in logical terms means that we have two equivalent propositions. On the left hand side, we have a proposition P implying another implication (Q -> R) and on the right we have a conjunction of two propositions P and Q implying R.

Type

I recalled from my earlier exposure to Curry Howard de Bruijn correspondence, and the talk and its accompanying blog series called “The Algebra of Algebraic Data Types” by Chris Taylor that X imply Y can be considered in type theory as the exponential type and X and Y as the product type.

What the post outlines is that these types denote the count of their inhabitants. Whenever you have P -> Q, it means that it is an exponential type and whenever you have P * Q, it means that it is a product type.

This in terms of concrete objects can be thought of as counting the number of possible functions in the case of exponential type and co-occurences of objects in the product type. What does this mean? It can be clarified, if we translate this to its arithmetic counterpart. If we denote exponential type with the raising operation and multiplication for the product type, we can see these closely mirroring the following arithmetic identity about raising numbers to powers:

That might be easy to understand in the case of numbers, but how does that relate to the case of computation? Consider the case of two types X and Y with 3 and 2 elements each, with the mapping X -> Y this can be something like 3 cars of 2 colors, 3 plants of 2 species, or even 3 stories of 2 dreams.

This scenario can be seen from two different perspectives. From the outer/external view, we can think of exponentials just like how exponentiation of numbers work. 3 -> 2 mirrors as 2³. That is, externally, the types can be thought of as tracking number of inhabitants as an exponentiation. But if we take the inner/internal view, we witness something really interesting happening!

What happens internally with exponentiation of types is that this mapping operation tracks potential functions between these two domains! We are counting out the number of functions, that is the number of many-to-one names that can be given for the things we have on the left side (domain) when mapped to a thing on the right (codomain). This is what exponentials in the form of X -> Y denote.

Computation

Types act as the outer view of internal computational content. Exponential types are how we describe functions, and product types capture the Cartesian product of all possible elements in the conjunct types. Using this line of thinking, what is captured by the logic expressed in types can be thought of as two different forms of descriptions of a computer program.

This is the types as propositions interpretation. Types compose to form propositional statements. In order to prove these propositions, we need to bring in evaluation rules that are harmonious with the properties of our proof system. If we turn our view around and look at this from the angle of computation, the process of proving these propositions parallels how we write computer programs that respect the types! In this manner, roughly, one can think of types as the form and computation as its content.

In terms of computation, the exponential type denote a way of organizing programs called currying. In this mode of expression, we pass in parameters one by one to the function. That is, we pass in a value of type P first, which unlocks a new function where you have to pass in a value of type Q to unlock R. Whereas the product type P * Q means a conjunction of parameters, that is both P and Q together as (P, Q) is now being passed as the parameter instead of passing in a chain of types/propositions of P first and then a Q to yield an R.

There is this very nice talk by Sergei on how logic of types can be leveraged to extract their computational content. It was very helpful in clarifying my understanding of how types map to computation for me!

Data

All these pieces clicked together and spurred me to write this post as I had been investigating some discrete calculus and combinatorics on the side. These efforts illuminated how the underlying structures can be seen as different ways in which the partitions / combinations described by the types track their inhabitant computational processes.

I will illustrate what happens combinatorially by taking an example where P has 2 elements, Q has 1, and R has 3 elements. This will give us a concrete context to interpret what is happening with the structures. This part is treated as algebraic formulae in many textbooks. But, I think there is so much juicy visual ideas inherent in the combinatorics. I personally feel the algebraic (intensional) textual treatment needs to be complemented by their visual geometric (extensional) counterparts to enrich and illuminate the underlying ideas.

I am increasingly getting convinced that whenever algebra is used to demarcate a form and study its content, however abstract or complex the underlying subject, a geometry can be associated with the algebraic formulae to give it a visual shape and communicable structure. The ways in which we visualize them provide a concrete setting to see how things connect to / distinguish from each other. This makes way for perceiving the form/content of mathematical objects both in our mind’s eye through algebra and their possible geometric instantiations with our bodily eyes. This marriage of algebra and geometry allows us to both perceive and communicate mathematics symbolically as well as tangibly with our peers.

This is how the mappings from the outside looks like. We will now evaluate the relationships inherent here and count the number of possible functions that hold between these. Using the intuition given in the types section, we can unfold out and see the number of possible combinations these can potentially spawn.

There are many ways to unfold the above relations. Each way we choose out of the possibilities yield a particular form of expansion. I have chosen one where I was able to maintain them as binary trees while revealing the exponentiation process as leading to a staged expansion where each level is progressively indexed by an inhabitant of the exponent.

The pattern of unfolding here can be seen as 8 nodes generated out of the multiplication of {a, b} three times, but each of these levels are indexed by one of the inhabitant of (P * Q) corresponding to a particular level. This may be easier to parse if we think of this in terms of arithmetic. P and Q have 3 and 1 element each, so this gives 3×1 = 3 nodes. This is then used as the exponent of R which has 2 elements, giving us 2(3×1) = 8 nodes.

One thing we can readily notice is that at each level of the unfolding, we obtain a branching tree. If we just look at the {a, b} pair which designate 2, we can see that, it is bifurcating at each level yielding the formal series 21, 22, 23. Thus, {a, b} being the inhabitants of R is being indexed at each level by an inhabitant of its exponent P * Q which has 3 elements, one for each stage of the unfolding. If we look at each level, we can see that it is a representation of (a, b) * (a, b) * (a, b) which is indexed at each level consuming one of the element from our (P * Q) pair with 3 elements.

When we expand out fully the algebraic relation among the inhabitants of the type, we get the following normalized results. We can think of these as the entities we obtain when we unfold the tree fully till it bottoms out.

Now let us look at the case of P -> (Q -> R). Here the unfolding pattern looks almost the same as the case of (P * Q) -> R. But on a closer scrutiny, we find that the labels that index and leaves unfolding at each level are different. What is now unfolding are the inhabitants of (Q -> R) where each level is indexed by the inhabitants of P at each level instead of inhabitants of R exponentiatied by P * Q in the previous case.

The study done here might give the impression that the unfolding patterns for both formulations are going to be the same no matter their inhabitants. But this happened here only because Q has a single inhabitant. In a later section, we will see an example where this uncurried / exponent of product version leads to a deeper tree than the shallower version given by the curried / chained exponentials version.

Here are the results of unfolding the tree out completely and obtaining their nodes. Notice how the inhabitants also share the same P -> (Q -> R) chained exponential pattern in the individual components they are made up of.

Now let us put the unfolding forms of the expressions and their normalized results together. On the left, we have the curried version with two chained exponentials and on the right, the uncurried version which chains product types with an exponential. Notice that we are reifying possible computations tracked by types that are processes, as data structures to do this counting.

The key idea which I want to highlight here is that while both of the expressions have a distinct unfolding pattern as a structure, on normalizing them, that is evaluating them to terms which can’t be simplified further, we end up with results which are identical.

There is a small wrinkle here that we have a difference in operators here, but at the level of normalized elements, we have the identity that 11 being the same as 1 × 1. That is exponentiating something by 1 is identical to multiplying it 1 time. This can be leveraged to turn them from one form to another. I will talk about these algebraic transforms in a later section. At this point the broad strokes details are only what I intend to be communicated.

The global structures we use to organize these two are very different while their local inhabitants turn out to be semantically identical once we unfold them out fully. This isomorphism between the end results is tracked by the logical equivalence between the types. The equivalence established in the logical realm translates as equality of cardinality of the inhabitant data structures. It enables us to see that the way in which we organize programs logically influence not just the way we think about them but also the way in which a machine executes it over space and time. This is a very elementary example and the underlying theory is really much more rich and deep and has more twists, turns, braids, and knots to it.

If this is your first time getting exposed to the ideas, don’t worry. Only a basic gist of the two ways of organizing programs at the type level resulting in two different unfolding patterns is the only thing you need to grasp at this point in the essay. Notice the curious fact that even when the unfolding patterns are structurally the same, their contents: the indices and inhabitants at the leaves of the tree, at each level are very different. I feel this is a significant idea which can shine light on decisions we take towards architecting databases and design algorithms. The broader implications this has for programming in general and dealing with data in systems is something I want to explore in the future. But concentrating our focus on a definite problem, we will flesh out the implications it has for mundane programming tasks using a concrete example in the upcoming sections.

A Brief History of the Correspondence

This connection to computation and logical systems was recognized in a computational context by Nicolaas G. de Bruijn when he designed AUTOMATH with propositions as “categories” of lambda calculus terms and proofs as terms. It is interesting to see him note that he borrowed the idea of exponentials from Heyting’s work. This is a nice paper by him reflecting on his work on AUTOMATH.

But the original identification of this correspondence, though there were no computer programs around at the time, was done by Haskell Curry when he was studying logical systems using his combinatory calculus. It was recorded in his paper called “Functionality in Combinatory Logic” from 1934. But this effort went un(der)developed for about 30 years and till William Howard took notice of this and extended it!

William Howard influenced by Haskell Curry’s work would independently state this correspondence later in his 1969 manuscript. This paper was widely circulated and published in 1980. By this time, this idea got osmosized into the research culture. It has been researched and developed ever since then!

That was a very quick and brief runthrough of the four way correspondence which I think shines light on why this is such an interesting idea! But it must have been too fast paced unless you knew these ideas beforehand. Let us unpack these at a slower pace considering each side of the original equation one at a time.

❖ ❖ ❖