add intercalate and concat

src/Data/Vec.hs

@@ -158,6 +158,14 @@ intersperse _ (x :- Nil) = x :- Nil
 intersperse s (x :- xs)  = gcastWith (double n) (x :- s :- intersperse s xs)
   where n = sLength (x :- xs)
 
+
+-- | 'intercalate' @xs xss@ is equivalent to
+-- @('concat' ('intersperse' xs xss))@. It inserts the vector @xs@
+-- in between the vectors in @xss@ and concatenates the result.
+intercalate ∷ Vec a n → Vec (Vec a n) m → Vec a ((m :+ Pred m) :× n)
+intercalate xs xss = concat (intersperse xs xss)
+
+
 -- | 'foldl' applied to a binary operator, a starting value
 -- and a 'Vec' reduces the vector to a single value obtained
 -- by sequentially applying the operation from the left to the right.
@@ -186,6 +194,16 @@ foldr₁ f (x :- Nil)     = x
 foldr₁ f (x :- y :- ys) = f x (foldr₁ f (y :- ys))
 
 
+-- | The concatenation of all the elements of a vector of vectors.
+concat ∷ Vec (Vec a n) m → Vec a (m :× n)
+concat Nil = Nil
+concat (xs :- xss) = gcastWith proof (xs ⧺ concat xss)
+  where
+    n = sLength xs
+    m = sLength xss
+    proof = plus_commut n (m %:× n)
+
+
 -- | 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