5
$\begingroup$

This is in the context of the Type Theory system $\lambda P$ as presented in Chapter 5 of "Type Theory and Formal Proof: An Introduction" by Rob Nederpelt and Herman Guevers.

Since I am unsure of how standard $\lambda P$ is in the literature, I'll just mention that it is a system of type theory in which in addition to terms depending on terms, there are types depending on terms.

The full paragraph in the text is:

"Martin-Löf (1980) calls a $\Pi$-type the Cartesian product of a family of types. If one considers A to be a finite type, say with two elements $a_1$ and $a_2$, then $\Pi x: A. B$ is indeed the same as $B[x := a_1] \times B[x := a_2]$, the Cartesian product and as a generalization of the function space (if $x \notin \operatorname{FV}(B)$, then $\Pi x : a. B$ is just $A \to B$)"

This equivalence to Cartesian products is not further explained. I have tried to make sense of it by considering concrete examples but have fallen short.

One possible reason I am failing to understand this is that I do not understand how (or even know if it is possible that) a type in beta-normal form can contain a free term, whereas in systems $\lambda \to$, $\lambda 2$, $\lambda \underline{\omega}$, I had no issue finding examples of the situations equivalent to this (for terms dependent on terms, terms dependent on types, and types dependent on terms).

$\endgroup$
3
  • $\begingroup$ I don't know this type theory, but it looks like the standard isomorphism given by $\lambda f.(f\,a_1,f\,a_2) : (\Pi(x:A)B)\to B\times B$ and $\lambda(b_1,b_2).(a_1\mapsto b_1, a_2\mapsto b_2):B\times B \to \Pi(x:A)B$. Does that make sense in your setting? $\endgroup$ Jul 5, 2020 at 3:54
  • $\begingroup$ @JackozeeHakkiuz Thanks for the comment. After about 5 minutes staring at that expression, I'm unable to parse it, so I think not. Maybe it is only a different notation and I should have understood, but I cannot see how. EDIT: I see you have capitalized the pi lol, that might've helped let me see. $\endgroup$
    – csgosmorf
    Jul 5, 2020 at 4:04
  • $\begingroup$ @JackozeeHakkiuz It looks familiar enough that perhaps with a bit of notational translating I could understand it. I am confused by the fact that $f$ does not appear to be typed and am confused as to what $(f_{a1},f_{a2})$ represents within the body (?) of an abstraction(?) $\endgroup$
    – csgosmorf
    Jul 5, 2020 at 4:11

1 Answer 1

6
$\begingroup$

Welcome to MSE ^_^

I am not familiar with Nederpelt and Guevers' book, so I'm sorry if the language I use is not the language used in your reference. I will try to explain everything as I go, in case some notation I use is unfamiliar.

A dependent type $\prod_{a:A} B(a)$ is indeed a generalization of the cartesian product. The easiest example is when $A = \text{Bool}$ with two values $T$ and $F$. Let's consider two types $B(T)$ and $B(F)$. Then the type $\prod_\text{x:Bool}B(x)$ is inhabited by functions $f$ so that $f(T) : B(T)$ and $f(F) : B(F)$. One can view such a function $f$ as selecting an element $f(x)$ of each $B(x)$.

Now, there is a natural (and eventually obvious) identification between these functions $f$ and a pair $(b_1,b_2) : B(T) \times B(F)$. Our function $f$ is totally specified by $f(T)$ and $f(F)$, so we can package those values up as a tuple. Dually, a tuple whose first element is in $B(T)$ and second is in $B(F)$ gives us the data of a function!

$$\left ( f : \prod_{x:\text{Bool}}B(x) \right ) \mapsto \bigg ( (f(T),f(F)) : B(T) \times B(F) \bigg )$$

$$\bigg ( (x,y) : B(T) \times B(F) \bigg ) \mapsto \left ( \lambda b . \text{if } b = T \text{ then } x \text{ else } y : \prod_{b:\text{Bool}} B(b) \right )$$

Following Homotopy Type Theory, my preferred interpretation of this phenomenon is geometric.

Consider the following picture:

fibres over Bool

Here we have two types, which you should view as "floating above" the type of booleans below. Then elements of $\prod_{x : \text{Bool}}B(x)$ are exactly functions out of $\text{Bool}$ so that the value of $f(x)$ lies above $x$. In this way, as I said earlier, an element of the $\prod$-type selects one element out of each of the pieces. Hopefully this picture, and the idea of a $\prod$-type as a "selector" helps explain in a different way why $\prod_{x : \text{Bool}}B(x)$ is the same as $B(T) \times B(F)$. They both represent ways to choose one element from $B(T)$ and one from $B(F)$!

At this point I will suggest a small exercise. Let $\mathbf{3}$ denote a type with three values: $x$, $y$, and $z$. Now fix 3 new types, say $B(x)$, $B(y)$, and $B(z)$. Do you see why $\prod_{t:\mathbf{3}}B(t)$ is the same as $B(x) \times B(y) \times B(z)$? Make sure you understand why that is before moving on!


Let's move on to a trickier example now. Let $\mathbb{Z}$ denote the type of integers. Now pick a type $B(n)$ for each integer $n : \mathbb{Z}$. What does an element of $\prod_{n : \mathbb{Z}} B(n)$ look like?

You should train yourself, pavlovianly, to pull the following picture to mind:

fibres over Z

Again, we have a function out of $\mathbb{Z}$, which selects one element of each $B(n)$. The analogy to cartesian products is slightly less clear now. But this is where we start generalizing. If $f : \prod_{n : \mathbb{Z}}B(n)$, then what type might you give the following "term"?

$$(\ldots, f(-2), f(-1), f(0), f(1), f(2), \ldots)$$

This "term" is a tuple with $\mathbb{Z}$ many entries, and the $n$th entry comes from $B(n)$. If you had to assign a type to something like this, you might say it has type $\ldots \times B(-2) \times B(-1) \times B(0) \times B(1) \times B(2) \times \ldots$.

It is in this sense, that $\prod_{n : \mathbb{Z}} B(n)$ is a "cartesian product". The functions inhabiting this $\prod$-type have exactly the same information as an infinite tuple indexed by $\mathbb{Z}$! But because functions are finitary, they can be expressed in type theory, while formalizing an "infinite tuple" is almost impossible!


It's time for the last example. What about $\prod_{a:A}B(a)$? Again, the response should be pavlovian:

fibres over an arbitrary type A

Here we write $B$ to mean the collection of all the $B(a)$s viewed as one type. (As a remark, $B$ is exactly the sum-type $\Sigma_{a:A}B(a)$!) Then functions $f : A \to B$ so that $f(a) : B(a)$ are exactly elements of $\prod_{a:A}B(a)$. Again, we are selecting one element from each $B(a)$. So we can think of this function as a "tuple indexed by $A$", and so we identify it with a "cartesian product" of one type for each element of $A$! This is exactly where the $\prod$ notation comes from - we are producting together the family of types $B(a)$. This is extra useful, as $A$ might not be ordered neatly in the way that $\mathbb{Z}$ is. So it is less clear how one might write a tuple with one entry for each value of $A$! In this case, if we want to show that we're thinking of $f$ as a tuple rather than a function, we might write something like $(f_a)_{a:A} : \prod_{a:A} B(a)$.


This was a long ride, but I hope it made some sense! I know $\prod$-types confused me when I was first getting started, but after I worked these "bubble" pictures into my subconscious (the bubbles are called "fibres", by the way), their properties became really obvious! The important thing to keep in mind is that, as far as type theory is concerned, a $\prod$-type is just a type full of functions. Their normal forms look just like functions. You can evaluate them, and you create them via $\lambda$-abstraction. But as humans, we have the power to think of them as more than functions. The confusion you're feeling with regards to $f$ not having a clean codomain is common. It is solved (as I alluded to earlier) by the introduction of $\sum$-types, but even without $\sum$-types, $\prod$-types have introduction and elimination rules just like anything else - there's nothing scary lying under the hood.

To get some practice, can you see (intuitively!) why the following facts must be true? Can you then formalize this intuition with an equivalence of types?

  • $\prod_{x:\mathbf{1}}A(x) \cong A(x)$ when $\mathbf{1}$ is the type with only one inhabitat

  • $\prod_{x:X}B(x) \cong \mathbf{0}$ whenever one of the $B(x)$s are $\mathbf{0}$ (the type with no inhabitants)


I hope this helps ^_^

$\endgroup$
2
  • 1
    $\begingroup$ Apparently MSE discourages "thanks" comments, but since I'm human and I cannot even publicly up-vote yet (need 15 reputation), I want to say thanks! After about two hours of trying to make sense of this, it clicked. Thank you kindly. $\endgroup$
    – csgosmorf
    Jul 5, 2020 at 8:17
  • $\begingroup$ Happy to help ^_^ $\endgroup$ Jul 5, 2020 at 15:25

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .