# 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
```