@@ -1,150 +1,58 @@
1+||| Basic matrix operations with dimensionalities enforced
2+||| at the type level
13module Data.Matrix
24
3−import Control.Algebra
4−import Control.Algebra.VectorSpace
5−import public Control.Algebra.NumericInstances
6−
7−import Data.Complex
8−import Data.ZZ
9−import Data.Fin
10−import Data.Vect
5+import public Data.Vect
116
127%default total
138
14−infixr 2 <:> -- vector inner product
15−infixr 2 >< -- vector outer product
16−infixr 2 <<>> -- matrix commutator
17−infixr 2 >><< -- matrix anticommutator
18−infixl 3 <\> -- row times a matrix
19−infixr 4 </> -- matrix times a column
20−infixr 5 <> -- matrix multiplication
21−infixr 7 \&\ -- vector tensor product
22−infixr 7 <&> -- matrix tensor product
23−
24−-----------------------------------------------------------------------
25−-- Vectors as members of algebraic classes
26−-----------------------------------------------------------------------
27−
28−instance Semigroup a => Semigroup (Vect n a) where
29− (<+>) v w = zipWith (<+>) v w
30−
31−instance Monoid a => Monoid (Vect n a) where
32− neutral {n} = replicate n neutral
33−
34−instance Group a => Group (Vect n a) where
35− inverse = map inverse
36−
37−instance AbelianGroup a => AbelianGroup (Vect n a) where {}
38−
39−instance Ring a => Ring (Vect n a) where
40− (<.>) v w = zipWith (<.>) v w
41−
42−instance RingWithUnity a => RingWithUnity (Vect n a) where
43− unity {n} = replicate n unity
44−
45−--instance Field a => Field (Vect n a) where
46−
47−instance RingWithUnity a => Module a (Vect n a) where
48− (<#>) r v = map (r <.>) v
49−
50−instance RingWithUnity a => Module a (Vect n (Vect l a)) where
51− (<#>) r m = map (r <#>) m
52−-- should be Module a b => Module a (Vect n b), but results in 'overlapping instance'
53−
54−-----------------------------------------------------------------------
55−-- (Ring) Vector functions
56−-----------------------------------------------------------------------
57−
58−||| Inner product of ring vectors
59−(<:>) : Ring a => Vect n a -> Vect n a -> a
60−(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)
61−
62−||| Tensor multiply (⊗) ring vectors
63−(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
64−(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where
65− orep : (n : Nat) -> Vect m a -> Vect (n * m) a
66− orep n v = concat $ replicate n v
67− oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
68− oextend n w = concat $ map (replicate n) w
69−
70−||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed
71−basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a
72−basis i = replaceAt i unity $ neutral
73−
74−-----------------------------------------------------------------------
75−-- Matrix functions
76−-----------------------------------------------------------------------
77−
789||| Matrix with n rows and m columns
7910Matrix : Nat -> Nat -> Type -> Type
8011Matrix n m a = Vect n (Vect m a)
8112
82−||| Gets the specified column of a matrix. For rows use the vector function 'index'
13+||| Get the specified column of a matrix
8314getCol : Fin m -> Matrix n m a -> Vect n a
84−getCol fm q = map (index fm) q
15+getCol f = map (index f)
8516
86−||| Deletes the specified column of a matrix. For rows use the vector function 'deleteAt'
87−deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
88−deleteCol f m = map (deleteAt f) m
17+||| Get the specified row of a matrix
18+getRow : Fin n -> Matrix n m a -> Vect m a
19+getRow = index
8920
90−||| Matrix element at specified row and column indices
91−indices : Fin n -> Fin m -> Matrix n m a -> a
92−indices f1 f2 m = index f2 (index f1 m)
21+||| Delete the specified column of a matrix
22+deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
23+deleteCol f = map (deleteAt f)
9324
94−||| Matrix times a column vector
95−(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
96−(</>) m v = map (v <:>) m
25+||| Delete the specified row of a matrix
26+deleteRow : Fin (S n) -> Matrix (S n) m a -> Matrix n m a
27+deleteRow = deleteAt
9728
98−||| Matrix times a row vector
99−(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
100−(<\>) r m = map (r <:>) $ transpose m
29+insertRow : Fin (S n) -> Vect m a -> Matrix n m a -> Matrix (S n) m a
30+insertRow = insertAt
10131
102−||| Matrix multiplication
103−(<>) : Ring a => Matrix n k a ->
104− Matrix k m a ->
105− Matrix n m a
106−(<>) m1 m2 = map (<\> m2) m1
32+insertCol : Fin (S m) -> Vect n a -> Matrix n m a -> Matrix n (S m) a
33+insertCol f = zipWith (insertAt f)
10734
108−||| Tensor multiply (⊗) for ring matrices
109−(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
110−(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
111− stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
112− stepOne {h2} m1 m2 = concat $ map (replicate h2) m1
113− stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
114− stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
35+||| Matrix element at specified row and column indices
36+indices : Fin n -> Fin m -> Matrix n m a -> a
37+indices f1 f2 = index f2 . index f1
11538
11639||| Cast a vector from a standard Vect to a proper n x 1 matrix
11740col : Vect n a -> Matrix n 1 a
118−col v = map (\x => [x]) v
41+col = map (\x => [x])
11942
12043||| Cast a row from a standard Vect to a proper 1 x n matrix
12144row : Vect n a -> Matrix 1 n a
12245row r = [r]
12346
124−||| Outer product between ring vectors
125−(><) : Ring a => Vect n a -> Vect m a -> Matrix n m a
126−(><) x y = (col x) <> (row y)
127−
128−||| All finite numbers up to the given bound
129−allN : (n : Nat) -> Vect n (Fin n)
130−allN Z = Nil
131−allN (S n) = FZ :: (map FS $ allN n)
132−
133−||| Identity matrix
134−Id : RingWithUnity a => {d : Nat} -> Matrix d d a
135−Id {d} = map (\n => basis n) $ allN d
136−
137−||| Matrix commutator
138−(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
139−(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)
140−
141−||| Matrix anti-commutator
142−(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
143−(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
144−
145−-----------------------------------------------------------------------
146−-- Matrix Algebra Properties
147−-----------------------------------------------------------------------
47+||| Matrix formed by deleting specified row and col
48+subMatrix : Fin (S n) -> Fin (S m) -> Matrix (S n) (S m) a -> Matrix n m a
49+subMatrix r c = deleteRow r . deleteCol c
14850
149−-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
51+||| Flatten a matrix of matrices
52+concatMatrix : Matrix n m (Matrix x y a) -> Matrix (n * x) (m * y) a
53+concatMatrix = Vect.concat . map (map Vect.concat) . map transpose
15054
55+||| All finite numbers of the specified level
56+fins : (n : Nat) -> Vect n (Fin n)
57+fins Z = Nil
58+fins (S n) = FZ :: (map FS $ fins n)