Ticket #2748: Det.hs

File Det.hs, 6.5 KB (added by sedillard, 5 years ago)
Line 
1
2{-# LANGUAGE TypeOperators #-}
3{-# LANGUAGE TypeSynonymInstances #-}
4{-# LANGUAGE EmptyDataDecls #-}
5{-# LANGUAGE FlexibleContexts #-}
6{-# LANGUAGE FlexibleInstances #-}
7{-# LANGUAGE FunctionalDependencies #-}
8{-# LANGUAGE MultiParamTypeClasses #-}
9{-# LANGUAGE NoMonomorphismRestriction #-}
10{-# LANGUAGE ScopedTypeVariables #-}
11{-# LANGUAGE UndecidableInstances #-}
12{-# LANGUAGE OverlappingInstances #-}
13
14import Prelude hiding (sum,head,tail,map,zipWith,foldr,foldl)
15
16
17data a :. b = !a :. !b
18  deriving (Eq,Ord,Read,Show)
19
20infixr :.
21
22class Det' a m | m -> a where
23  det' :: m -> a
24
25--base case for 2x2
26instance Num a => Det' a ((a:.a:.()):.(a:.a:.()):.()) where
27  det' ( (a:.b:.()) :. (c:.d:.()) :. () ) = a*d-b*c
28
29
30
31------------------------
32-- Overlapping instance (works in 6.8 & 6.10)
33{-
34instance
35    (Num a
36    ,Fold a v
37    ,Num v
38    ,Head m v
39    ,Vec n a v
40    ,Map m__ a vm v
41    ,Transpose vmt vm
42    ,DropConsec v vv
43    ,Map v vv m_ vmt
44    ,Tail m m_
45    ,Alternating n a v
46    ,Det' a m__
47    )
48    => Det' a m
49  where
50    det' m =
51      sum ((alternating undefined 1) * (head m) *
52           (map det' (transpose(map(dropConsec)(tail m)))))
53-}
54
55---------------------
56-- Non-overlapping instance (works in 6.8)
57
58instance
59    (Num a
60    ,Num (a:.a:.a:.v)
61    ,Fold a (a:.a:.a:.v)
62    ,Alternating (Succ (Succ (Succ n))) a (a:.a:.a:.v)
63    ,DropConsec (a:.a:.a:.v) vv
64    ,Map (a:.a:.a:.v) vv ((a:.a:.a:.v):.(a:.a:.a:.v):.m) vmt
65    ,Transpose vmt vm
66    ,Map ((a:.a:.v):.(a:.a:.v):.m_) a vm (a:.a:.a:.v)
67    ,Det' a ((a:.a:.v):.(a:.a:.v):.m_)
68    ,Vec (Succ (Succ (Succ n))) a (a:.a:.a:.v)
69    ,Vec (Succ (Succ (Succ n))) (a:.a:.a:.v) ((a:.a:.a:.v):.(a:.a:.a:.v):.(a:.a:.a:.v):.m)
70    )
71     => 
72    Det' a ((a:.a:.a:.v):.(a:.a:.a:.v):.(a:.a:.a:.v):.m)
73  where
74    det' (mh:.mt) =
75      sum ((alternating undefined 1) * mh *
76          (map det' (transpose (map dropConsec mt :: vmt))))
77
78
79
80
81
82
83
84
85
86
87
88
89det :: forall n a r m. (Vec n a r, Vec n r m, Det' a m) => m -> a
90det = det'
91
92
93
94-- Vector type. Matrices are vectors of vectors.
95
96
97data N0
98data Succ a
99
100class Pred x y | x -> y, y -> x
101instance Pred (Succ N0) N0
102instance Pred (Succ n) p => Pred (Succ (Succ n)) (Succ p)
103
104type N1  = Succ N0
105type N2  = Succ N1
106type N3  = Succ N2
107type N4  = Succ N3
108type N5  = Succ N4
109
110
111
112class Vec n a v | n a -> v, v -> n a where
113  mkVec :: n -> a -> v
114
115instance Vec N1 a ( a :. () ) where
116  mkVec _ a = a :. ()
117
118instance Vec (Succ n) a (a':.v) => Vec (Succ (Succ n)) a (a:.a':.v) where
119  mkVec _ a = a :. (mkVec undefined a)
120
121
122
123 
124class Head v a | v -> a  where 
125  head :: v -> a
126instance Head (a :. as) a where 
127  head (a :. _) = a
128
129
130class Tail v v_ | v -> v_ where 
131  tail :: v -> v_
132instance Tail (a :. as) as where 
133  tail (_ :. as) = as
134
135
136
137
138class Map a b u v | u -> a, v -> b, b u -> v, a v -> u where
139  map :: (a -> b) -> u -> v
140instance Map a b (a :. ()) (b :. ()) where
141  map f (x :. ()) = (f x) :. ()
142instance Map a b (a':.u) (b':.v) => Map a b (a:.a':.u) (b:.b':.v) where
143  map f (x:.v) = (f x):.(map f v)
144
145
146
147
148class ZipWith a b c u v w | u->a, v->b, w->c, u v c -> w where
149  zipWith :: (a -> b -> c) -> u -> v -> w
150instance ZipWith a b c (a:.()) (b:.()) (c:.()) where
151  zipWith f (x:._) (y:._) = f x y :.()
152instance ZipWith a b c (a:.()) (b:.b:.bs) (c:.()) where
153  zipWith f (x:._) (y:._) = f x y :.()
154instance ZipWith a b c (a:.a:.as) (b:.()) (c:.()) where
155  zipWith f (x:._) (y:._) = f x y :.()
156instance 
157  ZipWith a b c (a':.u) (b':.v) (c':.w) 
158  => ZipWith a b c (a:.a':.u) (b:.b':.v) (c:.c':.w) 
159    where
160      zipWith f (x:.u) (y:.v) = f x y :. zipWith f u v
161
162
163
164class Fold a v | v -> a where
165  fold  :: (a -> a -> a) -> v -> a
166instance Fold a (a:.()) where
167  fold  f   (a:._) = a
168instance Fold a (a':.u) => Fold a (a:.a':.u) where
169  fold  f   (a:.v) = (f a) (fold f v)
170
171sum ::  (Fold a v, Num a) => v -> a
172sum x = fold (+) x
173
174
175
176
177
178
179class Transpose a b | a -> b, b -> a where 
180  transpose :: a -> b
181
182instance Transpose () () where
183  transpose = id
184
185instance 
186    (Vec (Succ n) s (s:.ra)  --(s:ra) is an n-vector of s'es (row of a)
187    ,Vec (Succ m) (s:.ra) ((s:.ra):.a)  --a is an m-vector of ra's
188    ,Vec (Succ m) s (s:.rb)  --rb is an m-vector of s'es (row of b)
189    ,Vec (Succ n) (s:.rb) ((s:.rb):.b)  --b is an n-vector of rb's
190    ,Transpose' ((s:.ra):.a) ((s:.rb):.b)
191    )
192    => Transpose ((s:.ra):.a) ((s:.rb):.b)
193  where
194    transpose = transpose'
195
196
197
198
199
200
201class Transpose' a b | a->b
202  where transpose' :: a -> b
203
204instance Transpose' () () where 
205  transpose' = id
206
207instance 
208    (Transpose' vs vs') => Transpose' ( () :. vs ) vs'
209  where
210    transpose' (():.vs) = transpose' vs
211
212instance Transpose' ((x:.()):.()) ((x:.()):.()) where
213  transpose' = id
214
215instance 
216    (Head xss_h xss_hh
217    ,Map xss_h xss_hh (xss_h:.xss_t) xs'
218    ,Tail xss_h xss_ht
219    ,Map xss_h xss_ht (xss_h:.xss_t) xss_
220    ,Transpose' (xs :. xss_) xss'
221    )
222    => Transpose' ((x:.xs):.(xss_h:.xss_t)) ((x:.xs'):.xss') 
223  where
224    transpose' ((x:.xs):.xss) =
225      (x :. (map head xss)) :. (transpose' (xs :. (map tail xss) :: (xs:.xss_)))
226
227
228
229
230
231
232class DropConsec v vv | v -> vv where
233  dropConsec :: v -> vv
234
235instance 
236  (Vec n a v
237  ,Pred n n_
238  ,Vec n_ a v_
239  ,Vec n v_ vv
240  ,DropConsec' () v vv
241  ) => DropConsec v vv
242  where
243    dropConsec v = dropConsec' () v
244
245class DropConsec' p v vv  where
246  dropConsec' :: p -> v -> vv
247   
248instance DropConsec' p (a:.()) (p:.()) where
249  dropConsec' p (a:.()) = (p:.())
250
251instance 
252    (Append p (a:.v) x
253    ,Append p (a:.()) y
254    ,DropConsec' y (a:.v) z
255    ) 
256    => DropConsec' p (a:.a:.v) (x:.z)
257  where
258    dropConsec' p (a:.v) = 
259      (append p v) :. (dropConsec' (append p (a:.())) v)
260
261
262
263
264
265class Alternating n a v | v -> n a where
266  alternating :: n -> a -> v
267
268instance Alternating N1 a (a:.()) where
269  alternating _ a = a:.()
270
271instance (Num a, Alternating n a (a:.v)) => Alternating (Succ n) a (a:.a:.v) where
272  alternating _ a = a:.(alternating (undefined::n) (negate a))
273
274
275
276
277
278
279class Append v1 v2 v3 | v1 v2 -> v3, v1 v3 -> v2 where 
280  append :: v1 -> v2 -> v3
281
282instance Append () v v where
283  append _ = id
284
285instance Append (a:.()) v (a:.v) where
286  append (a:.()) v = a:.v
287
288instance (Append (a':.v1) v2 v3) => Append (a:.a':.v1) v2 (a:.v3) where
289  append (a:.u) v  =  a:.(append u v)
290
291
292
293
294
295instance
296    (Eq (a:.u)
297    ,Show (a:.u)
298    ,Num a
299    ,Map a a (a:.u) (a:.u) 
300    ,ZipWith a a a (a:.u) (a:.u) (a:.u)
301    ,Vec (Succ l) a (a:.u)
302    )
303    => Num (a:.u) 
304  where
305    (+) u v = zipWith (+) u v
306    (-) u v = zipWith (-) u v
307    (*) u v = zipWith (*) u v
308    abs u = map abs u
309    signum u = map signum u
310    fromInteger i = mkVec undefined (fromInteger i)