Matrix.idr

import Data.Vect

Matrix : Nat -> Nat -> Type -> Type
Matrix x y t = Vect x (Vect y t)

createEmpties : Vect n (Vect 0 elem)
createEmpties = replicate _ []

transposeMatrix : Matrix rows columns elem ->
                  Matrix columns rows elem
transposeMatrix [] = createEmpties
transposeMatrix (row :: rows) =
  let
    transposedRows = transposeMatrix rows
  in
    zipWith (::) row transposedRows



multiplyMatrix :  Num numType =>
                  Matrix firstRows n numType ->
                  Matrix n secondColumns numType ->
                  Matrix firstRows secondColumns numType
multiplyMatrix [] [] = [] -- for empty element we do nothing
multiplyMatrix [] (secondRow :: secondRows) = []
multiplyMatrix (firstRow :: firstRows) [] = ?onlyFirstMatrix
multiplyMatrix (firstRow :: firstRows) secondMatrix =
  let
    transposedSecondMatrix = transposeMatrix secondMatrix
    (transposedSecondRow :: transposedSecondRows) = transposedSecondMatrix
  in
    multiplyHelper transposedSecondRow firstRow firstRows transposedSecondRows transposedSecondMatrix secondMatrix