diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs index a38a81a..0ed16ef 100644 --- a/src/Data/Vec.hs +++ b/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, Num) +import Data.TypeClass (Show, Eq, Ord, Num, IsList, IsString) import Data.Singletons (SingI, sing) import qualified Data.TypeClass as T @@ -174,7 +174,7 @@ intercalate xs xss = concat (intersperse xs xss) -- > transpose [[1,2,3],[4,5,6]] == [[1,4],[2,5],[3,6]] -- transpose ∷ SingI n ⇒ Vec (Vec a n) m → Vec (Vec a m) n -transpose Nil = replicate Nil +transpose Nil = replicate Nil transpose (xs :- xss) = gcastWith proof (zipWith (:-) xs (transpose xss)) where proof = min_self (sLength xs) @@ -197,16 +197,17 @@ 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₁ _ (x :- Nil) = x +foldl₁ _ (x :- Nil) = x 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₁ (⊗) (x :- Nil) = x +foldr₁ _ (x :- Nil) = x foldr₁ (⊗) (x :- y :- ys) = x ⊗ (foldr₁ (⊗) (y :- ys)) + -- * Special folds -- | The concatenation of all the elements of a vector of vectors. @@ -259,6 +260,16 @@ all _ Nil = T all p (x :- xs) = and (map p (x :- xs)) +-- | The least element of a vector. +minimum ∷ Ord a ⇒ Vec a (S n) → a +minimum = foldr₁ T.min + + +-- | The largest element of a vector. +maximum ∷ Ord a ⇒ Vec a (S n) → a +maximum = foldr₁ T.max + + -- | The 'sum' function computes the sum of the numbers of a vector. sum ∷ Num a ⇒ Vec a n → a sum = foldr (T.+) 0 @@ -283,6 +294,7 @@ 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. @@ -310,8 +322,8 @@ 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' transforms a vectors of pairs into a vector of first components +-- and a vector 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)