git.iko.soy/laop
on master help sign in
Removed Empty constructor
c115295Armando Santos
src/LAoP/Matrix/Internal.hs−30
compare with master
unifiedsplit
@@ -60,7 +60,6 @@ module LAoP.Matrix.Internal
60 Trivial,
60 Trivial,
61
61
62 -- * Primitives
62 -- * Primitives
63− empty,
64 one,
63 one,
65 join,
64 join,
66 fork,
65 fork,
@@ -185,7 +184,6 @@ import qualified Prelude (id, (.))
185
184
186-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
185-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
187data Matrix e cols rows where
186data Matrix e cols rows where
188− Empty :: Matrix e Void Void
189 One :: e -> Matrix e () ()
187 One :: e -> Matrix e () ()
190 Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
188 Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
191 Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
189 Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
@@ -215,7 +213,6 @@ type family Count (d :: Type) :: Nat where
215--
213--
216-- Thanks to Li-Yao Xia this type family is super fast.
214-- Thanks to Li-Yao Xia this type family is super fast.
217type family FromNat (n :: Nat) :: Type where
215type family FromNat (n :: Nat) :: Type where
218− FromNat 0 = Void
219 FromNat 1 = ()
216 FromNat 1 = ()
220 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
217 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
221
218
@@ -247,13 +244,11 @@ instance (Num e) => Category (Matrix e) where
247 (.) = comp
244 (.) = comp
248
245
249instance NFData e => NFData (Matrix e cols rows) where
246instance NFData e => NFData (Matrix e cols rows) where
250− rnf Empty = ()
251 rnf (One e) = rnf e
247 rnf (One e) = rnf e
252 rnf (Join a b) = rnf a `seq` rnf b
248 rnf (Join a b) = rnf a `seq` rnf b
253 rnf (Fork a b) = rnf a `seq` rnf b
249 rnf (Fork a b) = rnf a `seq` rnf b
254
250
255instance Eq e => Eq (Matrix e cols rows) where
251instance Eq e => Eq (Matrix e cols rows) where
256− Empty == Empty = True
257 (One a) == (One b) = a == b
252 (One a) == (One b) = a == b
258 (Join a b) == (Join c d) = a == c && b == d
253 (Join a b) == (Join c d) = a == c && b == d
259 (Fork a b) == (Fork c d) = a == c && b == d
254 (Fork a b) == (Fork c d) = a == c && b == d
@@ -268,18 +263,15 @@ instance Num e => Num (Matrix e cols rows) where
268
263
269 a * b = zipWithM (*) a b
264 a * b = zipWithM (*) a b
270
265
271− abs Empty = Empty
272 abs (One a) = One (abs a)
266 abs (One a) = One (abs a)
273 abs (Join a b) = Join (abs a) (abs b)
267 abs (Join a b) = Join (abs a) (abs b)
274 abs (Fork a b) = Fork (abs a) (abs b)
268 abs (Fork a b) = Fork (abs a) (abs b)
275
269
276− signum Empty = Empty
277 signum (One a) = One (signum a)
270 signum (One a) = One (signum a)
278 signum (Join a b) = Join (signum a) (signum b)
271 signum (Join a b) = Join (signum a) (signum b)
279 signum (Fork a b) = Fork (signum a) (signum b)
272 signum (Fork a b) = Fork (signum a) (signum b)
280
273
281instance Ord e => Ord (Matrix e cols rows) where
274instance Ord e => Ord (Matrix e cols rows) where
282− Empty <= Empty = True
283 (One a) <= (One b) = a <= b
275 (One a) <= (One b) = a <= b
284 (Join a b) <= (Join c d) = (a <= c) && (b <= d)
276 (Join a b) <= (Join c d) = (a <= c) && (b <= d)
285 (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
277 (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
@@ -288,10 +280,6 @@ instance Ord e => Ord (Matrix e cols rows) where
288
280
289-- Primitives
281-- Primitives
290
282
291−-- | Empty matrix constructor
292−empty :: Matrix e Void Void
293−empty = Empty
294−
295-- | Unit matrix constructor
283-- | Unit matrix constructor
296one :: e -> Matrix e () ()
284one :: e -> Matrix e () ()
297one = One
285one = One
@@ -327,10 +315,6 @@ class FromLists cols rows where
327 -- error if the dimensions do not match.
315 -- error if the dimensions do not match.
328 fromLists :: [[e]] -> Matrix e cols rows
316 fromLists :: [[e]] -> Matrix e cols rows
329
317
330−instance FromLists Void Void where
331− fromLists [] = Empty
332− fromLists _ = error "Wrong dimensions"
333−
334instance {-# OVERLAPPING #-} FromLists () () where
318instance {-# OVERLAPPING #-} FromLists () () where
335 fromLists [[e]] = One e
319 fromLists [[e]] = One e
336 fromLists _ = error "Wrong dimensions"
320 fromLists _ = error "Wrong dimensions"
@@ -470,7 +454,6 @@ fromF f =
470
454
471-- | Converts a matrix to a list of lists of elements.
455-- | Converts a matrix to a list of lists of elements.
472toLists :: Matrix e cols rows -> [[e]]
456toLists :: Matrix e cols rows -> [[e]]
473−toLists Empty = []
474toLists (One e) = [[e]]
457toLists (One e) = [[e]]
475toLists (Fork l r) = toLists l ++ toLists r
458toLists (Fork l r) = toLists l ++ toLists r
476toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
459toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
@@ -522,7 +505,6 @@ iden = matrixBuilder' (bool 0 1 . uncurry (==))
522-- This definition takes advantage of divide-and-conquer and fusion laws
505-- This definition takes advantage of divide-and-conquer and fusion laws
523-- from LAoP.
506-- from LAoP.
524comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
507comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
525−comp Empty Empty = Empty
526comp (One a) (One b) = One (a * b)
508comp (One a) (One b) = One (a * b)
527comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
509comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
528comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
510comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
@@ -538,7 +520,6 @@ comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
538infixl 7 .|
520infixl 7 .|
539-- | Scalar multiplication of matrices.
521-- | Scalar multiplication of matrices.
540(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
522(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
541−(.|) _ Empty = Empty
542(.|) e (One a) = One (e * a)
523(.|) e (One a) = One (e * a)
543(.|) e (Join a b) = Join (e .| a) (e .| b)
524(.|) e (Join a b) = Join (e .| a) (e .| b)
544(.|) e (Fork a b) = Fork (e .| a) (e .| b)
525(.|) e (Fork a b) = Fork (e .| a) (e .| b)
@@ -548,7 +529,6 @@ infixl 7 .|
548infixl 7 ./
529infixl 7 ./
549-- | Scalar multiplication of matrices.
530-- | Scalar multiplication of matrices.
550(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
531(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
551−(./) Empty _ = Empty
552(./) (One a) e = One (a / e)
532(./) (One a) e = One (a / e)
553(./) (Join a b) e = Join (a ./ e) (b ./ e)
533(./) (Join a b) e = Join (a ./ e) (b ./ e)
554(./) (Fork a b) e = Fork (a ./ e) (b ./ e)
534(./) (Fork a b) e = Fork (a ./ e) (b ./ e)
@@ -703,7 +683,6 @@ infixl 4 ><
703-- @
683-- @
704abideJF :: Matrix e cols rows -> Matrix e cols rows
684abideJF :: Matrix e cols rows -> Matrix e cols rows
705abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
685abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
706−abideJF Empty = Empty
707abideJF (One e) = One e
686abideJF (One e) = One e
708abideJF (Join a b) = Join (abideJF a) (abideJF b)
687abideJF (Join a b) = Join (abideJF a) (abideJF b)
709abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
688abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
@@ -717,7 +696,6 @@ abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
717-- @
696-- @
718abideFJ :: Matrix e cols rows -> Matrix e cols rows
697abideFJ :: Matrix e cols rows -> Matrix e cols rows
719abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law
698abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law
720−abideFJ Empty = Empty
721abideFJ (One e) = One e
699abideFJ (One e) = One e
722abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
700abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
723abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
701abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
@@ -726,7 +704,6 @@ abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
726
704
727-- | Matrix transposition.
705-- | Matrix transposition.
728tr :: Matrix e cols rows -> Matrix e rows cols
706tr :: Matrix e cols rows -> Matrix e rows cols
729−tr Empty = Empty
730tr (One e) = One e
707tr (One e) = One e
731tr (Join a b) = Fork (tr a) (tr b)
708tr (Join a b) = Fork (tr a) (tr b)
732tr (Fork a b) = Join (tr a) (tr b)
709tr (Fork a b) = Join (tr a) (tr b)
@@ -865,7 +842,6 @@ prettyPrint = putStrLn . pretty
865
842
866-- | Zip two matrices with a given binary function
843-- | Zip two matrices with a given binary function
867zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
844zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
868−zipWithM _ Empty Empty = Empty
869zipWithM f (One a) (One b) = One (f a b)
845zipWithM f (One a) (One b) = One (f a b)
870zipWithM f (Join a b) (Join c d) = Join (zipWithM f a c) (zipWithM f b d)
846zipWithM f (Join a b) (Join c d) = Join (zipWithM f a c) (zipWithM f b d)
871zipWithM f (Fork a b) (Fork c d) = Fork (zipWithM f a c) (zipWithM f b d)
847zipWithM f (Fork a b) (Fork c d) = Fork (zipWithM f a c) (zipWithM f b d)
@@ -890,14 +866,12 @@ fromBool False = nat 0
890
866
891-- | Relational negation
867-- | Relational negation
892negateM :: Relation cols rows -> Relation cols rows
868negateM :: Relation cols rows -> Relation cols rows
893−negateM Empty = Empty
894negateM (One (Nat p)) = One (Nat (negate p))
869negateM (One (Nat p)) = One (Nat (negate p))
895negateM (Join a b) = Join (negateM a) (negateM b)
870negateM (Join a b) = Join (negateM a) (negateM b)
896negateM (Fork a b) = Fork (negateM a) (negateM b)
871negateM (Fork a b) = Fork (negateM a) (negateM b)
897
872
898-- | Relational addition
873-- | Relational addition
899orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
874orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
900−orM Empty Empty = Empty
901orM (One a) (One b) = One (fromBool (toBool a || toBool b))
875orM (One a) (One b) = One (fromBool (toBool a || toBool b))
902orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
876orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
903orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
877orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
@@ -906,7 +880,6 @@ orM x@(Join _ _) y@(Fork _ _) = orM (abideJF x) y
906
880
907-- | Relational multiplication
881-- | Relational multiplication
908andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
882andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
909−andM Empty Empty = Empty
910andM (One a) (One b) = One (fromBool (toBool a && toBool b))
883andM (One a) (One b) = One (fromBool (toBool a && toBool b))
911andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
884andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
912andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
885andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
@@ -915,7 +888,6 @@ andM x@(Join _ _) y@(Fork _ _) = andM (abideJF x) y
915
888
916-- | Relational subtraction
889-- | Relational subtraction
917subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
890subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
918−subM Empty Empty = Empty
919subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
891subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
920subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
892subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
921subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
893subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
@@ -924,7 +896,6 @@ subM x@(Join _ _) y@(Fork _ _) = subM (abideJF x) y
924
896
925-- | Matrix relational composition.
897-- | Matrix relational composition.
926compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
898compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
927−compRel Empty Empty = Empty
928compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
899compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
929compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
900compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
930compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
901compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
@@ -932,7 +903,6 @@ compRel c (Join a b) = Join (compRel c a) (compRel c b) -- Join fusion
932
903
933-- | Matrix relational right division
904-- | Matrix relational right division
934divR :: Relation b c -> Relation b a -> Relation a c
905divR :: Relation b c -> Relation b a -> Relation a c
935−divR Empty Empty = Empty
936divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
906divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
937divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
907divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
938divR (Fork a b) c = Fork (divR a c) (divR b c)
908divR (Fork a b) c = Fork (divR a c) (divR b c)
src/LAoP/Matrix/Nat.hs−4
@@ -67,7 +67,6 @@ module LAoP.Matrix.Nat
67 TrivialP,
67 TrivialP,
68
68
69 -- * Primitives
69 -- * Primitives
70− empty,
71 one,
70 one,
72 join,
71 join,
73 fork,
72 fork,
@@ -180,9 +179,6 @@ type TrivialP a b = I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) *
180
179
181-- Primitives
180-- Primitives
182
181
183−empty :: Matrix e 0 0
184−empty = M I.Empty
185−
186one :: e -> Matrix e 1 1
182one :: e -> Matrix e 1 1
187one = M . I.One
183one = M . I.One
188
184
src/LAoP/Matrix/Type.hs−5
@@ -71,7 +71,6 @@ module LAoP.Matrix.Type
71 One,
71 One,
72
72
73 -- * Primitives
73 -- * Primitives
74− empty,
75 one,
74 one,
76 join,
75 join,
77 fork,
76 fork,
@@ -229,10 +228,6 @@ type One = ()
229
228
230-- Primitives
229-- Primitives
231
230
232−-- | Empty matrix constructor
233−empty :: Matrix e Zero Zero
234−empty = M I.Empty
235−
236-- | Unit matrix constructor
231-- | Unit matrix constructor
237one :: e -> Matrix e One One
232one :: e -> Matrix e One One
238one = M . I.One
233one = M . I.One
src/LAoP/Relation.hs−1
@@ -41,7 +41,6 @@ module LAoP.Relation
41 TrivialP,
41 TrivialP,
42
42
43 -- * Primitives
43 -- * Primitives
44− empty,
45 one,
44 one,
46 join,
45 join,
47 (|||),
46 (|||),
src/LAoP/Relation/Internal.hs+1−6
@@ -52,7 +52,6 @@ module LAoP.Relation.Internal
52 TrivialP,
52 TrivialP,
53
53
54 -- * Primitives
54 -- * Primitives
55− empty,
56 one,
55 one,
57 join,
56 join,
58 (|||),
57 (|||),
@@ -229,10 +228,6 @@ type One = ()
229
228
230-- Primitives
229-- Primitives
231
230
232−-- | Empty matrix constructor
233−empty :: Relation Zero Zero
234−empty = R I.Empty
235−
236-- | Unit matrix constructor
231-- | Unit matrix constructor
237one :: Boolean -> Relation One One
232one :: Boolean -> Relation One One
238one = R . I.One
233one = R . I.One
@@ -383,7 +378,7 @@ belongs = toRel elemR
383-- | The zero relation. A relation where no element of type @a@ relates
378-- | The zero relation. A relation where no element of type @a@ relates
384-- with elements of type @b@.
379-- with elements of type @b@.
385--
380--
386−-- Also known as ⊥ (Bottom) Relation or empty Relation.
381+-- Also known as ⊥ (Bottom) Relation.
387--
382--
388-- @
383-- @
389-- r `.` ⊥ == ⊥ `.` r == ⊥
384-- r `.` ⊥ == ⊥ `.` r == ⊥