add zips

src/Data/Vec.hs

@@ -184,27 +184,27 @@ transpose (xs :- xss) = gcastWith proof (zipWith (:-) xs (transpose xss))
 -- by sequentially applying the operation from the left to the right.
 foldl ∷ (a → b → a) → a → Vec b n → a
 foldl _ x Nil       = x
-foldl f x (y :- ys) = foldl f (f x y) ys
+foldl (⊗) x (y :- ys) = foldl (⊗) (x ⊗ y) ys
 
 
 -- | Same as "fold" but reduces the vector in the opposite
 -- direction: from the right to the left.
 foldr ∷ (a → b → b) → b → Vec a n → b
-foldr f x Nil     = x
+foldr _ x Nil     = x
-foldr f x (y:-ys) = f y (foldr f x ys)
+foldr (⊗) x (y:-ys) = y ⊗ (foldr (⊗) x ys)
 
 
 -- | Variant of 'foldl' which requires no starting value but
 -- applies only on nonempty 'Vec'
 foldl₁ ∷ (a → a → a) → Vec a (S n) → a
-foldl₁ f (x :- Nil)     = x
+foldl₁ _ (x :- Nil)     = x
-foldl₁ f (x :- y :- ys) = foldl₁ f (f x y :- ys)
+foldl₁ (⊗) (x :- y :- ys) = foldl₁ (⊗) (x ⊗ y :- ys)
 
 
 -- | As for 'foldl', a variant of 'foldr' with no starting point
 foldr₁ ∷ (a → a → a) → Vec a (S n) → a
-foldr₁ f (x :- Nil)     = x
+foldr₁ (⊗) (x :- Nil)     = x
-foldr₁ f (x :- y :- ys) = f x (foldr₁ f (y :- ys))
+foldr₁ (⊗) (x :- y :- ys) = x ⊗ (foldr₁ (⊗) (y :- ys))
 
 
 -- * Special folds
@@ -282,3 +282,37 @@ drop ∷ Sℕ n → Vec a m → Vec a (m :- n)
 drop SZ     x         = x
 drop (SS n) (x :- xs) = drop n xs
 
+
+-- * Zipping and unzipping vectors
+
+-- | 'zip' takes two vectors and returns a vector of corresponding pairs.
+-- If one input vectors is short, excess elements of the longer vector are
+-- discarded.
+--
+-- 'zip' is right-lazy:
+--
+-- > zip Nil ⊥ = Nil
+zip ∷ Vec a n → Vec b m → Vec (a, b) (Min n m)
+zip = zipWith (,)
+
+
+-- | 'zipWith' generalises 'zip' by zipping with the function given
+-- as the first argument, instead of a tupling function.
+-- For example, @'zipWith' (+)@ is applied to two vectors to produce the
+-- vector of corresponding sums.
+--
+-- 'zipWith' is right-lazy:
+--
+-- > zipWith f Nil ⊥ = Nil
+zipWith ∷ (a → b → c) → Vec a n → Vec b m → Vec c (Min n m)
+zipWith _ Nil _ = Nil
+zipWith _ _ Nil = Nil
+zipWith (⊗) (x :- xs) (y :- ys) = x ⊗ y :- zipWith (⊗) xs ys
+
+
+-- | 'unzip' transforms a list of pairs into a list of first components
+-- and a list of second components.
+unzip ∷ Vec (a, b) n → (Vec a n, Vec b n)
+unzip Nil             = (Nil, Nil)
+unzip ((x, y) :- xys) = (x :- xs, y :- ys)
+  where (xs, ys) = unzip xys