Vector (Data Type)

Definition

A vector is a length-indexed list data type. Unlike ordinary lists, vectors carry their length as part of their type, enabling compile-time guarantees about size.

In Dependent Type Theory, vectors are typically defined as:

$\text{Vec}(A,n):\mathcal{U}$

where $A$ is the element type and $n:\mathbb{N}$ is the length. The type $\text{Vec}(A,n)$ contains lists of exactly $n$ elements of type $A$.

Construction

Vectors are typically constructed inductively:

• $\text{nil}:\text{Vec}(A,0)$ - The empty vector
• $\text{cons}:A\to \text{Vec}(A,n)\to \text{Vec}(A,n+1)$ - Prepending an element increases the length by one

Examples

• $\text{Vec}(\mathbb{N},3)$ - Vectors of exactly three natural numbers
• $\text{Vec}(\text{Bool},0)\cong 1$ - The empty vector is unique
• Operations like $\text{head}:\text{Vec}(A,n+1)\to A$ are total because the type guarantees non-emptiness

Properties

• The length is statically known and checked by the type system
• Operations like indexing, head, and tail can be made total
• Vector concatenation has type: $\text{Vec}(A,m)\to \text{Vec}(A,n)\to \text{Vec}(A,m+n)$
• Vectors are an example of a Dependent Pair: ${\Sigma }_{n:\mathbb{N}}\text{Vec}(A,n)$ represents lists with their length

Related Concepts

• Dependent Pair: Vectors with their length form a dependent pair
• Dependent Type Theory: The system enabling length-indexed types
• Type Constructor: Vector is a dependent type constructor