Matrix Multiplication, Idris Style

MatrixMultiplication.idr

module Main

import Data.Vect

Matrix: Nat -> Nat -> Type -> Type
Matrix n m a = Vect n (Vect m a)

total createEmpties : Matrix n Z a
createEmpties {n = Z} = []
createEmpties {n = (S k)} = [] :: createEmpties

total vectDotProduct : Num a => Vect n a -> Vect n a -> a
vectDotProduct [] [] = 0
vectDotProduct (x :: xs) (y :: ys) = x * y + vectDotProduct xs ys

total matrixVectMult : Num a => Matrix n m a -> Vect m a -> Vect n a
matrixVectMult [] [] = []
matrixVectMult [] (x :: xs) = []
matrixVectMult (row :: rows) as = (vectDotProduct row as) :: matrixVectMult rows as

total transposeMatrix : Matrix n m a -> Matrix m n a
transposeMatrix [] = createEmpties
transposeMatrix (row :: rows) = let xsTransposed = transposeMatrix rows in
                                zipWith (::) row xsTransposed

total matrixMult: Num a => Matrix n m a -> Matrix m p a -> Matrix n p a
matrixMult[] [] = []
matrixMult[] (row :: rows) = []
matrixMult(row :: rows) ys = let transposedYs = transposeMatrix ys in
                         matrixVectMult transposedYs row :: matrixMult rows ys