add more folds

src/Data/Vec.hs

@@ -22,7 +22,7 @@ import Data.Nat
 import Data.Bool
 import Data.Char         (Char)
 import Data.Function     ((∘), ($))
-import Data.TypeClass    (Show, IsList, IsString, Eq) 
+import Data.TypeClass    (Show, IsList, IsString, Eq, Num)
 import Data.Singletons   (SingI, sing)
 
 import qualified Data.TypeClass as T
@@ -196,6 +196,8 @@ foldr₁ f (x :- Nil)     = x
 foldr₁ f (x :- y :- ys) = f x (foldr₁ f (y :- ys))
 
 
+-- * Special folds
+
 -- | The concatenation of all the elements of a vector of vectors.
 concat ∷ Vec (Vec a n) m → Vec a (m :× n)
 concat Nil = Nil
@@ -207,7 +209,7 @@ concat (xs :- xss) = gcastWith proof (xs ⧺ concat xss)
 
 
 -- | Map a function over all the elements of a vector and concatenate
--- the resulting vectos.
+-- the resulting vectors.
 concatMap ∷ (a → Vec b n) → Vec a m → Vec b (m :× n)
 concatMap f = concat ∘ map f
 
@@ -219,6 +221,38 @@ replicate SZ     _ = Nil
 replicate (SS n) a = a :- replicate n a
 
 
+-- | 'and' returns the conjunction of a container of bools.
+and ∷ Vec 𝔹 (S n) → 𝔹
+and = foldr₁ (∧)
+
+
+-- | 'or' returns the disjunction of a container of bools.
+or ∷ Vec 𝔹 (S n) → 𝔹
+or = foldr₁ (∨)
+
+
+-- | Determines whether any element of the structure satisfies the predicate.
+any ∷ (a → 𝔹) → Vec a n → 𝔹
+any _ Nil = T
+any p xs  = or (map p xs)
+
+
+-- | Determines whether all elements of the structure satisfy the predicate.
+all ∷ (a → 𝔹) → Vec a n → 𝔹
+all _ Nil = T
+all p xs  = and (map p xs)
+
+
+-- | The 'sum' function computes the sum of the numbers of a vector.
+sum ∷ Num a ⇒ Vec a n → a
+sum = foldr (T.+) 0
+
+
+-- | The 'product' function computes the product of the numbers of a vector.
+product ∷ Num a ⇒ Vec a n → a
+product = foldr (T.*) 0
+
+
 -- | 'take' @n@ applied to a 'Vec', returns the first @n@ element
 -- of the vector
 take ∷ Sℕ n → Vec a m → Vec a n