Dependent Types: How is the dependent pair type an

问题:

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?

回答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.

回答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

回答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.

回答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.

回答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.

回答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 Σ.