add concatMap

src/Data/Vec.hs

@@ -155,8 +155,10 @@ reverse (y :- ys) = gcastWith proof (reverse ys ⧺ (y :- Nil))
 intersperse ∷ a → Vec a n → Vec a (n :+ Pred n)
 intersperse _ Nil        = Nil
 intersperse _ (x :- Nil) = x :- Nil
-intersperse s (x :- xs)  = gcastWith (double n) (x :- s :- intersperse s xs)
+intersperse s (x :- xs)  = gcastWith proof (x :- s :- intersperse s xs)
-  where n = sLength (x :- xs)
+  where
+    n     = sLength xs
+    proof = double (SS n)
 
 
 -- | 'intercalate' @xs xss@ is equivalent to
@@ -204,6 +206,12 @@ concat (xs :- xss) = gcastWith proof (xs ⧺ concat xss)
     proof = plus_commut n (m %:× n)
 
 
+-- | Map a function over all the elements of a vector and concatenate
+-- the resulting vectos.
+concatMap ∷ (a → Vec b n) → Vec a m → Vec b (m :× n)
+concatMap f = concat ∘ map f
+
+
 -- | Applied to a singleton natural @n@ and a value produces
 -- a vector obtained by duplicating the value @n@ times
 replicate ∷ Sℕ n → a → Vec a n