@@ -5,22 +5,50 @@ import Data.ZZ
55
66%default total
77
8−infixl 1 \+\ -- Vector plus (mnemonic: V begins with '\'
9−infixl 1 /+/ -- Matrix plus M begins with '/')
10−infixl 1 \-\ -- Vector minus
11−infixl 1 /-/ -- Matrix minus
8+
129infixr 2 <.> -- Vector inner product
1310infixr 2 >< -- Vector outer product
1411infixr 2 <<>> -- Matrix commutator
1512infixr 2 >><< -- Matrix anticommutator
16−infixl 3 <\> -- row times a matrix
17−infixr 4 </> -- matrix times a column
18−infixr 5 <> -- matrix multiplication
13+infixl 3 <\> -- row times a Matrix
14+infixr 4 </> -- Matrix times a column
15+infixr 5 <> -- Matrix multiplication
1916infixr 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
2149
2250-----------------------------------------------------------------------
23−-- Vector Stuff
51+-- (Ring) Vector functions
2452-----------------------------------------------------------------------
2553
2654||| Inner product of ring vectors
@@ -31,14 +59,6 @@ infixr 7 <&> -- matrix tensor product
3159scale : Ring a => a -> Vect n a -> Vect n a
3260scale s v = map (<*> s) v
3361
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−
4262||| Tensor multiply (⊗) ring vectors
4363(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
4464(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
@@ -47,32 +67,24 @@ scale s v = map (<*> s) v
4767 oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
4868 oextend n w = concat $ map (replicate n) w
4969
50−||| Zero vector
51−zero : Monoid a => {d : Nat} -> Vect d a
52−zero {d} = replicate d neutral
53−
5470||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed
5571basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a
56−basis i = replaceAt i unity $ zero
57−
58−||| All-unit vector
59−flat : RingWithUnity a => {d : Nat} -> Vect d a
60−flat {d} = replicate d unity
72+basis i = replaceAt i unity $ neutral
6173
6274
6375-----------------------------------------------------------------------
64−-- Matrix Stuff
76+-- Matrixrix functions
6577-----------------------------------------------------------------------
6678
6779||| Matrix with n rows and m columns
6880Matrix : Nat -> Nat -> Type -> Type
6981Matrix n m a = Vect n (Vect m a)
7082
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'
7284getCol : Fin m -> Matrix n m a -> Vect n a
7385getCol fm q = map (index fm) q
7486
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'
7688deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
7789deleteCol f m = map (deleteAt f) m
7890
@@ -80,19 +92,11 @@ deleteCol f m = map (deleteAt f) m
8092indices : Fin n -> Fin m -> Matrix n m a -> a
8193indices f1 f2 m = index f2 (index f1 m)
8294
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
9296RescaleBy.(*) : Ring a => a -> Matrix n m a -> Matrix n m a
9397RescaleBy.(*) s m = map (map (s <*>)) m
9498
95−||| Rescale matrix by a ring scalar
99+||| Rescale Matrix by a ring scalar
96100RescaleMatrix.(*) : Ring a => Matrix n m a -> a -> Matrix n m a
97101RescaleMatrix.(*) m s = map (map (<*> s)) m
98102
@@ -110,7 +114,7 @@ RescaleMatrix.(*) m s = map (map (<*> s)) m
110114 Matrix n m a
111115(<>) m1 m2 = map (<\> m2) m1
112116
113−||| Tensor multiply (⊗) for ring matrices
117+||| Tensor multiply (⊗) for ring Matrixrices
114118(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
115119(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
116120 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
118122 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
119123 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
120124
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
122126col : Vect n a -> Matrix n 1 a
123127col v = map (\x => [x]) v
124128
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
126130row : Vect n a -> Matrix 1 n a
127131row r = [r]
128132
@@ -135,55 +139,25 @@ allN : (n : Nat) -> Vect n (Fin n)
135139allN Z = Nil
136140allN (S n) = FZ :: (map FS $ allN n)
137141
138−||| Identity matrix
142+||| Identity Matrix
139143Id : RingWithUnity a => {d : Nat} -> Matrix d d a
140144Id {d} = map (\n => basis n) $ allN d
141145
142−||| Zero matrix
143−Zero : Monoid a => {d : Nat} -> Matrix d d a
144−Zero {d} = replicate d zero
145−
146146||| Matrix Commutator
147147(<<>>) : 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)
149149
150150||| Matrix Anti-Commutator
151151(>><<) : 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)
153153
154154
155155-----------------------------------------------------------------------
156156-- Matrix Algebra Properties
157157-----------------------------------------------------------------------
158158
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−
185159
186−-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
160+-- TODO: Prove properties of Matrix algebra for 'Verified' algebraic classes
187161
188162-----------------------------------------------------------------------
189163-- Numberic data types as rings
@@ -281,16 +255,16 @@ instance RingWithUnity ZZ where
281255instance Semigroup a => Semigroup (Complex a) where
282256 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
283257
284−instance (Num a, Monoid a) => Monoid (Complex a) where
285− neutral = (0 :+ 0)
258+instance Monoid a => Monoid (Complex a) where
259+ neutral = (neutral :+ neutral)
286260
287−instance (Num a, Neg a, Group a) => Group (Complex a) where
288− inverse = (\(r :+ i) => -r :+ -i)
261+instance Group a => Group (Complex a) where
262+ inverse (r :+ i) = (inverse r :+ inverse i)
289263
290−instance Group (Complex a) => AbelianGroup (Complex a) where {}
264+instance Ring a => AbelianGroup (Complex a) where {}
291265
292−instance (Num a, AbelianGroup (Complex a)) => Ring (Complex a) where
293− (<*>) (a :+ b) (c :+ d) = (a*c - b*d) :+ (a*d + b*c)
266+instance Ring a => Ring (Complex a) where
267+ (<*>) (a :+ b) (c :+ d) = (a <*> c <-> b <*> d) :+ (a <*> d <+> b <*> c)
294268
295−instance (Num a, Ring (Complex a)) => RingWithUnity (Complex a) where
296− unity = (1 :+ 0)
269+instance RingWithUnity a => RingWithUnity (Complex a) where
270+ unity = (unity :+ neutral)