I'm trying to understand $\Sigma$– and $\Pi$– types in dependent type theory. On the bottom of page 9 of this document, there are two equations giving a justification for the names of $\Pi$– and $\Sigma$ via an arithmetic interpretation of types.
I'll use the example of two simple domains to keep things concrete: Booleans (containing values true and false) and Alphas (containing values A, B, and C).
I understand how the space of functions from Booleans to Alphas can be thought of as exponentiation; there are $3^2$ ways to define a function $Boolean \rightarrow Alpha$:
-
$True \rightarrow A, False \rightarrow A$
-
$True \rightarrow A, False \rightarrow B$
-
$True \rightarrow A, False \rightarrow C$
-
$True \rightarrow B, False \rightarrow A$
-
…
For $\Pi$-types, we make the codomain type of the function dependent on the domain. I think this means that we would have a function $Boolean \rightarrow X(Boolean)$, and $X(Boolean)$ would have to co-vary with the domain value, so we would only have one possible function definition (which maps $True \rightarrow X(True)$ and $False \rightarrow X(False)$). I don't see where a product calculation applies here (which tells me I haven't understood $\Pi$-types).
My understanding of $\Sigma$-types is that they are tuples with the second element depending on the first. Here, again, I saw only 2 possible tuples: $(True, X(True)$ and $(False, X(False)$. I do not see where a sum calculation applies.
Best Answer
I'm going to be even more concrete than you and fill in the choice of $X$ in a way that I hope will be illuminating.
The note in the linked document is about the specific case of tuples, taking advantage of types $\overline{m}$ (where $m : \mathbb{N}$) that are inhabited by exactly $m$ elements; $\overline{m} = \{0, 1, \dots, m-1\}$. Altenkirch has previously demonstrated that $\overline{m+n}$ has as many elements as $\overline{m} + \overline{n}$, where the $+$ on the left is adding numbers and the $+$ on the right is the disjoint union of types. Similarly, multiplication of numbers corresponds here to the type-theoretic product, and as you observe, the function type $\overline{n}\rightarrow\overline{m}$ has the same number of elements as the type $\overline{m^n}$, namely $m^n$.
We now move on to the dependent product and sum.
Altenkirch's arithmetic claims for these are that for $m : \mathbb{N}$ and $f : \overline{m} \rightarrow \mathbb{N}$, we have:
(I've changed the notation a bit just because the original has some deliberate but potentially confusing overlap between numbers and their corresponding finite types.)
Your types of Booleans and Alphas are equivalent to $\overline{2}$ and $\overline{3}$.
When you form your $\Pi x:\mathrm{Boolean}\mathbin{.}X\,x$, this stands for the type of functions where a Boolean comes in, the result type can vary depending on whether that Boolean was true or false, and the result's value is of that correct type. Here, $X : \mathrm{Boolean} \rightarrow \mathbf{Type}$ is the thing which tells us the type of the result. A function $\phi$ of this $\Pi$-type is determined by the pair of values $(\phi(\mathrm{True}), \phi(\mathrm{False}))$ it takes in $X\;\mathrm{True} \times X\;\mathrm{False}$. For example, if $X\;\mathrm{True}$ is $\overline{7}$ and $X\;\mathrm{False}$ is $\overline{4}$, then a perfectly good function would be the one for which $\phi(\mathrm{True}) = 5$ and $\phi(\mathrm{False}) = 1$. We can see that for this $X$, the total number of possible functions is $7 \times 4$; and for a general $X$ it will be the product of the sizes of $X\;\mathrm{True}$ and $X\;\mathrm{False}$. That is what Altenkirch asserted in the special case of $m = 2$, and hopefully the behaviour for more general $m$ will now be clearer.
Turning to $\Sigma$-types, you propose $\Sigma x : \mathrm{Boolean}\mathbin{.}X x$ with $X$ as above. Something of this type consists of a Boolean $x$, together with a value in $X\;x$. So it is either $(\mathrm{True}, y)$ where $y : X\;\mathrm{True}$, or it is $(\mathrm{False}, z)$ where $z : X\;\mathrm{False}$. Again following the example just above, if $X\;\mathrm{True}$ is $\overline{7}$ and $X\;\mathrm{False}$ is $\overline{4}$, then our complete repertoire of elements is: $$ (\mathrm{True}, 0), (\mathrm{True}, 1), (\mathrm{True}, 2),(\mathrm{True}, 3),(\mathrm{True}, 4),(\mathrm{True}, 5),(\mathrm{True}, 6)\\ (\mathrm{False}, 0), (\mathrm{False}, 1), (\mathrm{False}, 2), (\mathrm{False}, 3) $$ There are evidently $7 + 4$ inhabitants of this type. For a general $X$, we would get the sum of the sizes of $X\;\mathrm{True}$ and $X\;\mathrm{False}$, consistent with Altenkirch's statement in the case $m=2$.