idris-matrix

A simple Idris library for manipulating matrices 🧙
Matrix.idr (4450B)

  1 module Data.Matrix
  2 
  3 import Data.Vect
  4 
  5 ||| A matrix with fixed dimentions.
  6 export
  7 data Matrix : (n : Nat) -> (m : Nat) -> Type -> Type where
  8   MkMatrix : Vect (S n) (Vect (S m) t) -> Matrix (S n) (S m) t 
  9 
 10 %name Matrix as, bs, cs, ds, xs, ys
 11 
 12 ||| A type alias for a square matrix.
 13 export
 14 Square : Nat -> Type -> Type
 15 Square n = Matrix n n
 16 
 17 -- ============================ Conversions ===================================
 18 
 19 implementation Cast (Vect (S n) (Vect (S m) t)) (Matrix (S n) (S m) t) where
 20   cast = MkMatrix
 21 
 22 implementation Cast (Matrix (S n) (S m) t) (Vect (S n) (Vect (S m) t)) where
 23   cast (MkMatrix as) = as
 24 
 25 ||| Generates a matrix from nested vectors.
 26 export total
 27 fromVect : Vect (S n) (Vect (S m) t) -> Matrix (S n) (S m) t
 28 fromVect = cast
 29 
 30 ||| Converts a matrix to nested vectors.
 31 export total
 32 toVect : Matrix (S n) (S m) t -> Vect (S n) (Vect (S m) t)
 33 toVect = cast
 34 
 35 implementation Cast (Matrix (S n) (S m) t) (List (List t)) where
 36   cast = toList . map toList . toVect
 37 
 38 -- =========================== Initialization =================================
 39 
 40 ||| Generates a matrix based on it's coordinates.
 41 export  total
 42 fromCoords : (f : Fin (S n) -> Fin (S m) -> t) -> Matrix (S n) (S m) t
 43 fromCoords f = MkMatrix (map (\i => map (f i) range) range)
 44 
 45 ||| Returns a matrix whose coordinate-values are constant.
 46 export total
 47 replicate : t -> Matrix (S n) (S m) t
 48 replicate x = fromVect (replicate _ (replicate _ x))
 49 
 50 -- =========================== Manipulations ==================================
 51 
 52 ||| Combines two matrix with the same dimentions pairwise with some function.
 53 export total
 54 zipWith : (f : a -> b -> c) -> Matrix (S n) (S m) a 
 55                             -> Matrix (S n) (S m) b
 56                             -> Matrix (S n) (S m) c
 57 zipWith f (MkMatrix as) (MkMatrix bs) = MkMatrix (zipWith (zipWith f) as bs)
 58 
 59 ||| Combines two matrices with the same dimentions into a matrix of tuples
 60 export total
 61 zip : Matrix (S n) (S m) a -> Matrix (S n) (S m) b -> Matrix (S n) (S m) (a, b)
 62 zip = zipWith (\a => \b => (a, b))
 63 
 64 -- ============================== Indexing ====================================
 65 
 66 ||| Returns the value of a matrix coordinate
 67 index : Fin (S n) -> Fin (S m) -> Matrix (S n) (S m) t -> t
 68 index i j (MkMatrix as) = index j (index i as)
 69 
 70 -- ======================== Basic Implementations =============================
 71 
 72 implementation Eq t => Eq (Matrix (S n) (S m) t) where
 73   (MkMatrix as) == (MkMatrix bs) = as == bs
 74   
 75 implementation Show t => Show (Matrix (S n) (S m) t) where
 76   show as = unlines (map unwords (map (map show) as'))
 77   where
 78     as' : List (List t)
 79     as' = cast as
 80 
 81 implementation Functor (Matrix (S n) (S m)) where
 82   map f (MkMatrix as) = MkMatrix (map (map f) as)
 83 
 84 implementation Applicative (Matrix (S n) (S m)) where
 85   pure = replicate
 86 
 87   (<*>) = zipWith apply
 88 
 89 implementation Semigroup t => Semigroup (Matrix (S n) (S m) t) where
 90   (<+>) = zipWith (<+>)
 91 
 92 implementation Monoid t => Monoid (Matrix (S n) (S m) t) where
 93   neutral = pure neutral
 94 
 95 -- =========================== Linear Algebra =================================
 96 
 97 ||| Returns the identity matrix.
 98 export
 99 ident : Num t => Matrix (S n) (S n) t
100 ident = fromCoords f
101   where
102     f i j = if i == j then 1 else 0
103 
104 ||| Transposes the matrix.
105 export total
106 transpose : Matrix (S n) (S m) t -> Matrix (S m) (S n) t
107 transpose (MkMatrix as) = MkMatrix (transpose as)
108 
109 ||| Adds two numeric matrices.
110 export total
111 (+) : Num t => Matrix (S n) (S m) t -> Matrix (S n) (S m) t 
112                                     -> Matrix (S n) (S m) t
113 (+) = zipWith (+)
114 
115 ||| Multiplies two numeric matrices.
116 export total
117 (*) : Num t => Matrix (S n) (S m) t -> Matrix (S m) (S p) t 
118                                     -> Matrix (S n) (S p) t
119 (*) {n} {m} {p} (MkMatrix as) (MkMatrix bs) = fromCoords f
120   where 
121     sum : Num t => Vect (S q) t -> t
122     sum = with Vect foldl1 (+)
123     bs' : Vect (S p) (Vect (S m) t)
124     bs' = transpose bs
125     f : Num t => Fin (S n) -> Fin (S p) -> t
126     f i j = sum (zipWith (*) (with Vect index i as) (with Vect index j bs'))
127 
128 infixr 8 .
129 
130 ||| Multiplies a matrix by a scalar.
131 export total
132 (.) : Num t => t -> Matrix (S n) (S m) t -> Matrix (S n) (S m) t
133 x . as = (x *) <$> as
134 
135 export total
136 negate : Neg t => Matrix (S n) (S m) t -> Matrix (S n) (S m) t
137 negate = negate <$>
138 
139 export total
140 (-) : Neg t => Matrix (S n) (S m) t -> Matrix (S n) (S m) t 
141                                     -> Matrix (S n) (S m) t
142 (-) = zipWith (-)
143