couple of matrix operations using dependent type

Matrix.idr

import Data.Vect

-- matrix representation using vectors
Matrix : (rows : Nat) -> (cols : Nat) -> (elem : Type) -> Type
Matrix rows cols elem = Vect rows (Vect cols elem)

-- add corresponding elements from two vectors
vector_op : Num elem => ((elem, elem) -> elem) -> Vect c elem -> Vect c elem -> Vect c elem
vector_op op av bv = let ts = zip av bv in map op ts

-- matrix transpose operation
transp : Matrix m n elem -> Matrix n m elem
transp [] = replicate _ []
transp (x :: xs) = let txs = transp xs in transpHelper x txs
                      where
                        transpHelper : Vect n elem -> Matrix n m elem -> Matrix n (S m) elem
                        transpHelper [] [] = []
                        transpHelper (x :: xs) (y :: ys) = (x :: y) :: transpHelper xs ys
-- matrix transp example
-- [1,2,3]     [1,4,7]
-- [4,5,6] =T> [2,5,8]
-- [7,8,9]     [3,6,9]
matrix_transp : Matrix 3 3 Nat
matrix_transp = transp [[1,2,3], [4,5,6], [7,8,9]]



-- matrix add operation
add : Num elem => Matrix r c elem -> Matrix r c elem -> Matrix r c elem
add x y = let z = zip x y in map (\(a, b) => vector_op (uncurry (+)) a b) z
-- matrix add example
-- [1,2,3]   [4,5,6]   [5,7,9]
-- [3,2,1] + [1,2,3] = [4,4,4]
-- [4,5,6]   [3,2,1]   [7,7,7]
matrix_add : Matrix 3 3 Nat
matrix_add = let
  m1 = [[1,2,3], [3,2,1], [4,5,6]]
  m2 = [[4,5,6], [1,2,3], [3,2,1]]
in
  add m1 m2



-- matrix multiplication operation
mul : Num elem => Matrix a b elem -> Matrix b c elem -> Matrix a c elem
mul [] y = []
mul (x :: xs) y = (single_vector x y) :: (mul xs y)
                  where
                    single_vector : Num elem => Vect b elem -> Matrix b c elem -> Vect c elem
                    single_vector v m = let tm = transp m
                                            mv = map (vector_op (uncurry (*)) v) tm
                                        in map sum mv
-- matrix mal example
-- [1,2,3]   [2,3]   [13,15]
-- [3,2,1] * [1,3] = [11,17]
-- [4,5,6]   [3,2]   [31,39]
matrix_mul : Matrix 3 2 Nat
matrix_mul = let
  m1 = [[1,2,3], [3,2,1], [4,5,6]]
  m2 = [[2,3], [1,3], [3,2]]
in
  mul m1 m2