## An introduction to the origins of type theory

“What does a barber have to do with computer science?” You’re probably asking yourself. Whether you’re curious about computer science or already a seasoned computer scientist, this article will not only answer that question, but it will also teach you the origins of an integral part of computer science: types.

To introduce the titular barber, consider the following riddle:

There is one barber in town. This barber shaves everyone who does not shave themselves, and no one else. Does the barber shave himself?

To better understand how we should approach this problem — and why it matters — we’ll first get into the basic philosophy of types.

To understand the world around us, we draw all kinds of identifying lines between different things: whether species of animals, magnitudes of earthquakes, or sizes of cities. There are apparent and distinct types of things that exist in the world around us. A dog is obviously different from a human, which are both different from a tree.

*But how do we make these distinctions concrete and specific enough for a computer to understand them?*

A simple approach is to define sets of things and establish relationships between those sets. You can think of sets as containers or buckets with labels on them — kind of like a category. For example, we could create some basic sets of the animal kingdom like so:

While this may seem simple, this organization of concepts already gives us some handy capabilities. For example, if I know that my friend Bob is a Human, then I also know that Bob must be a mammal. By putting sets inside other sets, I can describe a hierarchical relationship. Similarly, I can describe how dolphins are both sea creatures *and* mammals. By overlapping sets, I can describe concepts that have traits in common with multiple concepts.

However, sets do have some significant limitations. This is where we return to our barber. Recall our original riddle:

There is one barber in town. This barber shaves everyone who does not shave themselves, and no one else. Does the barber shave himself?

Okay, let’s break this down. If we were to ask a random person off the street in this town, “do you shave yourself?” and they reply “no,” then we know the barber must shave them. However, what if we ask the barber this same question?

If the barber says yes — he does shave himself, and since we know the barber doesn’t shave anyone who shaves themselves, the barber does not shave himself.

If the barber says no — he does not shave himself, and since we know the barber shaves all those who shave themselves, the barber does shave himself.

The barber shaves himself and he doesn’t shave himself?

Clearly, something in our setup doesn’t make sense. Aany problem which leads to these kinds of contradictions is what we call a paradox.

This particular paradox, however, isn’t just any random brainteaser — it is one of the most important problems in the history of computer science and mathematics. It was discovered in 1901 by famous British mathematician Bertrand Russel and is called Russel’s Paradox. The barber’s paradox is Russel’s way of expressing this problem he discovered in set theory in a way that could be commonly understood.

Building a system on top of a theory that can allow contradictions like Russel’s paradox will lead to all sorts of problems, so what can we do instead?

The essential problem of sets that leads to this paradox is that sets may be described through other sets, including themselves.

Russel, trying to solve these problems, began to add restrictions to sets, giving them more order. This order came in the form of specific rules about how these new and more complex sets should be allowed to interact with each other. In mathematics and type theory, we call these rules axioms.

Over time, as computer scientists argued and collaborated, these axioms evolved, and simple sets became complex types. Type theory would evolve over the years, and indeed it still does. Modern programming languages today rely on type theory — to make a distinction between a zip code and a first name or to figure out how many decimal points to keep when doing complex calculations.

Some examples of types in modern programming languages are integers: numbers with no decimal places, and strings: text-like sentences or even entire books.

However, what many computer scientists may not know when using strings, integers, or other complex types is that they all come from one very important barber.