Dependent Types: How is the dependent pair type analogous to a disjoint union?

Question

I've been studying dependent types and I understand the following:

1. Why universal quantification is represented as a dependent function type. ∀(x:A).B(x) means “for all x of type A there is a value of type B(x)”. Hence it's represented as a function which when given any value x of type A returns a value of type B(x).
2. Why existential quantification is represented as a dependent pair type. ∃(x:A).B(x) means “there exists an x of type A for which there is a value of type B(x)”. Hence it's represented as a pair whose first element is a particular value x of type A and whose second element is a value of type B(x).

Aside: It's also interesting to note that universal quantification is always used with material implication while existential quantification is always used with logical conjunction.

Anyway, the Wikipedia article on dependent types states that:

The opposite of the dependent type is the dependent pair type, dependent sum type or sigma-type. It is analogous to the coproduct or disjoint union.

How is it that a pair type (which is normally a product type) is analogous to a disjoint union (which is a sum type)? This has always confused me.

In addition, how is the dependent function type analogous to the product type?

Answer 1

The confusion arises from using similar terminology for the structure of a Σ type and for how its values look like.

A value of Σ(x:A) B(x) is a pair (a,b) where a∈A and b∈B(a). The type of the second element depends on the value of the first one.

If we look at the structure of Σ(x:A) B(x), it's a disjoint union (coproduct) of B(x) for all possible x∈A.

If B(x) is constant (independent of x) then Σ(x:A) B will be just |A| copies of B, that is A⨯B (a product of 2 types).

---

If we look at the structure of Π(x:A) B(x), it's a product of B(x) for all possible x∈A. Its values could be viewed as |A|-tuples where a-th component is of type B(a).

If B(x) is constant (independent of x) then Π(x:A) B will be just A→B - functions from A to B, that is Bᴬ (B to A) using the set-theory notation - the product of |A| copies of B.

---

So Σ(x∈A) B(x) is a |A|-ary coproduct indexed by the elements of A, while Π(x∈A) B(x) is a |A|-ary product indexed by the elements of A.

Answer 2

A dependent pair is typed with a type and a function from values of that type to another type. The dependent pair has values of pairs of a value of the first type and a value of the second type applied to the first value.

data Sg (S : Set) (T : S -> Set) : Set where
  Ex : (s : S) -> T s -> Sg S T

We can recapture sum types by showing how Either is canonically expressed as a sigma type: it's just Sg Bool (choice a b) where

choice : a -> a -> Bool -> a
choice l r True  = l
choice l r False = r

is the canonical eliminator of booleans.

eitherIsSg : {a b : Set} -> Either a b -> Sg Bool (choice a b)
eitherIsSg (Left  a) = Sg True  a
eitherIsSg (Right b) = Sg False b

sgIsEither : {a b : Set} -> Sg Bool (choice a b) -> Either a b
sgIsEither (Sg True  a) = Left  a
sgIsEither (Sg False b) = Right b

Answer 3

Building on Petr Pudlák’s answer, another angle to see this in a purely non-dependent fashion is to notice that the type Either a a is isomorphic to the type (Bool, a). Although the latter is, at first glance, a product, it makes sense to say it’s a sum type, as it is the sum of two instances of a.

I have to do this example with Either a a instead of Either a b, because for the latter to be expressed as a product, we need – well – dependent types.

Answer 4

Good question. The name could originate from Martin-Löf who used the term "Cartesian product of a family of sets" for the pi type. See the following notes, for example: http://www.cs.cmu.edu/afs/cs/Web/People/crary/819-f09/Martin-Lof80.pdf The point is while a pi type is in principle akin to an exponential, you can always see an exponential as an n-ary product where n is the exponent. More concretely, the non-dependent function A -> B can be seen as an exponential type B^A or an infinite product Pi_{a in A} B = B x B x B x ... x B (A times). A dependent product is in this sense a potentially infinite product Pi_{a in A} B(a) = B(a_1) x B(a_2) x ... x B (a_n) (once for every a_i in A).

The reasoning for dependent sum could be similar, as you can see a product as an n-ary sum where n is one of the factors of the product.

Answer 5

This is probably redundant with the other answers at this point, but here is the core of the issue:

How is it that a pair type (which is normally a product type) is analogous to a disjoint union (which is a sum type)? This has always confused me.

But what is a product but a sum of equal numbers? e.g. 4 × 3 = 3 + 3 + 3 + 3.

The same relationship holds for types, or sets, or similar things. In fact, the nonnegative integers are just the decategorification of finite sets. The definitions of addition and multiplication on numbers are chosen so that the cardinality of a disjoint union of sets is the sum of the cardinalities of the sets, and the cardinality of a product of sets is equal to the product of the cardinalities of the sets. In fact, if you substitute "set" with "herd of sheep", this is probably how arithmetic was invented.