5
$\begingroup$

It might just be a stupid question but I simply see no obvious reason why dependent sum type is a generalized form of product type. Concretely, the sigma type $\Sigma(x:S)T$ degenerates to a product type if $T$ does not depend on $x$ and is expressed to be $S\times T$ in this case.

Where the SUM part in dependent sum type is coming from? Also, the type of dependent functions is called dependent PRODUCT type. Might I ask why it's called product type as well? I kind of sense that it has something to do with algebraic data type but I can't get through it.

$\endgroup$
  • 2
    $\begingroup$ Just as a teaser: did you ever notice that $\sum_{i=1}^n m = n\times m$? $\endgroup$ – cody Sep 11 '17 at 18:33
  • $\begingroup$ @cody I do, but how should I interpret it? in another formalism, I would argue in this case n needs to have some structure, specifically, $n\times m = m + m + ... + m$ meaning the type of $n$ needs to be isomorphic to $\mathbb{Z}/|n|\mathbb{Z}$, which doesn't seem implied in the general case of dependent sums. $\endgroup$ – Jason Hu Sep 11 '17 at 18:38
  • $\begingroup$ @HuStmpHrrr What structure are you talking about? $\endgroup$ – Gilles 'SO- stop being evil' Sep 11 '17 at 19:38
10
$\begingroup$

Let's do products first. The usual cartesian product $A \times B$ is also called a binary product because we are making a product of two sets. We could make a ternary product $A \times B \times C$. What is the most general case? Well, to have an index set $I$ and a family of sets $X_i$, one for each $i \in I$, and then we make the product of all these $X_i$'s. This is written as $\prod_{i \in I} X_i$. When $I$ is infinite, it is called an infinitary product. Other products are a special case, for example if we take $I = \{1, 2\}$, $X_1 = A$ and $X_2 = B$ then $\prod_{i \in \{1,2\}} X_i = A \times B$, so a binary product is a special case of the general product.

We can do the previous paragraph in type theory, as there is nothing specific to sets there. Given a type family $i : I \vdash X(i) \ \mathsf{type}$, we may form the type $\prod (i : I) X(i)$. To get a binary product $A \times B$ as a special case, take $I = \mathsf{Bool}$, set $X(\mathsf{false}) = A$ and $X(\mathsf{true}) = B$.

Now let's try sums. I will assume you understand the sum of two sets or types, $A + B$. We could have a ternary sum, $A + B + C$. Again, there is a general case: take a family of sets $(X_i)_{i \in I}$ and form their sum. In set theory it is written as $\coprod_{i \in I} X_i$ and called coproduct, while in type theory it is written as $\sum (i : I) X(i)$ and called dependent sum. One way to see why people call it a sum is to consider how many elements it has. If $A$ has $a$ elements and $B$ has $b$ elements, then $A + B$ has $a + b$ elements. In general, if $X_i$ has $x_i$ elements, then $\sum (i : I) X_i$ has $\sum_i x_i$ elements.

We saw that the binary product is a special case of a general product. But it is also a special case of a dependent sum. Suppose $A = \{0, 1, 2\}$ and $B = \{0, 1\}$. Then $A \times B = B + B + B$. In general, if we want $A$-many copies of $B$, then that's $$A \times B = \underbrace{B + B + \cdots + B}_{A}$$ Of course, such notation is silly, so we prefer to take $I = A$ and $X_i = B$ and then the same thing is written as $$A \times B = \sum_{i \in I} X_i$$ or to confuse beginners $$A \times B = \sum_{a \in A} B.$$ This just says that $A$ times $B$ is the same thing as adding $A$-many $B$'s together. It's the first thing we're told about multiplication, except that here it's about sets, not numbers (but that's irrelevant, really).

$\endgroup$
  • $\begingroup$ as I raised it in a comment up there, it seems to me there is an implication of the structure of the first type $S$ as in my question. it seems to me $S$ needs to be isomorphic to $\mathbb{Z}/|S|\mathbb{Z}$ if it's finite, or $\mathbb{Z}$ if it's infinite. however, I see dependent sums as a representation of existential qualification, which doesn't seem to say anything about structure of $S$. when $S$ doesn't have that structure, your explanation doesn't seem sufficient. $\endgroup$ – Jason Hu Sep 11 '17 at 18:52
  • $\begingroup$ @HuStmpHrrr There's no structure on $S$. So if it's finite, it's isomorphic to $\mathbb{Z}/|S|\mathbb{Z}$, since with no structure “isomorphic” means “in bijection with”. $\endgroup$ – Gilles 'SO- stop being evil' Sep 11 '17 at 19:37
  • $\begingroup$ I explained the cases when $S$ is a finite set with decidable equality, but in general there need not be any special structure on any of these sets. The constructions are completely general. $\endgroup$ – Andrej Bauer Sep 11 '17 at 20:03
  • $\begingroup$ Perhaps you've got things backwards? Certain dependent sums can be viewed as coproducts of a discrete family of sets, and certain dependent sums can be seen as binary products, but dependent sums are more general than either of those concepts. For instance, they can be interpreted as giving the total space of a fibration (in homotopy type theory). $\endgroup$ – Andrej Bauer Sep 11 '17 at 21:02
  • $\begingroup$ great, that resolved my last bit of confusion. $\endgroup$ – Jason Hu Sep 11 '17 at 23:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.