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?

Dichromatism

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.

Anis

Σ(x:A) B(x) type cannot be seen as a disjoint union of B(x) for all possible x∈A. If you produce B(x) for all possible x∈A, you get Π(x:A) B(x). – Dolce

@SassaNF: But disjoint union doesn't require you to produce B(x) for all possible x, in the same sense that Either a b doesn't need to hold both a and b. – Basophil

@Basophil yes, that's why "B(x) for all possible x∈A" needs clarifying – Dolce

@SassaNF: Does it? I feel it pretty clearly states that (as an example) Σ(x∈Nat) B(x) can be seen as B(0) ∨ B(1) ∨ B(2) ∨ ... – Basophil

@Basophil I find it weird that one should say that Either a b is a disjoint union of just two types, if any type X == X + ⊥. So it is difficult to talk about "all possible", where "some possible" is meant. Well, if no one else finds it weird, I'll just have to live with it :) – Dolce

@SassaNF There is a difference between talking about types as a whole and their values. Let's view types as sets. For constructing a disjoint union of sets, we need all the indexes. For example a disjoint union of sets B(1)={a,b}, B(2)={b,c}, B(3)={a,b} indexed by A={1, 2, 3} would be {(a,1),(b,1), (b,2), (c,2), (a,3), (b,3)}. Each member of such a set is just one index and one value. But each member of their product contain of course contains all values: {(a,b,a), (a,b,b), (a,c,a), (a,c,b), ...}. – Anis

@PetrPudlák oh well. I completely forgot how disjoint union deals with B(x)={}. ok, no pair will exist for some x if B(x) is not inhabited. – Dolce

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

Calvaria

I'd have expected choice l r True = r, matching Haskell's bool. – Fence

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.

Copal

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.

Tapis

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.

Tsushima

Answer 6

First, see what a co-product is.

A co-product is a terminal object A for all objects B_i such that for all arrows B_i -> X there is an arrow B_i -> A, and a unique A -> X such that the corresponding triangles commute.

You can view this as a Haskell data type A with B_i -> A being a bunch of constructors with a single argument of type B_i. It is clear then that for every B_i -> X it is possible to supply an arrow from A -> X such that through pattern-matching you could apply that arrow to B_i to get X.

The important connection to sigma types is that the index i in B_i can be of any type, not just a type of natural numbers.

The important difference from the answers above is that it does not have to have a B_i for every value i of that type: once you've defined B_i ∀ i, you have a total function.

The difference between Π and Σ, as may be seen from Petr Pudlak's answer, is that for Σ some of the values B_i in the tuple may be missing - for some i there may be no corresponding B_i.

The other clear difference between Π and Σ is that Π characterizes a product of B_i by providing i-th projection from the product Π to each B_i (this is what the function i -> B_i means), but Σ provides the arrows the other way around - it provides the i-th injection from B_i into Σ.

Dolce