diff --git a/chapter3/Matrix.idr b/chapter3/Matrix.idr new file mode 100644 index 0000000..3cb1782 --- /dev/null +++ b/chapter3/Matrix.idr @@ -0,0 +1,30 @@ +module Matrix + +import Data.Vect + +addMatrix : Num numType => + Vect rows (Vect cols numType) -> + Vect rows (Vect cols numType) -> + Vect rows (Vect cols numType) +addMatrix = zipWith (zipWith (+)) + +multMatrix : Num numType => + Vect n (Vect m numType) -> Vect m (Vect p numType) -> + Vect n (Vect p numType) +-- 😔 + +createEmpties : Vect n (Vect 0 elem) +createEmpties = replicate _ [] + +createEmpties2 : Vect n (Vect 0 elem) +createEmpties2 {n = Z} = [] +createEmpties2 {n = (S k)} = [] :: createEmpties2 + + +transHelper : (x : Vect n elem) -> (xsTrans : Vect n (Vect len elem)) -> Vect n (Vect (S len) elem) +transHelper = zipWith (\x, y => x :: y) + +transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem) +transposeMat [] = createEmpties +transposeMat (x :: xs) = let xsTrans = transposeMat xs in + transHelper x xsTrans diff --git a/chapter3/Vectors.idr b/chapter3/Vectors.idr index 2290fc8..148f1bf 100644 --- a/chapter3/Vectors.idr +++ b/chapter3/Vectors.idr @@ -52,3 +52,12 @@ my_map f (x :: xs) = (f x) :: my_map f xs my_vect_map : (a -> b) -> Vect n a -> Vect n b my_vect_map _ [] = [] my_vect_map f (x :: xs) = (f x) :: my_vect_map f xs + + +lengthLong : Vect n elem -> Nat +lengthLong [] = 0 +lengthLong (x :: xs) = S (lengthLong xs) + + +lengthLong2 : Vect n elem -> Nat +lengthLong2 {n} xs = n