@@ -5,17 +5,15 @@ import Data.ZZ
55
66%default total
77
8−
9−infixr 2 <.> -- Vector inner product
10−infixr 2 >< -- Vector outer product
11−infixr 2 <<>> -- Matrix commutator
12−infixr 2 >><< -- Matrix anticommutator
13−infixl 3 <\> -- row times a Matrix
14−infixr 4 </> -- Matrix times a column
15−infixr 5 <> -- Matrix multiplication
8+infixr 2 <.> -- vector inner product
9+infixr 2 >< -- vector outer product
10+infixr 2 <<>> -- matrix commutator
11+infixr 2 >><< -- matrix anticommutator
12+infixl 3 <\> -- row times a matrix
13+infixr 4 </> -- matrix times a column
14+infixr 5 <> -- matrix multiplication
1615infixr 7 \&\ -- vector tensor product
17−infixr 7 <&> -- Matrix tensor product
18−
16+infixr 7 <&> -- matrix tensor product
1917
2018-----------------------------------------------------------------------
2119-- Vectors as members of algebraic classes
@@ -41,24 +39,17 @@ instance RingWithUnity a => RingWithUnity (Vect n a) where
4139instance Field a => Field (Vect n a) where
4240 inverseM = map inverseM
4341
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
42+instance RingWithUnity a => Module a (Vect n a) where
43+ (<#>) r v = map (r <*>) v
4944
5045-----------------------------------------------------------------------
51−-- (Ring) Vector functions
46+-- (Ring) Vector functions
5247-----------------------------------------------------------------------
5348
5449||| Inner product of ring vectors
5550(<.>) : Ring a => Vect n a -> Vect n a -> a
5651(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)
5752
58−||| Scale a ring vector by the appropriate scalar
59−scale : Ring a => a -> Vect n a -> Vect n a
60−scale s v = map (<*> s) v
61−
6253||| Tensor multiply (⊗) ring vectors
6354(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
6455(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
@@ -73,18 +64,18 @@ basis i = replaceAt i unity $ neutral
7364
7465
7566-----------------------------------------------------------------------
76−-- Matrixrix functions
67+-- Matrix functions
7768-----------------------------------------------------------------------
7869
7970||| Matrix with n rows and m columns
8071Matrix : Nat -> Nat -> Type -> Type
8172Matrix n m a = Vect n (Vect m a)
8273
83−||| Gets the specified column of a Matrix. For rows use the vector function 'index'
74+||| Gets the specified column of a matrix. For rows use the vector function 'index'
8475getCol : Fin m -> Matrix n m a -> Vect n a
8576getCol fm q = map (index fm) q
8677
87−||| Deletes the specified column of a Matrix. For rows use the vector function 'deleteAt'
78+||| Deletes the specified column of a matrix. For rows use the vector function 'deleteAt'
8879deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
8980deleteCol f m = map (deleteAt f) m
9081
@@ -92,14 +83,6 @@ deleteCol f m = map (deleteAt f) m
9283indices : Fin n -> Fin m -> Matrix n m a -> a
9384indices f1 f2 m = index f2 (index f1 m)
9485
95−||| Ring scalar times a Matrix
96−RescaleBy.(*) : Ring a => a -> Matrix n m a -> Matrix n m a
97−RescaleBy.(*) s m = map (map (s <*>)) m
98−
99−||| Rescale Matrix by a ring scalar
100−RescaleMatrix.(*) : Ring a => Matrix n m a -> a -> Matrix n m a
101−RescaleMatrix.(*) m s = map (map (<*> s)) m
102−
10386||| Matrix times a column vector
10487(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
10588(</>) m v = map (v <.>) m
@@ -108,13 +91,13 @@ RescaleMatrix.(*) m s = map (map (<*> s)) m
10891(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
10992(<\>) r m = map (r <.>) $ transpose m
11093
111−||| Matrix Multiplication
94+||| Matrix multiplication
11295(<>) : Ring a => Matrix n k a ->
11396 Matrix k m a ->
11497 Matrix n m a
11598(<>) m1 m2 = map (<\> m2) m1
11699
117−||| Tensor multiply (⊗) for ring Matrixrices
100+||| Tensor multiply (⊗) for ring matrices
118101(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
119102(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
120103 stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
@@ -122,11 +105,11 @@ RescaleMatrix.(*) m s = map (map (<*> s)) m
122105 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
123106 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
124107
125−||| Cast a vector from a standard Vect to a proper n x 1 Matrix
108+||| Cast a vector from a standard Vect to a proper n x 1 matrix
126109col : Vect n a -> Matrix n 1 a
127110col v = map (\x => [x]) v
128111
129−||| Cast a row from a standard Vect to a proper 1 x n Matrix
112+||| Cast a row from a standard Vect to a proper 1 x n matrix
130113row : Vect n a -> Matrix 1 n a
131114row r = [r]
132115
@@ -139,15 +122,15 @@ allN : (n : Nat) -> Vect n (Fin n)
139122allN Z = Nil
140123allN (S n) = FZ :: (map FS $ allN n)
141124
142−||| Identity Matrix
125+||| Identity matrix
143126Id : RingWithUnity a => {d : Nat} -> Matrix d d a
144127Id {d} = map (\n => basis n) $ allN d
145128
146−||| Matrix Commutator
129+||| Matrix commutator
147130(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
148131(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)
149132
150−||| Matrix Anti-Commutator
133+||| Matrix anti-commutator
151134(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
152135(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
153136
@@ -157,7 +140,7 @@ Id {d} = map (\n => basis n) $ allN d
157140-----------------------------------------------------------------------
158141
159142
160−-- TODO: Prove properties of Matrix algebra for 'Verified' algebraic classes
143+-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
161144
162145-----------------------------------------------------------------------
163146-- Numberic data types as rings