idris-matrix

A simple Idris library for manipulating matrices 🧙

Diffstat

2 files changed, 143 insertions, 0 deletions

diff --git a/Data/Matrix.ibc b/Data/Matrix.ibc
Binary files differ.

diff --git a/Data/Matrix.idr b/Data/Matrix.idr
@@ -0,0 +1,143 @@
+module Data.Matrix
+
+import Data.Vect
+
+||| A matrix with fixed dimentions.
+export
+data Matrix : (n : Nat) -> (m : Nat) -> Type -> Type where
+  MkMatrix : Vect (S n) (Vect (S m) t) -> Matrix (S n) (S m) t 
+
+%name Matrix as, bs, cs, ds, xs, ys
+
+||| A type alias for a square matrix.
+export
+Square : Nat -> Type -> Type
+Square n = Matrix n n
+
+-- ============================ Conversions ===================================
+
+implementation Cast (Vect (S n) (Vect (S m) t)) (Matrix (S n) (S m) t) where
+  cast = MkMatrix
+
+implementation Cast (Matrix (S n) (S m) t) (Vect (S n) (Vect (S m) t)) where
+  cast (MkMatrix as) = as
+
+||| Generates a matrix from nested vectors.
+export total
+fromVect : Vect (S n) (Vect (S m) t) -> Matrix (S n) (S m) t
+fromVect = cast
+
+||| Converts a matrix to nested vectors.
+export total
+toVect : Matrix (S n) (S m) t -> Vect (S n) (Vect (S m) t)
+toVect = cast
+
+implementation Cast (Matrix (S n) (S m) t) (List (List t)) where
+  cast = toList . map toList . toVect
+
+-- =========================== Initialization =================================
+
+||| Generates a matrix based on it's coordinates.
+export  total
+fromCoords : (f : Fin (S n) -> Fin (S m) -> t) -> Matrix (S n) (S m) t
+fromCoords f = MkMatrix (map (\i => map (f i) range) range)
+
+||| Returns a matrix whose coordinate-values are constant.
+export total
+replicate : t -> Matrix (S n) (S m) t
+replicate x = fromVect (replicate _ (replicate _ x))
+
+-- =========================== Manipulations ==================================
+
+||| Combines two matrix with the same dimentions pairwise with some function.
+export total
+zipWith : (f : a -> b -> c) -> Matrix (S n) (S m) a 
+                            -> Matrix (S n) (S m) b
+                            -> Matrix (S n) (S m) c
+zipWith f (MkMatrix as) (MkMatrix bs) = MkMatrix (zipWith (zipWith f) as bs)
+
+||| Combines two matrices with the same dimentions into a matrix of tuples
+export total
+zip : Matrix (S n) (S m) a -> Matrix (S n) (S m) b -> Matrix (S n) (S m) (a, b)
+zip = zipWith (\a => \b => (a, b))
+
+-- ============================== Indexing ====================================
+
+||| Returns the value of a matrix coordinate
+index : Fin (S n) -> Fin (S m) -> Matrix (S n) (S m) t -> t
+index i j (MkMatrix as) = index j (index i as)
+
+-- ======================== Basic Implementations =============================
+
+implementation Eq t => Eq (Matrix (S n) (S m) t) where
+  (MkMatrix as) == (MkMatrix bs) = as == bs
+  
+implementation Show t => Show (Matrix (S n) (S m) t) where
+  show as = unlines (map unwords (map (map show) as'))
+  where
+    as' : List (List t)
+    as' = cast as
+
+implementation Functor (Matrix (S n) (S m)) where
+  map f (MkMatrix as) = MkMatrix (map (map f) as)
+
+implementation Applicative (Matrix (S n) (S m)) where
+  pure = replicate
+
+  (<*>) = zipWith apply
+
+implementation Semigroup t => Semigroup (Matrix (S n) (S m) t) where
+  (<+>) = zipWith (<+>)
+
+implementation Monoid t => Monoid (Matrix (S n) (S m) t) where
+  neutral = pure neutral
+
+-- =========================== Linear Algebra =================================
+
+||| Returns the identity matrix.
+export
+ident : Num t => Matrix (S n) (S n) t
+ident = fromCoords f
+  where
+    f i j = if i == j then 1 else 0
+
+||| Transposes the matrix.
+export total
+transpose : Matrix (S n) (S m) t -> Matrix (S m) (S n) t
+transpose (MkMatrix as) = MkMatrix (transpose as)
+
+||| Adds two numeric matrices.
+export total
+(+) : Num t => Matrix (S n) (S m) t -> Matrix (S n) (S m) t 
+                                    -> Matrix (S n) (S m) t
+(+) = zipWith (+)
+
+||| Multiplies two numeric matrices.
+export total
+(*) : Num t => Matrix (S n) (S m) t -> Matrix (S m) (S p) t 
+                                    -> Matrix (S n) (S p) t
+(*) {n} {m} {p} (MkMatrix as) (MkMatrix bs) = fromCoords f
+  where 
+    sum : Num t => Vect (S q) t -> t
+    sum = with Vect foldl1 (+)
+    bs' : Vect (S p) (Vect (S m) t)
+    bs' = transpose bs
+    f : Num t => Fin (S n) -> Fin (S p) -> t
+    f i j = sum (zipWith (*) (with Vect index i as) (with Vect index j bs'))
+
+infixr 8 <>
+
+||| Multiplies a matrix by a scalar.
+export total
+(<>) : Num t => t -> Matrix (S n) (S m) t -> Matrix (S n) (S m) t
+x <> as = (x *) <$> as
+
+export total
+negate : Neg t => Matrix (S n) (S m) t -> Matrix (S n) (S m) t
+negate as = negate <$> as
+
+export total
+(-) : Neg t => Matrix (S n) (S m) t -> Matrix (S n) (S m) t 
+                                    -> Matrix (S n) (S m) t
+(-) = zipWith (-)
+