@@ -0,0 +1,254 @@
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
15+infixr 7 \&\ -- vector tensor product
16+infixr 7 <&> -- matrix tensor product
18+-----------------------------------------------------------------------
19+-- Vectors as members of algebraic classes
20+-----------------------------------------------------------------------
22+instance Semigroup a => Semigroup (Vect n a) where
23+ (<+>) v w = zipWith (<+>) v w
25+instance Monoid a => Monoid (Vect n a) where
26+ neutral {n} = replicate n neutral
28+instance Group a => Group (Vect n a) where
29+ inverse = map inverse
31+instance AbelianGroup a => AbelianGroup (Vect n a) where {}
33+instance Ring a => Ring (Vect n a) where
34+ (<*>) v w = zipWith (<*>) v w
36+instance RingWithUnity a => RingWithUnity (Vect n a) where
37+ unity {n} = replicate n unity
39+instance Field a => Field (Vect n a) where
40+ inverseM = map inverseM
42+instance RingWithUnity a => Module a (Vect n a) where
43+ (<#>) r v = map (r <*>) v
45+instance RingWithUnity a => Module a (Vect n (Vect l a)) where
46+ (<#>) r m = map (r <#>) m
47+-- should be Module a b => Module a (Vect n b), but results in 'overlapping instance'
49+-----------------------------------------------------------------------
50+-- (Ring) Vector functions
51+-----------------------------------------------------------------------
53+||| Inner product of ring vectors
54+(<.>) : Ring a => Vect n a -> Vect n a -> a
55+(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)
57+||| Tensor multiply (⊗) ring vectors
58+(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
59+(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
60+ orep : (n : Nat) -> Vect m a -> Vect (n * m) a
61+ orep n v = concat $ replicate n v
62+ oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
63+ oextend n w = concat $ map (replicate n) w
65+||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed
66+basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a
67+basis i = replaceAt i unity $ neutral
69+-----------------------------------------------------------------------
71+-----------------------------------------------------------------------
73+||| Matrix with n rows and m columns
74+Matrix : Nat -> Nat -> Type -> Type
75+Matrix n m a = Vect n (Vect m a)
77+||| Gets the specified column of a matrix. For rows use the vector function 'index'
78+getCol : Fin m -> Matrix n m a -> Vect n a
79+getCol fm q = map (index fm) q
81+||| Deletes the specified column of a matrix. For rows use the vector function 'deleteAt'
82+deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
83+deleteCol f m = map (deleteAt f) m
85+||| Matrix element at specified row and column indices
86+indices : Fin n -> Fin m -> Matrix n m a -> a
87+indices f1 f2 m = index f2 (index f1 m)
89+||| Matrix times a column vector
90+(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
91+(</>) m v = map (v <.>) m
93+||| Matrix times a row vector
94+(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
95+(<\>) r m = map (r <.>) $ transpose m
97+||| Matrix multiplication
98+(<>) : Ring a => Matrix n k a ->
101+(<>) m1 m2 = map (<\> m2) m1
103+||| Tensor multiply (⊗) for ring matrices
104+(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
105+(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
106+ stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
107+ stepOne {h2} m1 m2 = concat $ map (replicate h2) m1
108+ stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
109+ stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
111+||| Cast a vector from a standard Vect to a proper n x 1 matrix
112+col : Vect n a -> Matrix n 1 a
113+col v = map (\x => [x]) v
115+||| Cast a row from a standard Vect to a proper 1 x n matrix
116+row : Vect n a -> Matrix 1 n a
119+||| Outer product between ring vectors
120+(><) : Ring a => Vect n a -> Vect m a -> Matrix n m a
121+(><) x y = (col x) <> (row y)
123+||| All finite numbers up to the given bound
124+allN : (n : Nat) -> Vect n (Fin n)
126+allN (S n) = FZ :: (map FS $ allN n)
129+Id : RingWithUnity a => {d : Nat} -> Matrix d d a
130+Id {d} = map (\n => basis n) $ allN d
132+||| Matrix commutator
133+(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
134+(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)
136+||| Matrix anti-commutator
137+(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
138+(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
140+-----------------------------------------------------------------------
141+-- Matrix Algebra Properties
142+-----------------------------------------------------------------------
144+-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
146+-----------------------------------------------------------------------
147+-- Numberic data types as rings
148+-----------------------------------------------------------------------
150+instance Semigroup Integer where
153+instance Monoid Integer where
156+instance Group Integer where
159+instance AbelianGroup Integer
161+instance Ring Integer where
164+instance RingWithUnity Integer where
168+instance Semigroup Int where
171+instance Monoid Int where
174+instance Group Int where
177+instance AbelianGroup Int
179+instance Ring Int where
182+instance RingWithUnity Int where
186+instance Semigroup Float where
189+instance Monoid Float where
192+instance Group Float where
195+instance AbelianGroup Float
197+instance Ring Float where
200+instance RingWithUnity Float where
203+instance Field Float where
207+instance Semigroup Nat where
210+instance Monoid Nat where
213+instance VerifiedSemigroup Nat where
214+ semigroupOpIsAssociative = plusAssociative
216+instance VerifiedMonoid Nat where
217+ monoidNeutralIsNeutralL = plusZeroRightNeutral
218+ monoidNeutralIsNeutralR = plusZeroLeftNeutral
221+instance Semigroup ZZ where
224+instance Monoid ZZ where
227+instance Group ZZ where
230+instance AbelianGroup ZZ
232+instance Ring ZZ where
235+instance RingWithUnity ZZ where
239+instance Semigroup a => Semigroup (Complex a) where
240+ (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
242+instance Monoid a => Monoid (Complex a) where
243+ neutral = (neutral :+ neutral)
245+instance Group a => Group (Complex a) where
246+ inverse (r :+ i) = (inverse r :+ inverse i)
248+instance Ring a => AbelianGroup (Complex a) where {}
250+instance Ring a => Ring (Complex a) where
251+ (<*>) (a :+ b) (c :+ d) = (a <*> c <-> b <*> d) :+ (a <*> d <+> b <*> c)
253+instance RingWithUnity a => RingWithUnity (Complex a) where
254+ unity = (unity :+ neutral)