git.iko.soy/Idris-dev
on ec2a48a help sign in
Idris-dev/libs/base/Data/Matrix.idr
256 lines 7.2 kB history raw
1module Data.Matrix
3import Data.Complex
4import Data.ZZ
5import Data.Fin
6import Data.Vect
8%default total
10infixr 2 <.> -- vector inner product
11infixr 2 >< -- vector outer product
12infixr 2 <<>> -- matrix commutator
13infixr 2 >><< -- matrix anticommutator
14infixl 3 <\> -- row times a matrix
15infixr 4 </> -- matrix times a column
16infixr 5 <> -- matrix multiplication
17infixr 7 \&\ -- vector tensor product
18infixr 7 <&> -- matrix tensor product
20-----------------------------------------------------------------------
21-- Vectors as members of algebraic classes
22-----------------------------------------------------------------------
24instance Semigroup a => Semigroup (Vect n a) where
25 (<+>) v w = zipWith (<+>) v w
27instance Monoid a => Monoid (Vect n a) where
28 neutral {n} = replicate n neutral
30instance Group a => Group (Vect n a) where
31 inverse = map inverse
33instance AbelianGroup a => AbelianGroup (Vect n a) where {}
35instance Ring a => Ring (Vect n a) where
36 (<*>) v w = zipWith (<*>) v w
38instance RingWithUnity a => RingWithUnity (Vect n a) where
39 unity {n} = replicate n unity
41instance Field a => Field (Vect n a) where
42 inverseM = map inverseM
44instance RingWithUnity a => Module a (Vect n a) where
45 (<#>) r v = map (r <*>) v
47instance RingWithUnity a => Module a (Vect n (Vect l a)) where
48 (<#>) r m = map (r <#>) m
49-- should be Module a b => Module a (Vect n b), but results in 'overlapping instance'
51-----------------------------------------------------------------------
52-- (Ring) Vector functions
53-----------------------------------------------------------------------
55||| Inner product of ring vectors
56(<.>) : Ring a => Vect n a -> Vect n a -> a
57(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)
59||| Tensor multiply (⊗) ring vectors
60(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
61(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
62 orep : (n : Nat) -> Vect m a -> Vect (n * m) a
63 orep n v = concat $ replicate n v
64 oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
65 oextend n w = concat $ map (replicate n) w
67||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed
68basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a
69basis i = replaceAt i unity $ neutral
71-----------------------------------------------------------------------
72-- Matrix functions
73-----------------------------------------------------------------------
75||| Matrix with n rows and m columns
76Matrix : Nat -> Nat -> Type -> Type
77Matrix n m a = Vect n (Vect m a)
79||| Gets the specified column of a matrix. For rows use the vector function 'index'
80getCol : Fin m -> Matrix n m a -> Vect n a
81getCol fm q = map (index fm) q
83||| Deletes the specified column of a matrix. For rows use the vector function 'deleteAt'
84deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
85deleteCol f m = map (deleteAt f) m
87||| Matrix element at specified row and column indices
88indices : Fin n -> Fin m -> Matrix n m a -> a
89indices f1 f2 m = index f2 (index f1 m)
91||| Matrix times a column vector
92(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
93(</>) m v = map (v <.>) m
95||| Matrix times a row vector
96(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
97(<\>) r m = map (r <.>) $ transpose m
99||| Matrix multiplication
100(<>) : Ring a => Matrix n k a ->
101 Matrix k m a ->
102 Matrix n m a
103(<>) m1 m2 = map (<\> m2) m1
105||| Tensor multiply (⊗) for ring matrices
106(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
107(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
108 stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
109 stepOne {h2} m1 m2 = concat $ map (replicate h2) m1
110 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
111 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
113||| Cast a vector from a standard Vect to a proper n x 1 matrix
114col : Vect n a -> Matrix n 1 a
115col v = map (\x => [x]) v
117||| Cast a row from a standard Vect to a proper 1 x n matrix
118row : Vect n a -> Matrix 1 n a
119row r = [r]
121||| Outer product between ring vectors
122(><) : Ring a => Vect n a -> Vect m a -> Matrix n m a
123(><) x y = (col x) <> (row y)
125||| All finite numbers up to the given bound
126allN : (n : Nat) -> Vect n (Fin n)
127allN Z = Nil
128allN (S n) = FZ :: (map FS $ allN n)
130||| Identity matrix
131Id : RingWithUnity a => {d : Nat} -> Matrix d d a
132Id {d} = map (\n => basis n) $ allN d
134||| Matrix commutator
135(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
136(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)
138||| Matrix anti-commutator
139(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
140(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
142-----------------------------------------------------------------------
143-- Matrix Algebra Properties
144-----------------------------------------------------------------------
146-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
148-----------------------------------------------------------------------
149-- Numberic data types as rings
150-----------------------------------------------------------------------
152instance Semigroup Integer where
153 (<+>) = (+)
155instance Monoid Integer where
156 neutral = 0
158instance Group Integer where
159 inverse = (* -1)
161instance AbelianGroup Integer
163instance Ring Integer where
164 (<*>) = (*)
166instance RingWithUnity Integer where
167 unity = 1
170instance Semigroup Int where
171 (<+>) = (+)
173instance Monoid Int where
174 neutral = 0
176instance Group Int where
177 inverse = (* -1)
179instance AbelianGroup Int
181instance Ring Int where
182 (<*>) = (*)
184instance RingWithUnity Int where
185 unity = 1
188instance Semigroup Float where
189 (<+>) = (+)
191instance Monoid Float where
192 neutral = 0
194instance Group Float where
195 inverse = (* -1)
197instance AbelianGroup Float
199instance Ring Float where
200 (<*>) = (*)
202instance RingWithUnity Float where
203 unity = 1
205instance Field Float where
206 inverseM f = 1 / f
209instance Semigroup Nat where
210 (<+>) = (+)
212instance Monoid Nat where
213 neutral = 0
215instance VerifiedSemigroup Nat where
216 semigroupOpIsAssociative = plusAssociative
218instance VerifiedMonoid Nat where
219 monoidNeutralIsNeutralL = plusZeroRightNeutral
220 monoidNeutralIsNeutralR = plusZeroLeftNeutral
223instance Semigroup ZZ where
224 (<+>) = (+)
226instance Monoid ZZ where
227 neutral = 0
229instance Group ZZ where
230 inverse = (* -1)
232instance AbelianGroup ZZ
234instance Ring ZZ where
235 (<*>) = (*)
237instance RingWithUnity ZZ where
238 unity = 1
241instance Semigroup a => Semigroup (Complex a) where
242 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
244instance Monoid a => Monoid (Complex a) where
245 neutral = (neutral :+ neutral)
247instance Group a => Group (Complex a) where
248 inverse (r :+ i) = (inverse r :+ inverse i)
250instance Ring a => AbelianGroup (Complex a) where {}
252instance Ring a => Ring (Complex a) where
253 (<*>) (a :+ b) (c :+ d) = (a <*> c <-> b <*> d) :+ (a <*> d <+> b <*> c)
255instance RingWithUnity a => RingWithUnity (Complex a) where
256 unity = (unity :+ neutral)