0
$\begingroup$

Introduction:

Hi, I'm quite new to types so apologies in advance for the basic question and for any abuse of terminology. I believe I have a critical misunderstanding of dependent product types (and probably about types in general to be quite honest). My questions is based on a reading of Andrej's very helpful answer here.

I see the relationship between dependent sum types and the cartesian product, but I do not see the relationship between dependent product types and the cartesian product.

Question / Ask:

I was wondering if someone could provide a slower, step-by-step walkthrough of how to get to cartesian products from a special case of dependent product types (specifically how we get an ordered tuple from a dependent function).

My Thoughts:

In the first and second paragraphs of Andrej's answer, he relates a binary product to a dependent product type, stating first that we can write a binary product of sets as $\Pi_{i\in I}X_{i}$ and then stating second that we can write a dependent product type as $\Pi(i:I)X(i)$ which can then be used to get a binary product $A \times B$ as a special case if we take $I = \text{Bool}$, $X(\text{false})=A$, and $X(\text{true})=B$.

However, in my head these two $\Pi$ symbols mean something fairly different. In the first ($\Pi_{i\in I}X_{i}$), we are describing a set of ordered tuples $\{(x_1,x_1,\ldots,x_n) \space | \space x_1 \in X_1 , x_2 \in X_2, \ldots, x_n \in X_n\}$ where every combination of $(x_1, x_2, \ldots, x_n)$ is accounted for, whereas in the second ($\Pi(i:I)X(i)$), we are describing the type of a function that maps every element $i : I$ to an element in $X(i)$, where it's not necessarily true that for every $x \in X(i)$ there exists a function $f_x$ such that $f_x(i) = x$. How do we get an ordered tuple from a function?

To add to my confusion, the explanation of dependent product types on ncatlab here explicitly states the following:

It [dependent product types] includes function types as the special case when B is not dependent on A. Note that a binary product type is rather different, being actually a special case of a dependent sum type.

$\endgroup$
1
  • $\begingroup$ The nLab page was badly worded; I've amended it. The binary product type is a special case of both a dependent sum type and a dependent product type, specialised in two different ways. $\endgroup$
    – varkor
    Jul 11, 2022 at 23:26

1 Answer 1

1
$\begingroup$

Lets introduce $[n] = \{1,...,n\}$ as a convenience type and look a function $f$ in $\Pi (i:[n]) X(i)$. Now $f[i]$ maps to $x_i \in X_i$. So we could think of $f$ as an ordered sequence/tuple: $f \simeq (x_1,...,x_n)$. Of course for different indexing types its not an ordered tuple in the "classical integer index" sense.

Also $\Pi (i:[n]) X(i)$ contains all of the $n$-long tuples and just some as you thought; so for every $x \in X_i$ there is $f_x: \Pi(i:I)X(i)$ with $f_X(i) = x$.

The last quote is easy to misunderstand; what they try to say is $A \times B = \Sigma (a:A) B $. Where the second object is a dependent sum type $\Sigma (a:A) B(a)$. With $B(a) = B$ constant. I usually think of inhabitants of $\Sigma (a:A) B(a)$ as a pairs $(a, b_a \in B(a))$ and of $\Pi(i:I)X(i)$ as functions $f(i) = x_i \in X_i$. At "runtime" the a function can be evaluated at any $i$ but a pair is fixed.

$\endgroup$
1
  • $\begingroup$ Thank you, the second paragraph especially helped clear my confusion—specifically the notion that all n-long tuples are contained in the type. $\endgroup$
    – NNNComplex
    Jul 12, 2022 at 14:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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