4
$\begingroup$

Based on following sentence

In type theory, commonly used in programming languages, a tuple has a product type; this fixes not only the length, but also the underlying types of each component.

I come to the conclusion that there are two different approaches:

  1. In set theory tuples are "just tuples" and the 1-tuple $(x) \neq x$.
  2. In type theory tuples have a type that is defined by a Cartesian product. So e.g. $(x_1,x_2)\in X\times X$ with $x_1,x_2\in X$. So for a 1-tuple it should be $(x)\in X$ with $x\in X$. Because $x,(x)\in X$, I think that in this theory $(x) = x$.

Is that true so far? If yes, is also $\{x\} = x$ in type theory?

$\endgroup$
3
  • 1
    $\begingroup$ Since Haskell (ghci) gives True for (x) == x I would answer yes to your first question. $\endgroup$
    – T'x
    Commented Jan 3, 2016 at 20:29
  • $\begingroup$ Are you sure that Haskell is a good reference for that? Is it true for only type theory or for both? $\endgroup$
    – andrew
    Commented Jan 3, 2016 at 20:32
  • $\begingroup$ Haskell is no reference at all, although it is very strict with types. It is only one incarnation of type theory. I think in set theory it should be true aswell, since the product-operation of sets needs at least two sets and therefore 1-tuples are not necessary (i.e. I guess 1-tuples don't appear in set theory so the question itself is obsolete). $\endgroup$
    – T'x
    Commented Jan 3, 2016 at 20:48

1 Answer 1

2
$\begingroup$

I believe that a correct answer to your question is "it depends on what do you mean by $1$-ary product of types".

A possible solution would be to identify every type $T$ with its unary product: if that's the case then $(x) = x$.

Of course you could also decide that the unary product of a type $T$ is not the type $T$ but it's a new type $\prod T$ that has:

  • a constructor $$(\_) \colon T \to \prod T$$
  • an eliminator $$\pi \colon \prod T \to T$$
  • and computational rules telling you that $$\forall x \in T\; \pi((x))=x$$ $$\forall z \in \prod T\; (\pi(z))=z\ .$$

About the last question, whether $\{x\}=x$ is true, the answer is clearly no in type theory. This is due to the fact that $\{x\}$ and $x$ have two different types: namely if $T$ is the type of $x$, hence $x \in T$, then $\{x\} \in \mathcal P(T)$, where by $\mathcal P(T)$ I mean the type of subtypes of $T$, which is different by $T$.

Hope this helps.

$\endgroup$
2
  • $\begingroup$ So it doesn't depend on whether you are in set or type theory at all? What are the most common solutions for defining the unary Cartesian product? $\endgroup$
    – andrew
    Commented Jan 3, 2016 at 22:15
  • $\begingroup$ @andrew Both the solutions I've described above are used, each one has its advantages: for instance the unary-product-as-the-type approach is simpler and gives a simpler notation, on the other hand if you want to use a general product operation (for instance if you need a dependent product operation) treating unary products as new types can be a better choice. $\endgroup$ Commented Jan 4, 2016 at 18:13

You must log in to answer this question.

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