Sigma, Pi. Sum, Product.

home writeups

Introduction

On my earliest expeditions into the world of type theory, I remember being very irritated by the apparent inconsistency in the naming of (dependent) sum and product. After exploring a little more, my confusion disappeared, and irritation gave way to appreciation for the (actual) symmetries that those names express. Here, I'll explain this symmetry using some simple examples, and in the process hopefully give a tolerable introduction to dependent types for curious newcomers.

Sum and Product

Let's begin by examining regular sum and product types. Any programmer who has used an ML-style functional language will be familiar with these. To illustrate, consider these (truly exemplary) examples:

Inductive Sum (a b : Type) : Type :=
| left : a -> Sum a b
| right : b -> Sum a b. 

Inductive Product (a b : Type) : Type :=
| both : a -> b -> Product a b.

Fundamentally, the sum expresses alternation (disjoint union, "one or the other"), while the product expresses combination ("give me both!"). This intuitively corresponds with logical disjunction and logical conjunction (and this intuition is a good one). Further, the names "sum" and "product" correspond nicely with the notion of disjunction as "logical sum" and conjunction as "logical product". For now, all is fine and dandy.

Next, we'll consider the dependent sum (sigma) and product (pi) types. These are tragically absent from most mainstream programming languages (by a definition that considers languages like Haskell mainstream), and by such warrant a bit more explanation.

Dependent Product

First, the dependent product, often called the pi type. In papers or other literature, you'll see it written as

\begin{equation*} \Pi x : A.B(x) \end{equation*}

or sometimes instead as

\begin{equation*} \forall x : A.B(x) \end{equation*}

which foreshadows the eventual connection to logic we'll be making.

Let's break down what the above means.

Recall that the type \(A \to B\) denotes functions from a domain \(A\) to a codomain \(B\). The dependent product type extends this basic notion of function to allow the codomain \(B\) of a function \(f(x)\) to change depending on the value of \(x\). Why is this useful? Well, if you've written much Haskell or ML, you've certainly written functions that are dependent, albeit only in a very particular sort of way. For example:

f :: Maybe x
f = Nothing

Perhaps surprisingly, this is a dependent product. Writing the previous example more verbosely (the meaning is unchanged):

{-# LANGUAGE ExplicitForAll #-}

import Data.Kind (Type)

f :: forall (x :: Type). Maybe x
f = Nothing

This looks a whole lot like a dependent product! Here, \(A\) is Type, and \(B\) is Maybe (a unary type constructor). Unfortunately, in Haskell this kind of dependency works only in the special case (polymorphism) where \(A\) is Type (or some type-ish thing, mostly). However, you can probably imagine some cases where it would be useful to be "polymorphic" over something other than a type (maybe a number, or a string, or even something even more complex). This is precisely the functionality of the dependent product.

To move forward from here, it might be helpful to consider a (maybe contrived) example from logic. Let's imagine that we have a type Man and a unary type constructor Mortal. Also, let's imagine that the terms of type Man somehow correspond to men, and that Mortal x where x :: Man somehow encodes the proposition that x is mortal. In a hypothetical dependent Haskell, we might write:

{-# LANGUAGE ExplicitForAll #-}

allMenAreMortal :: forall (x :: Man). Mortal x
allMenAreMortal = _proofGoesHere

Above, we've used the dependent product to encode a universally quantified proposition. We can gain some intuition for why this actually expresses universal quantification by imagining what ought to replace the hole _proofGoesHere. Remember, the dependent product type is a generalized function type. In order to define allMenAreMortal, we must construct a function from x (some arbitrary term of type Man) to a term of type Mortal x (proof of mortality, maybe a death certificate) for that particular x. Further, this function should handle all possible terms of type Man, since partial functions aren't very nice, leading to runtime errors and all sorts of other nastiness. Therefore, to define a term of type forall (x :: Man). Mortal x, we must define a mapping from any possible Man to an example that demonstrates that exact Man's mortality. This is exactly the essence of universal quantification, and reasoning of this kind is the main thrust of the mathematics that gives us a chance to prove properties about programs.

For posterity, let's write the exemplary dependent product in Coq, a real dependently typed language, rather than our fake Haskell with -XDependentTypes:

Definition Pi (a : Type) (b : a -> Type) : Type :=
  forall (x : a), b x.

Nothing too foreign now that we're comfortable with the notation. You can download Coq or another dependently-typed language today, and play with some similar examples, which might even be practically useful in some cases.

In all this discussion about the dependent product, something should have been nagging at the unfamiliar reader's mind: what does any of this have to do with the good old normal product type? Isn't a product supposed to just be a pair, an n-tuple, a Cartesian product? What's the deal? In fact, this confusion is the very reason for this posting. A hint lies in one part of the nomenclature that makes immediate sense: correspondence with universal quantification aligns nicely with the correspondence of the product type with conjunction, because universal quantification is a sort of "extended" conjunction.

Think about it:

\begin{equation*} \forall x. Y(x) \end{equation*}

is equivalent to

\begin{equation*} Y(x_1) \wedge Y(x_2) \wedge \cdots \wedge Y(x_n) \end{equation*}

where \(x_1, x_2, \dots, x_n\) enumerate all possible values for \(x\).

Once we recognize that universal quantification is a sort of generalized conjunction, we can gain insight by flipping the reasoning upside-down in our head, and thinking instead of conjunction as a specific case of universal quantification. Let's think about what a pair of an integer and a rational number looks like in this formulation. First, consider a type \(\mathbb{B}\) that has two constructors, \(\mathrm{true}\) and \(\mathrm{false}\). This trivial two-constructor type seems like the correct type over which to quantify, since we're trying to create a conjunction of exactly two terms:

\begin{equation*} \forall x : \mathbb{B}. B(x) \end{equation*}

Now we must determine the proper definition of \(B : \mathbb{B} \to \mathrm{Type}\), which will determine the respective types of the terms in our conjunction. This is simple enough; \(\mathrm{true}\) should correspond to the type of the first term (the integer type \(\mathbb{Z}\)) and \(\mathrm{false}\) should correspond to the type of the second term (the rational type \(\mathbb{Q}\)).

\begin{equation*} B(x) = \begin{cases} \mathbb{Z} & x = \mathrm{true}\\ \mathbb{Q} & x = \mathrm{false} \end{cases} \end{equation*}

Let's see how we'd write a term of the above type that expresses, say, the pair of \(5\) and \(3.5\). Remember that since the product type is a generalized function type, we'll be constructing a function term, and that the domain of this function is \(\mathbb{B}\) and the codomain is \(B(x)\). Ready?

\begin{equation*} \mathrm{pair}(x) = \begin{cases} 5 & x = \mathrm{true}\\ 3.5 & x = \mathrm{false} \end{cases} \end{equation*}

(Some readers might notice that this definition of \(\mathrm{pair} : \forall x : \mathbb{B}.B(x)\) (and also the definition of \(B\) for that matter) is very similar to the Church encoding of a pair in the untyped lambda calculus. The main difference is that here we retain full static (compile-time) type safety!)

This idea of dependent product as generalized product using an indexing type (here the type with two terms \(\mathbb{B}\)) is the reason behind the name. The product type as an n-tuple only allows us to use a finite type with \(n\) elements as that index, but introducing the dependent product frees us from our shackles and allows us to use any type. This is precisely the context in which Per Martin-Löf introduces the dependent product type in his influential 1972 paper An Intuitionistic Theory of Types, which presents a type system whose lineage extends through Coq, Agda, and Idris.

Dependent Sum

Next up, the sum type, also called the sigma type. You'll see this one written as

\begin{equation*} \Sigma x : A.B(x) \end{equation*}

or maybe as

\begin{equation*} \exists x : A.B(x) \end{equation*}

(Notice a trend?)

This time around, we'll start off with an example in Coq:

Inductive Sigma (a : Type) (b : a -> Type) : Type :=
| witnessed : forall (x : a), b x -> Sigma a b.

What is this saying? Namely, that to build a term of type Sigma a b, we need both a term x of type a and a term of type b x. At first glance, the dependent sum type is a generalized pair (product type), just like the dependent product type is a generalized function type. The difference between the dependent sum type and the product type is that the dependent sum allows the type of the second term to depend upon the first term, which brings with it major expressive power. For example, with the help of the dependent sum, it is trivial to turn homogeneous data structures into heterogeneous data structures! Given a type a, imagine the type of homogeneous lists of a, which we will denote [a] (like in Haskell). We can then define a heterogeneous list as [Sigma Type id] (where id is the identity function for Type). These heterogeneous lists do not sacrifice type safety, as the elements are always associated with their types.

(By this point, you should be thoroughly irritated that dependent sum generalizes product. Read on.)

Moving on, let's change our perspective on the dependent sum, and consider it as an expression of existential quantification (as the notation suggests). Let's return to our previous example: terms of type Man that might be Mortal in pseudo-Haskell. We can attempt to express the claim that there exists at least one Man who is Mortal:

oneMortalMan :: exists (x :: Man). Mortal x
oneMortalMan = _proofGoesHere

Assuming exists is the type constructor for the dependent sum, what must replace _proofGoesHere? Well, the dependent sum is a generalized pair, so in order to define oneMortalMan we must build a pair of x (a Man) and a proof of x's mortality (a Mortal x). This sounds a whole lot like a proof of the existentially quantified statement: we've shown that there is a man (x) and that Mortal x holds for that man. This is fundamental notion of a constructive existence proof, and it makes a lot of sense. To show that a thing exists, we must be to identify it (that is, to provide a witness). Here, if we had a man socrates :: Man and a proof-of-mortality socratesDies :: Mortal socrates, the pair of socrates and socratesDies could replace _proofGoesHere. We've shown that at least one mortal man exists by finding a concrete example of one such man.

At this point, we have a decent sense of the dependent sum as existential quantification. What does this say about the naming? What on earth does this have to do with the regular sum type? It seems like dependent sum is expressing a Cartesian product (having both things), not disjoint union (having one thing or the other).

To make sense of this, let's start with what does make sense: the sum type corresponds with disjunction, while the dependent sum corresponds with existential quantification. Of course, just as universal quantification is arbitrary-arity conjunction, existential quantification is arbitrary-arity disjunction.

Consider that

\begin{equation*} \exists x. Y(x) \end{equation*}

is the same as

\begin{equation*} Y(x_1) \vee Y(x_2) \vee \cdots \vee Y(x_n) \end{equation*}

where \(x_1, x_2, \dots, x_n\) again enumerate all possible values for \(x\).

So, just like in the case of the dependent product, let's flip everything upside-down. Let's think about disjunction as a special case of existential quantification. How, then, would we write the disjoint union of an integer and a rational number? Once again, we'll consider the type with two terms, which here we'll call \(\mathbb{B}\). Since we have two options in our disjoint union, this makes a lot of sense: we only need to store a term of one type (either \(\mathbb{Z}\) or \(\mathbb{Q}\)), so we can use the first element of the pair as an index that determines the type of the second element. This is exactly what the dependent sum does:

\begin{equation*} \exists x : \mathbb{B}. B(x) \end{equation*}

One question remains: the definition of \(B : \mathbb{B} \to \mathrm{Type}\), which given a boolean determines the type of the second element in the pair. It turns out that this is exactly the same function that we used before to write product in terms of dependent product!

\begin{equation*} B(x) = \begin{cases} \mathbb{Z} & x = \mathrm{true}\\ \mathbb{Q} & x = \mathrm{false} \end{cases} \end{equation*}

By considering indexing of this kind, we've successfully made sense of the dependent sum and dependent product. We can now refer to the sigma and pi types as dependent sum and dependent product without wanting to rip out our hair. Small victories!

Author: Samuel Breese

Created: 2018-10-18 Thu 13:10

Validate