on master help sign in
Removed Empty constructor
commitc1152959e01a0714b9725126fd5726352765a40b authorArmando Santos <armandoifsantos@gmail.com> dateSat 9 May 2020, 14:19 (6 years ago) parenta3aa4a2
5 files changed+1−46
src/LAoP/Matrix/Internal.hs−30 src/LAoP/Matrix/Nat.hs−4 src/LAoP/Matrix/Type.hs−5 src/LAoP/Relation.hs−1 src/LAoP/Relation/Internal.hs+1−6
src/LAoP/Matrix/Internal.hs−30
@@ -60,7 +60,6 @@ module LAoP.Matrix.Internal
6060 Trivial,
6161
6262 -- * Primitives
63− empty,
6463 one,
6564 join,
6665 fork,
@@ -185,7 +184,6 @@ import qualified Prelude (id, (.))
185184
186185-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
187186data Matrix e cols rows where
188− Empty :: Matrix e Void Void
189187 One :: e -> Matrix e () ()
190188 Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
191189 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
215213--
216214-- Thanks to Li-Yao Xia this type family is super fast.
217215type family FromNat (n :: Nat) :: Type where
218− FromNat 0 = Void
219216 FromNat 1 = ()
220217 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
221218
@@ -247,13 +244,11 @@ instance (Num e) => Category (Matrix e) where
247244 (.) = comp
248245
249246instance NFData e => NFData (Matrix e cols rows) where
250− rnf Empty = ()
251247 rnf (One e) = rnf e
252248 rnf (Join a b) = rnf a `seq` rnf b
253249 rnf (Fork a b) = rnf a `seq` rnf b
254250
255251instance Eq e => Eq (Matrix e cols rows) where
256− Empty == Empty = True
257252 (One a) == (One b) = a == b
258253 (Join a b) == (Join c d) = a == c && b == d
259254 (Fork a b) == (Fork c d) = a == c && b == d
@@ -268,18 +263,15 @@ instance Num e => Num (Matrix e cols rows) where
268263
269264 a * b = zipWithM (*) a b
270265
271− abs Empty = Empty
272266 abs (One a) = One (abs a)
273267 abs (Join a b) = Join (abs a) (abs b)
274268 abs (Fork a b) = Fork (abs a) (abs b)
275269
276− signum Empty = Empty
277270 signum (One a) = One (signum a)
278271 signum (Join a b) = Join (signum a) (signum b)
279272 signum (Fork a b) = Fork (signum a) (signum b)
280273
281274instance Ord e => Ord (Matrix e cols rows) where
282− Empty <= Empty = True
283275 (One a) <= (One b) = a <= b
284276 (Join a b) <= (Join c d) = (a <= c) && (b <= d)
285277 (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
@@ -288,10 +280,6 @@ instance Ord e => Ord (Matrix e cols rows) where
288280
289281-- Primitives
290282
291−-- | Empty matrix constructor
292−empty :: Matrix e Void Void
293−empty = Empty
294−
295283-- | Unit matrix constructor
296284one :: e -> Matrix e () ()
297285one = One
@@ -327,10 +315,6 @@ class FromLists cols rows where
327315 -- error if the dimensions do not match.
328316 fromLists :: [[e]] -> Matrix e cols rows
329317
330−instance FromLists Void Void where
331− fromLists [] = Empty
332− fromLists _ = error "Wrong dimensions"
333−
334318instance {-# OVERLAPPING #-} FromLists () () where
335319 fromLists [[e]] = One e
336320 fromLists _ = error "Wrong dimensions"
@@ -470,7 +454,6 @@ fromF f =
470454
471455-- | Converts a matrix to a list of lists of elements.
472456toLists :: Matrix e cols rows -> [[e]]
473−toLists Empty = []
474457toLists (One e) = [[e]]
475458toLists (Fork l r) = toLists l ++ toLists r
476459toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
@@ -522,7 +505,6 @@ iden = matrixBuilder' (bool 0 1 . uncurry (==))
522505-- This definition takes advantage of divide-and-conquer and fusion laws
523506-- from LAoP.
524507comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
525−comp Empty Empty = Empty
526508comp (One a) (One b) = One (a * b)
527509comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
528510comp (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
538520infixl 7 .|
539521-- | Scalar multiplication of matrices.
540522(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
541−(.|) _ Empty = Empty
542523(.|) e (One a) = One (e * a)
543524(.|) e (Join a b) = Join (e .| a) (e .| b)
544525(.|) e (Fork a b) = Fork (e .| a) (e .| b)
@@ -548,7 +529,6 @@ infixl 7 .|
548529infixl 7 ./
549530-- | Scalar multiplication of matrices.
550531(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
551−(./) Empty _ = Empty
552532(./) (One a) e = One (a / e)
553533(./) (Join a b) e = Join (a ./ e) (b ./ e)
554534(./) (Fork a b) e = Fork (a ./ e) (b ./ e)
@@ -703,7 +683,6 @@ infixl 4 ><
703683-- @
704684abideJF :: Matrix e cols rows -> Matrix e cols rows
705685abideJF (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
707686abideJF (One e) = One e
708687abideJF (Join a b) = Join (abideJF a) (abideJF b)
709688abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
@@ -717,7 +696,6 @@ abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
717696-- @
718697abideFJ :: Matrix e cols rows -> Matrix e cols rows
719698abideFJ (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
721699abideFJ (One e) = One e
722700abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
723701abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
@@ -726,7 +704,6 @@ abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
726704
727705-- | Matrix transposition.
728706tr :: Matrix e cols rows -> Matrix e rows cols
729−tr Empty = Empty
730707tr (One e) = One e
731708tr (Join a b) = Fork (tr a) (tr b)
732709tr (Fork a b) = Join (tr a) (tr b)
@@ -865,7 +842,6 @@ prettyPrint = putStrLn . pretty
865842
866843-- | Zip two matrices with a given binary function
867844zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
868−zipWithM _ Empty Empty = Empty
869845zipWithM f (One a) (One b) = One (f a b)
870846zipWithM f (Join a b) (Join c d) = Join (zipWithM f a c) (zipWithM f b d)
871847zipWithM f (Fork a b) (Fork c d) = Fork (zipWithM f a c) (zipWithM f b d)
@@ -890,14 +866,12 @@ fromBool False = nat 0
890866
891867-- | Relational negation
892868negateM :: Relation cols rows -> Relation cols rows
893−negateM Empty = Empty
894869negateM (One (Nat p)) = One (Nat (negate p))
895870negateM (Join a b) = Join (negateM a) (negateM b)
896871negateM (Fork a b) = Fork (negateM a) (negateM b)
897872
898873-- | Relational addition
899874orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
900−orM Empty Empty = Empty
901875orM (One a) (One b) = One (fromBool (toBool a || toBool b))
902876orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
903877orM (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
906880
907881-- | Relational multiplication
908882andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
909−andM Empty Empty = Empty
910883andM (One a) (One b) = One (fromBool (toBool a && toBool b))
911884andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
912885andM (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
915888
916889-- | Relational subtraction
917890subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
918−subM Empty Empty = Empty
919891subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
920892subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
921893subM (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
924896
925897-- | Matrix relational composition.
926898compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
927−compRel Empty Empty = Empty
928899compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
929900compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
930901compRel (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
932903
933904-- | Matrix relational right division
934905divR :: Relation b c -> Relation b a -> Relation a c
935−divR Empty Empty = Empty
936906divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
937907divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
938908divR (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
6767 TrivialP,
6868
6969 -- * Primitives
70− empty,
7170 one,
7271 join,
7372 fork,
@@ -180,9 +179,6 @@ type TrivialP a b = I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) *
180179
181180-- Primitives
182181
183−empty :: Matrix e 0 0
184−empty = M I.Empty
185−
186182one :: e -> Matrix e 1 1
187183one = M . I.One
188184
src/LAoP/Matrix/Type.hs−5
@@ -71,7 +71,6 @@ module LAoP.Matrix.Type
7171 One,
7272
7373 -- * Primitives
74− empty,
7574 one,
7675 join,
7776 fork,
@@ -229,10 +228,6 @@ type One = ()
229228
230229-- Primitives
231230
232−-- | Empty matrix constructor
233−empty :: Matrix e Zero Zero
234−empty = M I.Empty
235−
236231-- | Unit matrix constructor
237232one :: e -> Matrix e One One
238233one = M . I.One
src/LAoP/Relation.hs−1
@@ -41,7 +41,6 @@ module LAoP.Relation
4141 TrivialP,
4242
4343 -- * Primitives
44− empty,
4544 one,
4645 join,
4746 (|||),
src/LAoP/Relation/Internal.hs+1−6
@@ -52,7 +52,6 @@ module LAoP.Relation.Internal
5252 TrivialP,
5353
5454 -- * Primitives
55− empty,
5655 one,
5756 join,
5857 (|||),
@@ -229,10 +228,6 @@ type One = ()
229228
230229-- Primitives
231230
232−-- | Empty matrix constructor
233−empty :: Relation Zero Zero
234−empty = R I.Empty
235−
236231-- | Unit matrix constructor
237232one :: Boolean -> Relation One One
238233one = R . I.One
@@ -383,7 +378,7 @@ belongs = toRel elemR
383378-- | The zero relation. A relation where no element of type @a@ relates
384379-- with elements of type @b@.
385380--
386−-- Also known as ⊥ (Bottom) Relation or empty Relation.
381+-- Also known as ⊥ (Bottom) Relation.
387382--
388383-- @
389384-- r `.` ⊥ == ⊥ `.` r == ⊥