Product Type

Definition

A product type is a Type Constructor that combines two types $A$ and $B$ into a composite type. Given types $A$ and $B$, their product $A\times B$ consists of pairs $(a,b)$ where $a:A$ and $b:B$.

More generally, the product of types $A_1,A_2,\dots ,A_n$ is written $A_1\times A_2\times \cdots \times A_n$ and contains $n$-tuples $(a_1,a_2,\dots ,a_n)$ where $a_i:A_i$ for each $i$.

Type Rules

Product types are characterized by their introduction and elimination rules:

Introduction Rule

$\frac{a:Ab:B}{(a,b):A\times B}$

If we have $a:A$ and $b:B$, we can construct the pair $(a,b):A\times B$.

Elimination Rules

$\frac{p:A\times B}{{\pi }_1(p):A}\frac{p:A\times B}{{\pi }_2(p):B}$

From a pair $p:A\times B$, we can project out its components using ${\pi }_1$ and ${\pi }_2$.

Computation Rules

${\pi }_1(a,b)=a{\pi }_2(a,b)=b$

Eta Rule

For any $p:A\times B$, we have $p=({\pi }_1(p),{\pi }_2(p))$.

Category-Theoretic View

In category theory, the product type corresponds to the categorical product. The type $A\times B$ is the product of $A$ and $B$ with projection morphisms ${\pi }_1:A\times B\to A$ and ${\pi }_2:A\times B\to B$.

The product satisfies a universal property: for any type $C$ with morphisms $f:C\to A$ and $g:C\to B$, there exists a unique morphism $⟨f,g⟩:C\to A\times B$ such that ${\pi }_1\circ ⟨f,g⟩=f$ and ${\pi }_2\circ ⟨f,g⟩=g$.

Related Concepts

• Ordered Tuple: Elements of product types
• Sum Type: The dual construction for type theory
• Dependent Pair: A generalization where the second type depends on the first value
• Record Type: Product types with named fields
• Function Type: Related by currying via the isomorphism $(A\times B)\to C\cong A\to (B\to C)$
• Cartesian Product: The set-theoretic analogue