git.iko.soy/Idris-dev
on master help sign in
Update Matrix.idr
5e8c7faCliff Harvey
libs/base/Data/Matrix.idr+59−85
compare with master
unifiedsplit
@@ -5,22 +5,50 @@ import Data.ZZ
5
5
6%default total
6%default total
7
7
8−infixl 1 \+\ -- Vector plus (mnemonic: V begins with '\'
8+
9−infixl 1 /+/ -- Matrix plus M begins with '/')
10−infixl 1 \-\ -- Vector minus
11−infixl 1 /-/ -- Matrix minus
12infixr 2 <.> -- Vector inner product
9infixr 2 <.> -- Vector inner product
13infixr 2 >< -- Vector outer product
10infixr 2 >< -- Vector outer product
14infixr 2 <<>> -- Matrix commutator
11infixr 2 <<>> -- Matrix commutator
15infixr 2 >><< -- Matrix anticommutator
12infixr 2 >><< -- Matrix anticommutator
16−infixl 3 <\> -- row times a matrix
13+infixl 3 <\> -- row times a Matrix
17−infixr 4 </> -- matrix times a column
14+infixr 4 </> -- Matrix times a column
18−infixr 5 <> -- matrix multiplication
15+infixr 5 <> -- Matrix multiplication
19infixr 7 \&\ -- vector tensor product
16infixr 7 \&\ -- vector tensor product
20−infixr 7 <&> -- matrix tensor product
17+infixr 7 <&> -- Matrix tensor product
18+
19+
20+-----------------------------------------------------------------------
21+-- Vectors as members of algebraic classes
22+-----------------------------------------------------------------------
23+
24+instance Semigroup a => Semigroup (Vect n a) where
25+ (<+>) v w = zipWith (<+>) v w
26+
27+instance Monoid a => Monoid (Vect n a) where
28+ neutral {n} = replicate n neutral
29+
30+instance Group a => Group (Vect n a) where
31+ inverse = map inverse
32+
33+instance AbelianGroup a => AbelianGroup (Vect n a) where {}
34+
35+instance Ring a => Ring (Vect n a) where
36+ (<*>) v w = zipWith (<*>) v w
37+
38+instance RingWithUnity a => RingWithUnity (Vect n a) where
39+ unity {n} = replicate n unity
40+
41+instance Field a => Field (Vect n a) where
42+ inverseM = map inverseM
43+
44+instance (Field a, AbelianGroup a) => VectorSpace a (Vect n a) where
45+ (<#>) s v = map (s <*>) v
46+
47+instance (Field a, AbelianGroup a) => VectorSpace a (Vect n (Vect n a)) where
48+ (<#>) s m = map (s <#>) m
21
49
22-----------------------------------------------------------------------
50-----------------------------------------------------------------------
23−-- Vector Stuff
51+-- (Ring) Vector functions
24-----------------------------------------------------------------------
52-----------------------------------------------------------------------
25
53
26||| Inner product of ring vectors
54||| Inner product of ring vectors
@@ -31,14 +59,6 @@ infixr 7 <&> -- matrix tensor product
31scale : Ring a => a -> Vect n a -> Vect n a
59scale : Ring a => a -> Vect n a -> Vect n a
32scale s v = map (<*> s) v
60scale s v = map (<*> s) v
33
61
34−||| Vector addition
35−(\+\) : Ring a => Vect n a -> Vect n a -> Vect n a
36−(\+\) v w = zipWith (<+>) v w
37−
38−||| Vector subtraction
39−(\-\) : Ring a => Vect n a -> Vect n a -> Vect n a
40−(\-\) v w = zipWith (<->) v w
41−
42||| Tensor multiply (⊗) ring vectors
62||| Tensor multiply (⊗) ring vectors
43(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
63(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
44(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
64(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
@@ -47,32 +67,24 @@ scale s v = map (<*> s) v
47 oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
67 oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
48 oextend n w = concat $ map (replicate n) w
68 oextend n w = concat $ map (replicate n) w
49
69
50−||| Zero vector
51−zero : Monoid a => {d : Nat} -> Vect d a
52−zero {d} = replicate d neutral
53−
54||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed
70||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed
55basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a
71basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a
56−basis i = replaceAt i unity $ zero
72+basis i = replaceAt i unity $ neutral
57−
58−||| All-unit vector
59−flat : RingWithUnity a => {d : Nat} -> Vect d a
60−flat {d} = replicate d unity
61
73
62
74
63-----------------------------------------------------------------------
75-----------------------------------------------------------------------
64−-- Matrix Stuff
76+-- Matrixrix functions
65-----------------------------------------------------------------------
77-----------------------------------------------------------------------
66
78
67||| Matrix with n rows and m columns
79||| Matrix with n rows and m columns
68Matrix : Nat -> Nat -> Type -> Type
80Matrix : Nat -> Nat -> Type -> Type
69Matrix n m a = Vect n (Vect m a)
81Matrix n m a = Vect n (Vect m a)
70
82
71−||| Gets the specified column of a matrix. For rows use the vector function 'index'
83+||| Gets the specified column of a Matrix. For rows use the vector function 'index'
72getCol : Fin m -> Matrix n m a -> Vect n a
84getCol : Fin m -> Matrix n m a -> Vect n a
73getCol fm q = map (index fm) q
85getCol fm q = map (index fm) q
74
86
75−||| Deletes the specified column of a matrix. For rows use the vector function 'deleteAt'
87+||| Deletes the specified column of a Matrix. For rows use the vector function 'deleteAt'
76deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
88deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
77deleteCol f m = map (deleteAt f) m
89deleteCol f m = map (deleteAt f) m
78
90
@@ -80,19 +92,11 @@ deleteCol f m = map (deleteAt f) m
80indices : Fin n -> Fin m -> Matrix n m a -> a
92indices : Fin n -> Fin m -> Matrix n m a -> a
81indices f1 f2 m = index f2 (index f1 m)
93indices f1 f2 m = index f2 (index f1 m)
82
94
83−||| Matrix addition
84−(/+/) : Ring a => Matrix n m a -> Matrix n m a -> Matrix n m a
85−(/+/) = zipWith (\+\)
86−
87−||| Matrix subtraction
88−(/-/) : Ring a => Matrix n m a -> Matrix n m a -> Matrix n m a
89−(/-/) = zipWith (\-\)
90−
91−||| Ring scalar times a matrix
95+||| Ring scalar times a Matrix
92RescaleBy.(*) : Ring a => a -> Matrix n m a -> Matrix n m a
96RescaleBy.(*) : Ring a => a -> Matrix n m a -> Matrix n m a
93RescaleBy.(*) s m = map (map (s <*>)) m
97RescaleBy.(*) s m = map (map (s <*>)) m
94
98
95−||| Rescale matrix by a ring scalar
99+||| Rescale Matrix by a ring scalar
96RescaleMatrix.(*) : Ring a => Matrix n m a -> a -> Matrix n m a
100RescaleMatrix.(*) : Ring a => Matrix n m a -> a -> Matrix n m a
97RescaleMatrix.(*) m s = map (map (<*> s)) m
101RescaleMatrix.(*) m s = map (map (<*> s)) m
98
102
@@ -110,7 +114,7 @@ RescaleMatrix.(*) m s = map (map (<*> s)) m
110 Matrix n m a
114 Matrix n m a
111(<>) m1 m2 = map (<\> m2) m1
115(<>) m1 m2 = map (<\> m2) m1
112
116
113−||| Tensor multiply (⊗) for ring matrices
117+||| Tensor multiply (⊗) for ring Matrixrices
114(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
118(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
115(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
119(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
116 stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
120 stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
@@ -118,11 +122,11 @@ RescaleMatrix.(*) m s = map (map (<*> s)) m
118 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
122 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
119 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
123 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
120
124
121−||| Cast a vector from a standard Vect to a proper n x 1 matrix
125+||| Cast a vector from a standard Vect to a proper n x 1 Matrix
122col : Vect n a -> Matrix n 1 a
126col : Vect n a -> Matrix n 1 a
123col v = map (\x => [x]) v
127col v = map (\x => [x]) v
124
128
125−||| Cast a row from a standard Vect to a proper 1 x n matrix
129+||| Cast a row from a standard Vect to a proper 1 x n Matrix
126row : Vect n a -> Matrix 1 n a
130row : Vect n a -> Matrix 1 n a
127row r = [r]
131row r = [r]
128
132
@@ -135,55 +139,25 @@ allN : (n : Nat) -> Vect n (Fin n)
135allN Z = Nil
139allN Z = Nil
136allN (S n) = FZ :: (map FS $ allN n)
140allN (S n) = FZ :: (map FS $ allN n)
137
141
138−||| Identity matrix
142+||| Identity Matrix
139Id : RingWithUnity a => {d : Nat} -> Matrix d d a
143Id : RingWithUnity a => {d : Nat} -> Matrix d d a
140Id {d} = map (\n => basis n) $ allN d
144Id {d} = map (\n => basis n) $ allN d
141
145
142−||| Zero matrix
143−Zero : Monoid a => {d : Nat} -> Matrix d d a
144−Zero {d} = replicate d zero
145−
146||| Matrix Commutator
146||| Matrix Commutator
147(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
147(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
148−(<<>>) m1 m2 = (m1 <> m2) /-/ (m2 <> m1)
148+(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)
149
149
150||| Matrix Anti-Commutator
150||| Matrix Anti-Commutator
151(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
151(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
152−(>><<) m1 m2 = (m1 <> m2) /+/ (m2 <> m1)
152+(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
153
153
154
154
155-----------------------------------------------------------------------
155-----------------------------------------------------------------------
156-- Matrix Algebra Properties
156-- Matrix Algebra Properties
157-----------------------------------------------------------------------
157-----------------------------------------------------------------------
158
158
159−instance Semigroup a => Semigroup (Vect n a) where
160− (<+>) v w = zipWith (<+>) v w
161−
162−instance Monoid a => Monoid (Vect n a) where
163− neutral {n} = replicate n neutral
164−
165−instance Group a => Group (Vect n a) where
166− inverse = map inverse
167−
168−instance AbelianGroup a => AbelianGroup (Vect n a) where {}
169−
170−instance Ring a => Ring (Vect n a) where
171− (<*>) v w = zipWith (<*>) v w
172−
173−instance RingWithUnity a => RingWithUnity (Vect n a) where
174− unity {n} = replicate n unity
175−
176−instance Field a => Field (Vect n a) where
177− inverseM = map inverseM
178−
179−instance (Field a, AbelianGroup a) => VectorSpace a (Vect n a) where
180− (<#>) s v = map (s <*>) v
181−
182−instance (Field a, AbelianGroup a) => VectorSpace a (Vect n (Vect n a)) where
183− (<#>) s m = map (s <#>) m
184−
185
159
186−-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
160+-- TODO: Prove properties of Matrix algebra for 'Verified' algebraic classes
187
161
188-----------------------------------------------------------------------
162-----------------------------------------------------------------------
189-- Numberic data types as rings
163-- Numberic data types as rings
@@ -281,16 +255,16 @@ instance RingWithUnity ZZ where
281instance Semigroup a => Semigroup (Complex a) where
255instance Semigroup a => Semigroup (Complex a) where
282 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
256 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
283
257
284−instance (Num a, Monoid a) => Monoid (Complex a) where
258+instance Monoid a => Monoid (Complex a) where
285− neutral = (0 :+ 0)
259+ neutral = (neutral :+ neutral)
286
260
287−instance (Num a, Neg a, Group a) => Group (Complex a) where
261+instance Group a => Group (Complex a) where
288− inverse = (\(r :+ i) => -r :+ -i)
262+ inverse (r :+ i) = (inverse r :+ inverse i)
289
263
290−instance Group (Complex a) => AbelianGroup (Complex a) where {}
264+instance Ring a => AbelianGroup (Complex a) where {}
291
265
292−instance (Num a, AbelianGroup (Complex a)) => Ring (Complex a) where
266+instance Ring a => Ring (Complex a) where
293− (<*>) (a :+ b) (c :+ d) = (a*c - b*d) :+ (a*d + b*c)
267+ (<*>) (a :+ b) (c :+ d) = (a <*> c <-> b <*> d) :+ (a <*> d <+> b <*> c)
294
268
295−instance (Num a, Ring (Complex a)) => RingWithUnity (Complex a) where
269+instance RingWithUnity a => RingWithUnity (Complex a) where
296− unity = (1 :+ 0)
270+ unity = (unity :+ neutral)