2
$\begingroup$

In several papers on type theory it's possible to see some sort of numerical notation for types based on the number of possible constructors for the type. For example, the unit type is usually written as $1$, as there's only one possible constructor for it; similarly, they use $2$ for booleans, $x + y$ for disjoint unions (sum types), $x * y$ for product types, and so on.

This kind of notation seems to be assumed familiar to the reader. Where does it come from? Are there any sources that explicitly explain this notation?

$\endgroup$
  • 1
    $\begingroup$ I could say it's from category theory but I could be wrong if this is a question about history. It could be more on topic to ask what is the common thing between [product type/multiplication of number/cartesian product of set/logical and/infimum] so that they sometimes share a common notation. $\endgroup$ – Apiwat Chantawibul Jan 3 '18 at 12:32
  • $\begingroup$ Actually I just would like to have a reference to explain why this notation exists, not really about its history. It seems to me that it "counts" how many ways there are to construct the element, it even has fixed points ($\mu$ and $\nu$), but this notation always seem to be "obvious" to the reader. $\endgroup$ – paulotorrens Jan 3 '18 at 12:36
5
$\begingroup$

This almost certainly derives from (finite) set theory. The cardinality of a finite set $S$, written $|S|$, is the number of distinct elements it has. For finite sets, we have the following relations: $$\begin{align} |\emptyset| & = 0 \\ |1| & = 1 \\ |A\times B| & = |A||B| \\ |A\uplus B| & = |A|+|B| \\ |B^A| & = |B|^{|A|} \end{align}$$ where $A\times B$ is the Cartesian product of $A$ and $B$, $A\uplus B$ is the disjoint union of $A$ and $B$, and $B^A$ is the set of functions from $A$ to $B$. The type theoretic constructions $A\times B$ (product types), $A+B$ (sum types), and $A\to B$ (function types) correspond to these set theoretic constructs. For example, finite sets form a model of the simply typed lambda calculus with products and sums where product, sum, and function types are interpreted as exactly the constructs on finite sets above. This correspondence is not general. There are many other models of the simply typed lambda calculus that will interpret these type constructions differently. Nevertheless, this is the archetypal example.

Category theorists often use similar notation but it is motivated the same way.

Another take on this is that these type operations (ignoring function types though their existence implies distributivity) make types into a commutative semiring up to isomorphism. Equations that you can prove in the theory of commutative semirings give rise to type isomorphisms.

$\endgroup$
5
$\begingroup$

Although they obviously come from a much more ancient tradition (we'd need to pick apart sources from Zermelo, Russel and Wittgenstein to get to the bottom of this!), the 1972 article An intuitionistic theory of types by Martin-Löf already contains the notations $+$ and $\times$ for disjoint sum and Cartesian product, respectively, and have been standard ever since.

It's worth a read: https://michaelt.github.io/martin-lof/An-Intuitionisitic-Theory-of-Types-1972.pdf

I'm not sure when the notations $\mathbf{0}$, $\mathbf{1}$ and $\mathbf{2}$ became widespread. I remember seeing them in Connor McBride's articles first, but that's just anecdotal. As Derek points out, the notations are very reasonable.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.