Ordered Tuple

Definition

An ordered tuple is a finite sequence of elements where each position may have a distinct type. In type theory, an $n$-tuple is an element of a product type.

For types $A_1,A_2,\dots ,A_n$, an ordered tuple $(a_1,a_2,\dots ,a_n)$ has type $A_1\times A_2\times \cdots \times A_n$, where each $a_i:A_i$.

Two ordered tuples $(a_1,a_2,\dots ,a_n)$ and $(b_1,b_2,\dots ,b_m)$ are equal if and only if $n=m$ and $a_i=b_i$ for all $i$.

Type-Theoretic Perspective

In type theory, tuples are built from the product type constructor. The product type $A\times B$ has:

• Introduction rule: Given $a:A$ and $b:B$, we can form $(a,b):A\times B$
• Elimination rules: Projection functions ${\pi }_1:A\times B\to A$ and ${\pi }_2:A\times B\to B$ where ${\pi }_1(a,b)=a$ and ${\pi }_2(a,b)=b$

For $n$-tuples, this generalizes to $n$ projection functions ${\pi }_i:A_1\times \cdots \times A_n\to A_i$ for $i=1,\dots ,n$.

Special Cases

• A 2-tuple $(a,b):A\times B$ is called an ordered pair
• A 3-tuple $(a,b,c):A\times B\times C$ is called an ordered triple
• The unit type $1$ can be viewed as a 0-tuple

Properties

• Components may have different types: $(3,\text{true},"hello"):\mathbb{N}\times \text{Bool}\times \text{String}$
• Tuples can be nested: $((a,b),c):(A\times B)\times C$ is distinct from $(a,(b,c)):A\times (B\times C)$

Related Concepts

• Product Type: The type-theoretic generalization of tuples
• Cartesian Product: The set-theoretic construction $A\times B=\{(a,b)\mid a\in A,b\in B\}$
• Dependent Pair: A generalization where the second type may depend on the first value
• Record Type: Tuples with named fields
• Function Type: The dual to product types in type theory