Understanding zip and zipWith in Idris 2

Both zip and zipWith combine two sequences element-by-element. In Idris 2, these operations exist both for standard dynamic-length lists (List a) and fixed-length dependent vectors (Vect n a).

1. Standard Lists (List a)

For standard lists, zip and zipWith behave similarly to other functional languages like Haskell. If the input lists have unequal lengths, the resulting list truncates to the length of the shorter input list.

1.1 zip

zip takes two lists and pairs up their corresponding elements into a list of tuples.

$$\text{zip } [a_1, a_2] \, [b_1, b_2] = [(a_1, b_1), (a_2, b_2)]$$

import Data.List

-- Pairing equal-length lists
sampleZipList : List (Nat, String)
sampleZipList = zip [1, 2, 3] ["apple", "banana", "cherry"]
-- Result: [(1, "apple"), (2, "banana"), (3, "cherry")]

-- Truncating mismatched lengths
sampleZipTruncated : List (Nat, String)
sampleZipTruncated = zip [1, 2, 3, 4, 5] ["a", "b"]
-- Result: [(1, "a"), (2, "b")]

1.2 zipWith

zipWith takes a combining function $f : a \to b \to c$ along with two lists. It applies the function to each pair of corresponding elements.

$$\text{zipWith } f \, [a_1, a_2] \, [b_1, b_2] = [f(a_1, b_1), f(a_2, b_2)]$$

import Data.List

-- Pairwise addition
sampleZipWithList : List Nat
sampleZipWithList = zipWith (+) [1, 2, 3] [10, 20, 30]
-- Result: [11, 22, 33]

-- Combining different types using a custom function
formatItem : Nat -> String -> String
formatItem index name = show index ++ ". " ++ name

sampleFormatted : List String
sampleFormatted = zipWith formatItem [1, 2] ["Alice", "Bob"]
-- Result: ["1. Alice", "2. Bob"]

2. Length-Indexed Vectors (Vect n a)

When working with Data.Vect, the Idris 2 type checker enforces at compile-time that both vectors have the exact same length $n$.

2.1 Vector zip

$$\text{zip} : \text{Vect } n \, a \to \text{Vect } n \, b \to \text{Vect } n \, (a, b)$$

import Data.Vect

v1 : Vect 3 Nat
v1 = [1, 2, 3]

v2 : Vect 3 String
v2 = ["x", "y", "z"]

zippedVect : Vect 3 (Nat, String)
zippedVect = zip v1 v2
-- Result: [(1, "x"), (2, "y"), (3, "z")]

2.2 Vector zipWith

$$\text{zipWith} : (a \to b \to c) \to \text{Vect } n \, a \to \text{Vect } n \, b \to \text{Vect } n \, c$$

import Data.Vect

vAdd1 : Vect 3 Nat
vAdd1 = [1, 2, 3]

vAdd2 : Vect 3 Nat
vAdd2 = [10, 20, 30]

addedVect : Vect 3 Nat
addedVect = zipWith (+) vAdd1 vAdd2
-- Result: [11, 22, 33]

3. Advanced Application: Multidimensional zipWith

Because zipWith operates element-wise, nesting zipWith allows us to easily execute multi-dimensional matrix operations.

import Data.Vect

-- Matrix type definition (m rows, n columns)
Matrix : Nat -> Nat -> Type -> Type
Matrix m n a = Vect m (Vect n a)

-- Matrix Addition using nested zipWith:
-- 1. Inner zipWith (+) adds elements of two 1D row vectors.
-- 2. Outer zipWith applies that row-addition across all m rows.
addMatrix : Num a => Matrix m n a -> Matrix m n a -> Matrix m n a
addMatrix = zipWith (zipWith (+))

4. Summary Table