git.iko.soy/laop
on master help sign in
Fixed Eq instance
2a059dfArmando Santos
app/Main.hs+30−22
compare with master
unifiedsplit
@@ -11,6 +11,7 @@ import Dist
11import GHC.TypeLits
11import GHC.TypeLits
12import Data.Coerce
12import Data.Coerce
13import System.CPUTime
13import System.CPUTime
14+import System.Random
14
15
15-- Monty Hall Problem
16-- Monty Hall Problem
16data Outcome = Win | Lose
17data Outcome = Win | Lose
@@ -29,7 +30,7 @@ secondChoice = fromF switch
29-- Dice sum
30-- Dice sum
30
31
31sumSS :: Natural 6 -> Natural 6 -> Natural 12
32sumSS :: Natural 6 -> Natural 6 -> Natural 12
32−sumSS = coerceNat (+)
33+sumSS = coerceNat (+)
33
34
34mulSS :: Natural 6 -> Natural 6 -> Natural 36
35mulSS :: Natural 6 -> Natural 6 -> Natural 36
35mulSS = coerceNat (*)
36mulSS = coerceNat (*)
@@ -58,29 +59,36 @@ grass_wet = row [0,1] `comp` kp1 @Double @2 @4
58
59
59rainning = row [0,1] `comp` kp2 @Double @2 @2 `comp` kp2 @Double @2 @4
60rainning = row [0,1] `comp` kp2 @Double @2 @2 `comp` kp2 @Double @2 @4
60
61
61−-- Random Matrix multiplication
62+-- Random Matrix
62
63
63−-- a :: Matrix Double 1000 1000
64+randomRow :: IO [Double]
64−-- a = identity
65+randomRow = mapM (const (randomRIO (0, 1000))) [0..2399]
65
66
67+randomList :: IO [[Double]]
68+randomList = mapM (const randomRow) [0..2399]
69+
66−-- b :: Matrix Double 1000 1000
70+randomMatrix :: IO (Matrix Double 2400 2400)
67−-- b = identity
71+randomMatrix = fromLists <$> randomList
68
72
69main :: IO ()
73main :: IO ()
70main = do
74main = do
71− putStrLn "Monty Hall Problem solution:"
75+ -- putStrLn "Monty Hall Problem solution:"
72− prettyPrint (p1 @Double @1 `comp` secondChoice `comp` firstChoice)
76+ -- prettyPrint (p1 @Double @1 `comp` secondChoice `comp` firstChoice)
73− putStrLn "\n Sum of dices probability:"
77+ -- putStrLn "\n Sum of dices probability:"
74− prettyPrint (sumSSM `comp` khatri die die)
78+ -- prettyPrint (sumSSM `comp` khatri die die)
75− putStrLn "\n Checking that the last result is indeed a distribution: "
79+ -- putStrLn "\n Checking that the last result is indeed a distribution: "
76− prettyPrint (bang `comp` sumSSM `comp` khatri die die)
80+ -- prettyPrint (bang `comp` sumSSM `comp` khatri die die)
77− putStrLn "\n Probability of grass being wet:"
81+ -- putStrLn "\n Probability of grass being wet:"
78− prettyPrint (grass_wet `comp` state)
82+ -- prettyPrint (grass_wet `comp` state)
79− putStrLn "\n Probability of rain:"
83+ -- putStrLn "\n Probability of rain:"
80− prettyPrint (rainning `comp` state)
84+ -- prettyPrint (rainning `comp` state)
81−
85+
86+ -- Random Matrix multiplication
87+ !a <- randomMatrix
88+ !b <- randomMatrix
82− -- start <- getCPUTime
89+ !start <- getCPUTime
83− -- let !r = a `comp` b
90+ let !r = b `comp` a
84− -- end <- getCPUTime
91+ !end <- getCPUTime
92+ print "Time in milisseconds:"
85− -- print (end - start)
93+ print (fromInteger (end - start) / 1000000000)
86−
94+ print (r == a)
src/Matrix/Type.hs+14−11
@@ -137,7 +137,6 @@ import Data.List
137import Data.Proxy
137import Data.Proxy
138import Data.Void
138import Data.Void
139import GHC.TypeLits
139import GHC.TypeLits
140−import Data.Type.Bool
141import Data.Type.Equality
140import Data.Type.Equality
142import GHC.Generics
141import GHC.Generics
143
142
@@ -168,13 +167,15 @@ type family Count (d :: Type) where
168 Count d = Count (Rep d R)
167 Count d = Count (Rep d R)
169
168
170-- | Type family that computes of a given type dimension from a given natural
169-- | Type family that computes of a given type dimension from a given natural
170+-- Thanks to Li-Yao Xia this type family is super fast.
171type family FromNat (n :: Nat) where
171type family FromNat (n :: Nat) where
172 FromNat 0 = Void
172 FromNat 0 = Void
173 FromNat 1 = ()
173 FromNat 1 = ()
174− FromNat n = If (Mod n 2 == 0)
174+ FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
175− (Either (FromNat (Div n 2)) (FromNat (Div n 2)))
175+
176− (Either () (FromNat (n - 1)))
176+type family FromNat' (b :: Bool) (m :: Type) :: Type where
177− -- Either () (FromNat (n - 1))
177+ FromNat' 'True m = Either m m
178+ FromNat' 'False m = Either () (Either m m)
178
179
179-- | Type family that normalizes the representation of a given data
180-- | Type family that normalizes the representation of a given data
180-- structure
181-- structure
@@ -182,10 +183,12 @@ type family Normalize (d :: Type) where
182 Normalize d = FromNat (Count d)
183 Normalize d = FromNat (Count d)
183
184
184instance Eq e => Eq (Matrix e cols rows) where
185instance Eq e => Eq (Matrix e cols rows) where
185− Empty == Empty = True
186+ Empty == Empty = True
186− (One a) == (One b) = a == b
187+ (One a) == (One b) = a == b
187− (Junc a b) == (Junc c d) = a == c && b == d
188+ (Junc a b) == (Junc c d) = a == c && b == d
188− (Split a b) == (Split c d) = a == c && b == d
189+ (Split a b) == (Split c d) = a == c && b == d
190+ x@(Split a b) == y@(Junc c d) = x == abideJS y
191+ x@(Junc a b) == y@(Split c d) = abideJS x == y
189
192
190instance Num e => Num (Matrix e cols rows) where
193instance Num e => Num (Matrix e cols rows) where
191
194
@@ -268,7 +271,7 @@ instance {-# OVERLAPPING #-} FromLists e () () where
268 fromLists [[e]] = One e
271 fromLists [[e]] = One e
269 fromLists _ = error "Wrong dimensions"
272 fromLists _ = error "Wrong dimensions"
270
273
271−instance (FromLists e cols ()) => FromLists e (Either () cols) () where
274+instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
272 fromLists [h : t] = Junc (One h) (fromLists [t])
275 fromLists [h : t] = Junc (One h) (fromLists [t])
273 fromLists _ = error "Wrong dimensions"
276 fromLists _ = error "Wrong dimensions"
274
277
@@ -278,7 +281,7 @@ instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), KnownNat (Cou
278 in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])
281 in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])
279 fromLists _ = error "Wrong dimensions"
282 fromLists _ = error "Wrong dimensions"
280
283
281−instance (FromLists e () rows) => FromLists e () (Either () rows) where
284+instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
282 fromLists ([h] : t) = Split (One h) (fromLists t)
285 fromLists ([h] : t) = Split (One h) (fromLists t)
283 fromLists _ = error "Wrong dimensions"
286 fromLists _ = error "Wrong dimensions"
284
287