Ticket #2748: Det_TF.hs

File Det_TF.hs, 6.0 KB (added by sedillard, 6 years ago)
Line 
1{-# LANGUAGE EmptyDataDecls #-}
2{-# LANGUAGE FlexibleContexts #-}
3{-# LANGUAGE FlexibleInstances #-}
4{-# LANGUAGE MultiParamTypeClasses #-}
5{-# LANGUAGE ScopedTypeVariables #-}
6{-# LANGUAGE TypeFamilies #-}
7{-# LANGUAGE TypeOperators #-}
8{-# LANGUAGE TypeSynonymInstances #-}
9{-# LANGUAGE UndecidableInstances #-}
10
11import Prelude hiding (map,zipWith,foldl,foldr,head,tail,sum)
12
13data (:.) a b = !a :. !b
14  deriving (Eq,Ord,Read,Show)
15infixr 9 :.
16
17
18
19class Det m where
20  det :: m -> Elem (Elem m)
21
22instance Det ((a:.()):.()) where
23  det ((a:._):._) = a
24
25instance 
26  ( (x:.x:.xs) ~ r                     -- a row of the matrix, an n-vector
27  , ((x:.x:.xs):.(x:.x:.xs):.xss) ~ m  -- an n*n matrix, n >= 2
28  , ((x:.xs):.(x:.xs):.xss_) ~ m_      -- an n*(n-1) matrix
29  , MapF (x:.xs) m                     -- drop the first column of m ...
30  , Map (x:.xs) m ~ m_                 -- ... to get m_
31  , DropConsecF' () m_                 -- an n-vector of (n-1)*(n-1) matrices
32  , Det ((x:.xs):.xss_)                -- determinant of (n-1)*(n-1) matrix
33  , MapF x (DropConsec' () m_)         -- dets of all n of the (n-1)*(n-1) matrices...
34  , Map x (DropConsec' () m_) ~ r      -- ... the result is same type as a row
35  , MapF x m                           -- grab the first column using "map head" ...
36  , Map x m ~ r                        -- ... the result is same type as a row
37  , NegateOdds r                       -- flip sign of odd elements of first column
38  , FoldF r                            -- finally add evertyhing up
39  , Num r
40  , Num x
41  ) => Det ((x:.x:.xs):.(x:.x:.xs):.xss) 
42  where
43  det m =
44    sum $ (negateOdds $ map head m) * map det (dropConsec' () (map tail m))
45
46
47
48
49data N0
50data Succ n
51type N1 = Succ N0
52type N2 = Succ N1
53type N3 = Succ N2
54
55class VecF n e where
56  type Vec n e
57
58instance VecF N0 e where
59  type Vec N0 e = ()
60
61instance VecF n e => VecF (Succ n) e where
62  type Vec (Succ n) e = e :. Vec n e
63
64
65
66class ElemF v where
67  type Elem v
68
69instance ElemF (a:.v) where
70  type Elem (a:.v) = a
71
72
73class HeadF v where
74  type Head v
75  head :: v -> Head v
76
77instance HeadF (a:.v) where
78  type Head (a:.v) = a
79  head (a:.v) = a
80
81
82class TailF v where
83  type Tail v
84  tail :: v -> Tail v
85
86instance TailF (a:.v) where
87  type Tail (a:.v) = v
88  tail (a:.v) = v
89
90
91
92class MapF r v where
93  type Map r v
94  map :: (Elem v -> r) -> v -> Map r v
95
96instance MapF b (a:.()) where
97  type Map b (a:.()) = (b:.())
98  map f (a:.()) = f a :. ()
99 
100instance MapF b (a:.v) => MapF b (a:.(a:.v)) where
101  type Map b (a:.(a:.v)) = b :. Map b (a:.v) 
102  map f (a:.v) = f a :. map f v
103
104
105
106class ZipWithF r v1 v2 where
107  type ZipWith r v1 v2
108  zipWith :: (Elem v1 -> Elem v2 -> r) -> v1 -> v2 -> ZipWith r v1 v2
109
110instance ZipWithF c (a:.()) (b:.()) where
111  type ZipWith c (a:.()) (b:.()) = (c:.())
112  zipWith f (a:.()) (b:.()) = f a b :. ()
113
114instance ZipWithF c (a:.va) (b:.vb) => ZipWithF c (a:.a:.va) (b:.b:.vb) where
115  type ZipWith c (a:.a:.va) (b:.b:.vb) = c :. ZipWith c (a:.va) (b:.vb)
116  zipWith f (a:.va) (b:.vb) = f a b :. zipWith f va vb
117
118
119
120
121class FoldF v where
122  fold  :: (Elem v -> Elem v -> Elem v) -> v -> Elem v
123  foldr :: (Elem v -> a -> a) -> a -> v -> a
124  foldl :: (a -> Elem v -> a) -> a -> v -> a
125
126instance FoldF (a:.()) where
127  fold _ (a:.()) = a
128  foldr f z (a:.()) = f a z
129  foldl f z (a:.()) = f z a
130
131instance FoldF (a:.v) => FoldF (a:.a:.v) where
132  fold f (a:.v) = a `f` fold f v
133  foldr f z (a:.v) = a `f` foldr f z v
134  foldl f z (a:.v) = foldl f (f z a) v
135
136sum :: (Num (Elem v), FoldF v) => v -> Elem v
137sum = fold (+)
138
139
140
141class DropConsecF' p v where
142  type DropConsec' p v
143  dropConsec' :: p -> v -> DropConsec' p v
144
145instance DropConsecF' p (a:.()) where
146  type DropConsec' p (a:.()) = p:.()
147  dropConsec' p (a:.()) = (p:.())
148
149
150instance 
151    ( AppendF p (a:.v)
152    , AppendF p (a:.())
153    , DropConsecF' (Append p (a:.())) (a:.v)
154    ) => DropConsecF' p (a:.a:.v) 
155  where
156    type DropConsec' p (a:.a:.v) = Append p (a:.v) :. DropConsec' (Append p (a:.())) (a:.v)
157    dropConsec' p (a:.v) = append p v :. dropConsec' (append p (a:.())) v
158
159
160
161
162class AppendF v1 v2 where
163  type Append v1 v2
164  append :: v1 -> v2 -> Append v1 v2
165
166instance AppendF () v where
167  type Append () v = v
168  append _ = id
169
170instance AppendF (a:.()) v where
171  type Append (a:.()) v = a :. v
172  append (a:.()) v = a:.v
173
174instance AppendF (a:.v1) v2  => AppendF (a:.a:.v1) v2 where
175  type Append (a:.a:.v1) v2 = a :. Append (a:.v1) v2
176  append (a:.u) v = a :. append u v
177
178
179
180instance
181    (Eq (a:.u)
182    ,Show (a:.u)
183    ,Num a
184    ,MapF a (a:.u) 
185    ,Map a (a:.u) ~ (a:.u)
186    ,ZipWithF a (a:.u) (a:.u) 
187    ,ZipWith a (a:.u) (a:.u) ~ (a:.u)
188    )
189    => Num (a:.u) 
190  where
191    (+) u v = zipWith (+) u v
192    (-) u v = zipWith (-) u v
193    (*) u v = zipWith (*) u v
194    abs u = map abs u
195    signum u = map signum u
196    fromInteger i = error "not implemented" 
197
198
199
200class NegateOdds v where
201  negateOdds :: v -> v
202
203class NegateEvens v where
204  negateEvens :: v -> v
205
206instance NegateOdds  () where negateOdds  () = ()
207instance NegateEvens () where negateEvens () = ()
208
209instance (Num a, NegateOdds v) => NegateEvens (a:.v) where
210  negateEvens (a:.v) = negate a :. negateOdds v
211
212instance (Num a, NegateEvens v) => NegateOdds (a:.v) where
213  negateOdds (a:.v) = a :. negateEvens v
214
215 
216 
217 
218class TransposeF m where 
219  type Transpose m
220  transpose :: m -> Transpose m
221
222instance TransposeF () where 
223  type Transpose () = ()
224  transpose = id
225
226instance TransposeF m => TransposeF ( () :. m ) where
227  type Transpose ( () :. m ) = Transpose m
228  transpose ( () :. m ) = transpose m
229 
230
231instance TransposeF ((x:.()):.()) where
232  type Transpose ((x:.()):.()) = (x:.()):.()
233  transpose = id
234
235instance 
236  ( HeadF xss_h
237  , TailF xss_h
238  , MapF (Head xss_h) (xss_h:.xss_t)
239  , MapF (Tail xss_h) (xss_h:.xss_t)
240  , TransposeF ( xs :. Map (Tail xss_h) (xss_h:.xss_t) ) 
241  ) => TransposeF ((x:.xs):.(xss_h:.xss_t) )
242  where
243    type Transpose ((x:.xs):.(xss_h:.xss_t)) = 
244      (x:. Map (Head xss_h) (xss_h:.xss_t )) :. 
245        Transpose ( xs :. Map (Tail xss_h) (xss_h:.xss_t) ) 
246    transpose ((x:.xs):.xss) = 
247      (x :. map head xss) :. 
248        transpose (xs :. map tail xss)