Dependent Product

Definition

A dependent product (or dependent function type) is a generalization of Function Type where the output type may depend on the input value.

The dependent product type is written ${\Pi }_{x:A}B(x)$ or $\Pi x:A.B(x)$, where $A$ is a type and $B:A\to \mathcal{U}$ is a type family indexed by $A$.

An element of ${\Pi }_{x:A}B(x)$ is a function $f$ such that for each $a:A$, we have $f(a):B(a)$.

Type Rules

• Introduction rule: Given an expression $e:B(x)$ with free variable $x:A$, we can form $\lambda x.e:{\Pi }_{x:A}B(x)$.
• Elimination rule: Given $f:{\Pi }_{x:A}B(x)$ and $a:A$, we have $f(a):B(a)$.
• Computation rule (β-rule): $(\lambda x.e)(a)\equiv e[a/x]$

Examples

• Polymorphic Identity Function: ${\Pi }_{A:\mathcal{U}}A\to A$ takes a type and returns the identity function on that type
• vectors: ${\Pi }_{n:\mathbb{N}}A\to \text{Vec}(A,n)\to \text{Vec}(A,n+1)$ might prepend an element to vectors of any length
• Universal quantification: The proposition $\forall x:A.P(x)$ corresponds to ${\Pi }_{x:A}P(x)$

Special Cases

When $B$ is a constant type family (does not depend on $x$), the dependent product reduces to the ordinary Function Type: ${\Pi }_{x:A}B\cong A\to B$.

Related Concepts

• Function Type: The non-dependent special case
• Dependent Sum: The dual construction where pairs have dependent components
• Product Type: The non-dependent product
• Lambda Calculus: The foundation for function abstraction