I've been studying dependent types and I understand the following:
∀(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).∃(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?
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.