@@ -30,7 +30,7 @@
30-- motivation behind the library, the underlying theory, and implementation details.
30-- motivation behind the library, the underlying theory, and implementation details.
32-- This module offers many of the combinators mentioned in the work of
32-- This module offers many of the combinators mentioned in the work of
33−-- Macedo (2012) and Oliveira (2012).
33+-- Macedo (2012) and Oliveira (2012).
35-- This is an Internal module and it is no supposed to be imported.
35-- This is an Internal module and it is no supposed to be imported.
@@ -43,23 +43,23 @@ module LAoP.Matrix.Internal
44 -- There exists two type families that make it easier to write
44 -- There exists two type families that make it easier to write
45 -- matrix dimensions: 'FromNat' and 'Count'. This approach
45 -- matrix dimensions: 'FromNat' and 'Count'. This approach
46− -- leads to a very straightforward implementation
46+ -- leads to a very straightforward implementation
47− -- of LAoP combinators.
47+ -- of LAoP combinators.
49 -- * Type safe matrix representation
49 -- * Type safe matrix representation
50 Matrix (..),
50 Matrix (..),
52 -- * Constraint type aliases
52 -- * Constraint type aliases
53 Countable,
53 Countable,
54− CountableDimensions,
54+ CountableDims,
55 CountableN,
55 CountableN,
56− CountableDimensionsN,
56+ CountableDimsN,
61 -- * Primitives
62 -- * Primitives
@@ -86,7 +86,9 @@ module LAoP.Matrix.Internal
87 -- ** Get dimensions
87 -- ** Get dimensions
91 -- ** Matrix Transposition
93 -- ** Matrix Transposition
@@ -174,6 +176,7 @@ import Data.Kind
174import Data.List
176import Data.List
175import Data.Maybe
177import Data.Maybe
176import Data.Proxy
178import Data.Proxy
177import Data.Void
180import Data.Void
178import GHC.TypeLits
181import GHC.TypeLits
179import Data.Type.Equality
182import Data.Type.Equality
@@ -184,7 +187,6 @@ import qualified Prelude (id, (.))
185-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
188-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
186data Matrix e cols rows where
189data Matrix e cols rows where
187− Empty :: Matrix e Void Void
188 One :: e -> Matrix e () ()
190 One :: e -> Matrix e () ()
189 Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
191 Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
190 Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
192 Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
@@ -214,7 +216,6 @@ type family Count (d :: Type) :: Nat where
215-- Thanks to Li-Yao Xia this type family is super fast.
217-- Thanks to Li-Yao Xia this type family is super fast.
216type family FromNat (n :: Nat) :: Type where
218type family FromNat (n :: Nat) :: Type where
218 FromNat 1 = ()
219 FromNat 1 = ()
219 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
220 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
@@ -231,27 +232,26 @@ type family Normalize (d :: Type) :: Type where
231-- | Constraint type synonyms to keep the type signatures less convoluted
232-- | Constraint type synonyms to keep the type signatures less convoluted
232type Countable a = KnownNat (Count a)
233type Countable a = KnownNat (Count a)
233type CountableN a = KnownNat (Count (Normalize a))
234type CountableN a = KnownNat (Count (Normalize a))
234−type CountableDimensions a b = (Countable a, Countable b)
235+type CountableDims a b = (Countable a, Countable b)
235−type CountableDimensionsN a b = (CountableN a, CountableN b)
236+type CountableDimsN a b = (CountableN a, CountableN b)
237+type FL a b = FromLists a b
236−type FromListsN e a b = FromLists e (Normalize a) (Normalize b)
238+type FLN a b = FromLists (Normalize a) (Normalize b)
237type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
239type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
238type Trivial a = FromNat (Count a) ~ a
240type Trivial a = FromNat (Count a) ~ a
240-- | It is possible to implement a constrained version of the category type
242-- | It is possible to implement a constrained version of the category type
242instance (Num e) => Category (Matrix e) where
244instance (Num e) => Category (Matrix e) where
243− type Object (Matrix e) a = (FromLists e a a, Countable a)
245+ type Object (Matrix e) a = (FL a a, Countable a)
244− id = iden
246+ id = iden
245 (.) = comp
247 (.) = comp
247instance NFData e => NFData (Matrix e cols rows) where
249instance NFData e => NFData (Matrix e cols rows) where
249 rnf (One e) = rnf e
250 rnf (One e) = rnf e
250 rnf (Join a b) = rnf a `seq` rnf b
251 rnf (Join a b) = rnf a `seq` rnf b
251 rnf (Fork a b) = rnf a `seq` rnf b
252 rnf (Fork a b) = rnf a `seq` rnf b
253instance Eq e => Eq (Matrix e cols rows) where
254instance Eq e => Eq (Matrix e cols rows) where
254− Empty == Empty = True
255 (One a) == (One b) = a == b
255 (One a) == (One b) = a == b
256 (Join a b) == (Join c d) = a == c && b == d
256 (Join a b) == (Join c d) = a == c && b == d
257 (Fork a b) == (Fork c d) = a == c && b == d
257 (Fork a b) == (Fork c d) = a == c && b == d
@@ -259,25 +259,21 @@ instance Eq e => Eq (Matrix e cols rows) where
259 x@(Join _ _) == y@(Fork _ _) = abideJF x == y
259 x@(Join _ _) == y@(Fork _ _) = abideJF x == y
261instance Num e => Num (Matrix e cols rows) where
261instance Num e => Num (Matrix e cols rows) where
263 a + b = zipWithM (+) a b
262 a + b = zipWithM (+) a b
265 a - b = zipWithM (-) a b
264 a - b = zipWithM (-) a b
267 a * b = zipWithM (*) a b
266 a * b = zipWithM (*) a b
270 abs (One a) = One (abs a)
268 abs (One a) = One (abs a)
271 abs (Join a b) = Join (abs a) (abs b)
269 abs (Join a b) = Join (abs a) (abs b)
272 abs (Fork a b) = Fork (abs a) (abs b)
270 abs (Fork a b) = Fork (abs a) (abs b)
274− signum Empty = Empty
275 signum (One a) = One (signum a)
272 signum (One a) = One (signum a)
276 signum (Join a b) = Join (signum a) (signum b)
273 signum (Join a b) = Join (signum a) (signum b)
277 signum (Fork a b) = Fork (signum a) (signum b)
274 signum (Fork a b) = Fork (signum a) (signum b)
279instance Ord e => Ord (Matrix e cols rows) where
276instance Ord e => Ord (Matrix e cols rows) where
280− Empty <= Empty = True
281 (One a) <= (One b) = a <= b
277 (One a) <= (One b) = a <= b
282 (Join a b) <= (Join c d) = (a <= c) && (b <= d)
278 (Join a b) <= (Join c d) = (a <= c) && (b <= d)
283 (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
279 (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
@@ -286,10 +282,6 @@ instance Ord e => Ord (Matrix e cols rows) where
287-- Primitives
283-- Primitives
289−-- | Empty matrix constructor
290−empty :: Matrix e Void Void
293-- | Unit matrix constructor
285-- | Unit matrix constructor
294one :: e -> Matrix e () ()
286one :: e -> Matrix e () ()
@@ -320,40 +312,39 @@ infixl 2 ===
321-- Given that it is not possible to branch on types at the term level type
313-- Given that it is not possible to branch on types at the term level type
322-- classes are needed very much like an inductive definition but on types.
314-- classes are needed very much like an inductive definition but on types.
323−class FromLists e cols rows where
315+class FromLists cols rows where
324 -- | Build a matrix out of a list of list of elements. Throws a runtime
316 -- | Build a matrix out of a list of list of elements. Throws a runtime
325 -- error if the dimensions do not match.
317 -- error if the dimensions do not match.
326 fromLists :: [[e]] -> Matrix e cols rows
318 fromLists :: [[e]] -> Matrix e cols rows
328−instance FromLists e Void Void where
320+instance FromLists () () where
329− fromLists [] = Empty
330− fromLists _ = error "Wrong dimensions"
332−instance {-# OVERLAPPING #-} FromLists e () () where
333 fromLists [[e]] = One e
321 fromLists [[e]] = One e
334 fromLists _ = error "Wrong dimensions"
322 fromLists _ = error "Wrong dimensions"
336−instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
324+instance (FromLists cols ()) => FromLists (Either () cols) () where
337 fromLists [h : t] = Join (One h) (fromLists [t])
325 fromLists [h : t] = Join (One h) (fromLists [t])
338 fromLists _ = error "Wrong dimensions"
326 fromLists _ = error "Wrong dimensions"
328+instance {-# OVERLAPPABLE #-}
340−instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), Countable a) => FromLists e (Either a b) () where
329+ (FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () where
341 fromLists [l] =
330 fromLists [l] =
342 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
331 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
343 in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
332 in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
344 fromLists _ = error "Wrong dimensions"
333 fromLists _ = error "Wrong dimensions"
346−instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
335+instance (FromLists () rows) => FromLists () (Either () rows) where
347 fromLists ([h] : t) = Fork (One h) (fromLists t)
336 fromLists ([h] : t) = Fork (One h) (fromLists t)
348 fromLists _ = error "Wrong dimensions"
337 fromLists _ = error "Wrong dimensions"
339+instance {-# OVERLAPPABLE #-}
350−instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, Countable a) => FromLists e () (Either a b) where
340+ (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where
351− fromLists l@([_] : _) =
341+ fromLists l@([_] : _) =
352 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
342 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
353 in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
343 in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
354 fromLists _ = error "Wrong dimensions"
344 fromLists _ = error "Wrong dimensions"
356−instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a b) d, Countable c) => FromLists e (Either a b) (Either c d) where
346+instance (FromLists (Either a b) c, FromLists (Either a b) d, Countable c)
347+ => FromLists (Either a b) (Either c d) where
357 fromLists l@(h : t) =
348 fromLists l@(h : t) =
358 let lh = length h
349 let lh = length h
359 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
350 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
@@ -366,8 +357,8 @@ instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a
366-- a construction function that operates with indices.
357-- a construction function that operates with indices.
367matrixBuilder' ::
358matrixBuilder' ::
368 forall e cols rows.
359 forall e cols rows.
369− ( FromLists e cols rows,
360+ ( FL cols rows,
370− CountableDimensions cols rows
361+ CountableDims cols rows
371 ) => ((Int, Int) -> e) -> Matrix e cols rows
362 ) => ((Int, Int) -> e) -> Matrix e cols rows
372matrixBuilder' f =
363matrixBuilder' f =
373 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
364 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
@@ -379,17 +370,16 @@ matrixBuilder' f =
379-- a construction function that operates with arbitrary types.
370-- a construction function that operates with arbitrary types.
380matrixBuilder ::
371matrixBuilder ::
381 forall e a b.
372 forall e a b.
382− ( FromListsN e a b,
373+ ( FLN a b,
386 Bounded a,
376 Bounded a,
387 Bounded b,
377 Bounded b,
389− CountableDimensionsN a b
379+ Countable b
390 ) => ((a, b) -> e) -> Matrix e (Normalize a) (Normalize b)
380 ) => ((a, b) -> e) -> Matrix e (Normalize a) (Normalize b)
391matrixBuilder f =
381matrixBuilder f =
392− let r = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
382+ let r = fromInteger $ natVal (Proxy :: Proxy (Count b))
393 positions = [(a, b) | a <- [minBound .. maxBound], b <- [minBound .. maxBound]]
383 positions = [(a, b) | a <- [minBound .. maxBound], b <- [minBound .. maxBound]]
394 in fromLists . map (map f) . transpose . buildList r $ positions
384 in fromLists . map (map f) . transpose . buildList r $ positions
@@ -397,11 +387,11 @@ matrixBuilder f =
397 buildList r l = take r l : buildList r (drop r l)
387 buildList r l = take r l : buildList r (drop r l)
399-- | Constructs a column vector matrix
389-- | Constructs a column vector matrix
400−col :: (FromLists e () rows) => [e] -> Matrix e () rows
390+col :: (FL () rows) => [e] -> Matrix e () rows
401col = fromLists . map (: [])
391col = fromLists . map (: [])
403-- | Constructs a row vector matrix
393-- | Constructs a row vector matrix
404−row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
394+row :: (FL cols ()) => [e] -> Matrix e cols ()
405row = fromLists . (: [])
395row = fromLists . (: [])
407-- | Lifts functions to matrices with arbitrary dimensions.
397-- | Lifts functions to matrices with arbitrary dimensions.
@@ -411,8 +401,8 @@ row = fromLists . (: [])
412 forall a b cols rows e.
402 forall a b cols rows e.
413 ( Liftable e a b,
403 ( Liftable e a b,
414− CountableDimensions cols rows,
404+ CountableDims cols rows,
415− FromLists e rows cols
405+ FL rows cols
417 (a -> b) ->
407 (a -> b) ->
418 Matrix e cols rows
408 Matrix e cols rows
@@ -440,35 +430,17 @@ fromF' f =
441 forall a b e.
431 forall a b e.
442 ( Liftable e a b,
432 ( Liftable e a b,
443− CountableDimensionsN a b,
433+ CountableDimsN a b,
444− FromListsN e b a
434+ FLN b a
446 (a -> b) ->
436 (a -> b) ->
447 Matrix e (Normalize a) (Normalize b)
437 Matrix e (Normalize a) (Normalize b)
448−fromF f =
438+fromF = fromF'
449− let minA = minBound @a
453− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
454− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
455− elementsA = take ccols [minA .. maxA]
456− elementsB = take rrows [minB .. maxB]
457− combinations = (,) <$> elementsA <*> elementsB
458− combAp = map snd . sort . map (\(a, b) -> if f a == b
459− then ((fromEnum a, fromEnum b), 1)
460− else ((fromEnum a, fromEnum b), 0)) $ combinations
461− mList = buildList combAp rrows
462− in tr $ fromLists mList
465− buildList l r = take r l : buildList (drop r l) r
467-- Conversion
440-- Conversion
469-- | Converts a matrix to a list of lists of elements.
442-- | Converts a matrix to a list of lists of elements.
470toLists :: Matrix e cols rows -> [[e]]
443toLists :: Matrix e cols rows -> [[e]]
472toLists (One e) = [[e]]
444toLists (One e) = [[e]]
473toLists (Fork l r) = toLists l ++ toLists r
445toLists (Fork l r) = toLists l ++ toLists r
474toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
446toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
@@ -480,7 +452,7 @@ toList = concat . toLists
480-- Zeros Matrix
452-- Zeros Matrix
482-- | The zero matrix. A matrix wholly filled with zeros.
454-- | The zero matrix. A matrix wholly filled with zeros.
483−zeros :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows
455+zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
484zeros = matrixBuilder' (const 0)
456zeros = matrixBuilder' (const 0)
486-- Ones Matrix
458-- Ones Matrix
@@ -488,20 +460,20 @@ zeros = matrixBuilder' (const 0)
488-- | The ones matrix. A matrix wholly filled with ones.
460-- | The ones matrix. A matrix wholly filled with ones.
490-- Also known as T (Top) matrix.
462-- Also known as T (Top) matrix.
491−ones :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows
463+ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
492ones = matrixBuilder' (const 1)
464ones = matrixBuilder' (const 1)
494-- Const Matrix
466-- Const Matrix
496-- | The constant matrix constructor. A matrix wholly filled with a given
468-- | The constant matrix constructor. A matrix wholly filled with a given
498−constant :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => e -> Matrix e cols rows
470+constant :: (Num e, FL cols rows, CountableDims cols rows) => e -> Matrix e cols rows
499constant e = matrixBuilder' (const e)
471constant e = matrixBuilder' (const e)
501-- Bang Matrix
473-- Bang Matrix
503-- | The T (Top) row vector matrix.
475-- | The T (Top) row vector matrix.
504−bang :: forall e cols. (Num e, Enum e, FromLists e cols (), Countable cols) => Matrix e cols ()
476+bang :: forall e cols. (Num e, Enum e, FL cols (), Countable cols) => Matrix e cols ()
506 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
478 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
507 in fromLists [take c [1, 1 ..]]
479 in fromLists [take c [1, 1 ..]]
@@ -509,7 +481,7 @@ bang =
509-- iden Matrix
481-- iden Matrix
511-- | iden matrix.
483-- | iden matrix.
512−iden :: forall e cols . (Num e, FromLists e cols cols, Countable cols) => Matrix e cols cols
484+iden :: forall e cols . (Num e, FL cols cols, Countable cols) => Matrix e cols cols
513iden = matrixBuilder' (bool 0 1 . uncurry (==))
485iden = matrixBuilder' (bool 0 1 . uncurry (==))
514{-# NOINLINE iden #-}
486{-# NOINLINE iden #-}
@@ -520,13 +492,12 @@ iden = matrixBuilder' (bool 0 1 . uncurry (==))
520-- This definition takes advantage of divide-and-conquer and fusion laws
492-- This definition takes advantage of divide-and-conquer and fusion laws
521-- from LAoP.
493-- from LAoP.
522comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
494comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
523−comp Empty Empty = Empty
524comp (One a) (One b) = One (a * b)
495comp (One a) (One b) = One (a * b)
525comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
496comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
526comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
497comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
527comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
498comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
528{-# NOINLINE comp #-}
499{-# NOINLINE comp #-}
529−{-# RULES
500+{-# RULES
530 "comp/iden1" forall m. comp m iden = m ;
501 "comp/iden1" forall m. comp m iden = m ;
531 "comp/iden2" forall m. comp iden m = m
502 "comp/iden2" forall m. comp iden m = m
@@ -536,7 +507,6 @@ comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
536infixl 7 .|
507infixl 7 .|
537-- | Scalar multiplication of matrices.
508-- | Scalar multiplication of matrices.
538(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
509(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
540(.|) e (One a) = One (e * a)
510(.|) e (One a) = One (e * a)
541(.|) e (Join a b) = Join (e .| a) (e .| b)
511(.|) e (Join a b) = Join (e .| a) (e .| b)
542(.|) e (Fork a b) = Fork (e .| a) (e .| b)
512(.|) e (Fork a b) = Fork (e .| a) (e .| b)
@@ -546,7 +516,6 @@ infixl 7 .|
546infixl 7 ./
516infixl 7 ./
547-- | Scalar multiplication of matrices.
517-- | Scalar multiplication of matrices.
548(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
518(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
550(./) (One a) e = One (a / e)
519(./) (One a) e = One (a / e)
551(./) (Join a b) e = Join (a ./ e) (b ./ e)
520(./) (Join a b) e = Join (a ./ e) (b ./ e)
552(./) (Fork a b) e = Fork (a ./ e) (b ./ e)
521(./) (Fork a b) e = Fork (a ./ e) (b ./ e)
@@ -554,45 +523,59 @@ infixl 7 ./
554-- Projections
523-- Projections
556-- | Biproduct first component projection
525-- | Biproduct first component projection
557−p1 :: (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e (Either m n) m
526+p1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e (Either m n) m
558p1 = join id zeros
527p1 = join id zeros
560-- | Biproduct second component projection
529-- | Biproduct second component projection
561−p2 :: (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e (Either m n) n
530+p2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e (Either m n) n
562p2 = join zeros id
531p2 = join zeros id
564-- Injections
533-- Injections
566-- | Biproduct first component injection
535-- | Biproduct first component injection
567−i1 :: (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
536+i1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e m (Either m n)
568i1 = tr p1
537i1 = tr p1
570-- | Biproduct second component injection
539-- | Biproduct second component injection
571−i2 :: (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
540+i2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e n (Either m n)
572i2 = tr p2
541i2 = tr p2
574-- Dimensions
543-- Dimensions
576-- | Obtain the number of rows.
545-- | Obtain the number of rows.
578−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
547+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
579−-- dimensions in constant time.
548+-- dimensions in constant time. For a version that doesn't require the
580−--
549+-- constraint see 'rows''.
581−-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
582−-- exchange for performance.
583rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
550rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
584rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
551rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
553+-- | Obtain the number of rows in an inefficient manner, but without any
556+-- For a more efficient version see 'rows'.
557+rows' :: Matrix e cols rows -> Int
559+rows' (Join lhs _) = rows' lhs
560+rows' (Fork top bottom) = rows' top + rows' bottom
586-- | Obtain the number of columns.
562-- | Obtain the number of columns.
588−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
589−-- dimensions in constant time.
591−-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
564+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
592−-- exchange for performance.
565+-- dimensions in constant time. For a version that doesn't require the
566+-- constraint see 'columns''.
593columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
567columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
594columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
568columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
570+-- | Obtain the number of columns in an inefficient manner, but without any
573+-- For a more efficient version see 'columns'.
574+columns' :: Matrix e cols rows -> Int
576+columns' (Join lhs rhs) = columns' lhs + columns' rhs
577+columns' (Fork top _) = columns' top
596-- Coproduct Bifunctor
579-- Coproduct Bifunctor
598infixl 5 -|-
581infixl 5 -|-
@@ -601,11 +584,11 @@ infixl 5 -|-
602 forall e n k m j.
585 forall e n k m j.
604− CountableDimensions j k,
587+ CountableDims j k,
605− FromLists e k k,
588+ FL k k,
606− FromLists e j k,
589+ FL j k,
607− FromLists e k j,
590+ FL k j,
608− FromLists e j j
591+ FL j j
610 Matrix e n k ->
593 Matrix e n k ->
611 Matrix e m j ->
594 Matrix e m j ->
@@ -618,8 +601,8 @@ infixl 5 -|-
619 forall e m k .
602 forall e m k .
621− CountableDimensions k m,
604+ CountableDims k m,
622− FromLists e (Normalize (m, k)) m,
605+ FL (Normalize (m, k)) m,
623 CountableN (m, k)
606 CountableN (m, k)
624 ) => Matrix e (Normalize (m, k)) m
607 ) => Matrix e (Normalize (m, k)) m
625fstM = matrixBuilder' f
608fstM = matrixBuilder' f
@@ -633,8 +616,8 @@ fstM = matrixBuilder' f
634 forall e m k .
617 forall e m k .
636− CountableDimensions k m,
619+ CountableDims k m,
637− FromLists e (Normalize (m, k)) k,
620+ FL (Normalize (m, k)) k,
638 CountableN (m, k)
621 CountableN (m, k)
639 ) => Matrix e (Normalize (m, k)) k
622 ) => Matrix e (Normalize (m, k)) k
640sndM = matrixBuilder' f
623sndM = matrixBuilder' f
@@ -647,7 +630,7 @@ sndM = matrixBuilder' f
647-- | Khatri Rao Matrix product also known as matrix pairing.
630-- | Khatri Rao Matrix product also known as matrix pairing.
649-- NOTE: That this is not a true categorical product, see for instance:
632-- NOTE: That this is not a true categorical product, see for instance:
652-- | fstM . kr a b == a
635-- | fstM . kr a b == a
653-- kr a b ==> |
636-- kr a b ==> |
@@ -658,10 +641,10 @@ sndM = matrixBuilder' f
659 forall e cols a b.
642 forall e cols a b.
661− CountableDimensions a b,
644+ CountableDims a b,
662 CountableN (a, b),
645 CountableN (a, b),
663− FromLists e (Normalize (a, b)) a,
646+ FL (Normalize (a, b)) a,
664− FromLists e (Normalize (a, b)) b
647+ FL (Normalize (a, b)) b
665 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
648 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
667 let fstM' = fstM @e @a @b
650 let fstM' = fstM @e @a @b
@@ -676,14 +659,14 @@ infixl 4 ><
677 forall e m p n q.
660 forall e m p n q.
679− CountableDimensions m n,
662+ CountableDims m n,
680− CountableDimensions p q,
663+ CountableDims p q,
681− CountableDimensionsN (m, n) (p, q),
664+ CountableDimsN (m, n) (p, q),
682− FromLists e (Normalize (m, n)) m,
665+ FL (Normalize (m, n)) m,
683− FromLists e (Normalize (m, n)) n,
666+ FL (Normalize (m, n)) n,
684− FromLists e (Normalize (p, q)) p,
667+ FL (Normalize (p, q)) p,
685− FromLists e (Normalize (p, q)) q
668+ FL (Normalize (p, q)) q
687 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
670 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
688(><) a b =
671(><) a b =
689 let fstM' = fstM @e @m @n
672 let fstM' = fstM @e @m @n
@@ -701,7 +684,6 @@ infixl 4 ><
702abideJF :: Matrix e cols rows -> Matrix e cols rows
685abideJF :: Matrix e cols rows -> Matrix e cols rows
703abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
686abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
704−abideJF Empty = Empty
705abideJF (One e) = One e
687abideJF (One e) = One e
706abideJF (Join a b) = Join (abideJF a) (abideJF b)
688abideJF (Join a b) = Join (abideJF a) (abideJF b)
707abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
689abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
@@ -715,7 +697,6 @@ abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
716abideFJ :: Matrix e cols rows -> Matrix e cols rows
698abideFJ :: Matrix e cols rows -> Matrix e cols rows
717abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law
699abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law
718−abideFJ Empty = Empty
719abideFJ (One e) = One e
700abideFJ (One e) = One e
720abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
701abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
721abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
702abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
@@ -724,7 +705,6 @@ abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
725-- | Matrix transposition.
706-- | Matrix transposition.
726tr :: Matrix e cols rows -> Matrix e rows cols
707tr :: Matrix e cols rows -> Matrix e rows cols
728tr (One e) = One e
708tr (One e) = One e
729tr (Join a b) = Fork (tr a) (tr b)
709tr (Join a b) = Fork (tr a) (tr b)
730tr (Fork a b) = Join (tr a) (tr b)
710tr (Fork a b) = Join (tr a) (tr b)
@@ -733,32 +713,32 @@ tr (Fork a b) = Join (tr a) (tr b)
734-- | Selective functors 'select' operator equivalent inspired by the
714-- | Selective functors 'select' operator equivalent inspired by the
735-- ArrowMonad solution presented in the paper.
715-- ArrowMonad solution presented in the paper.
736−select :: (Num e, FromLists e b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
716+select :: (Num e, FL b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
737select (Fork a b) y = y . a + b -- Divide-and-conquer law
717select (Fork a b) y = y . a + b -- Divide-and-conquer law
738select (Join (Fork a c) (Fork b d)) y = join (y . a + c) (y . b + d) -- Pattern matching + DnC law
718select (Join (Fork a c) (Fork b d)) y = join (y . a + c) (y . b + d) -- Pattern matching + DnC law
739select m y = join y id . m
719select m y = join y id . m
743− CountableDimensions a b,
723+ CountableDims a b,
744− CountableDimensions c (Either b c),
724+ CountableDims c (Either b c),
745− FromLists e c b,
725+ FL c b,
746− FromLists e a b,
726+ FL a b,
747− FromLists e a a,
727+ FL a a,
748− FromLists e b b,
728+ FL b b,
749− FromLists e c c,
729+ FL c c,
750− FromLists e b a,
730+ FL b a,
751− FromLists e b c,
731+ FL b c,
752− FromLists e (Either b c) b,
732+ FL (Either b c) b,
753− FromLists e (Either b c) c
733+ FL (Either b c) c
755 => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c
735 => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c
756branch x l r = f x `select` g l `select` r
736branch x l r = f x `select` g l `select` r
758− f :: (Num e, Countable a, CountableDimensions b c, FromLists e a b, FromLists e c b, FromLists e b b, FromLists e b a, FromLists e a a)
738+ f :: (Num e, Countable a, CountableDims b c, FL a b, FL c b, FL b b, FL b a, FL a a)
759 => Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
739 => Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
760 f m = fork (tr i1) (i1 . tr i2) . m
740 f m = fork (tr i1) (i1 . tr i2) . m
761− g :: (Num e, CountableDimensions b c, FromLists e b c, FromLists e c c) => Matrix e a c -> Matrix e a (Either b c)
741+ g :: (Num e, CountableDims b c, FL b c, FL c c) => Matrix e a c -> Matrix e a (Either b c)
762 g m = i2 . m
742 g m = i2 . m
764-- McCarthy's Conditional
744-- McCarthy's Conditional
@@ -767,9 +747,9 @@ branch x l r = f x `select` g l `select` r
768 ( Trivial cols,
748 ( Trivial cols,
769 Countable cols,
749 Countable cols,
770− FromLists e () cols,
750+ FL () cols,
771− FromLists e cols (),
751+ FL cols (),
772− FromLists e cols cols,
752+ FL cols cols,
773 Bounded a,
753 Bounded a,
@@ -782,9 +762,9 @@ cond p f g = join f g . grd p
783 ( Trivial q,
763 ( Trivial q,
784 Countable q,
764 Countable q,
785− FromLists e () q,
765+ FL () q,
786− FromLists e q (),
766+ FL q (),
787− FromLists e q q,
767+ FL q q,
788 Bounded a,
768 Bounded a,
@@ -798,9 +778,9 @@ corr ::
798 forall e a q .
778 forall e a q .
799 ( Trivial q,
779 ( Trivial q,
800 Countable q,
780 Countable q,
801− FromLists e () q,
781+ FL () q,
802− FromLists e q (),
782+ FL q (),
803− FromLists e q q,
783+ FL q q,
804 Liftable e a Bool
784 Liftable e a Bool
806 => (a -> Bool) -> Matrix e q q
786 => (a -> Bool) -> Matrix e q q
@@ -829,7 +809,7 @@ prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
829 fill str = replicate (widest - length str - 2) ' ' ++ str
809 fill str = replicate (widest - length str - 2) ' ' ++ str
831-- | Matrix pretty printer
811-- | Matrix pretty printer
832−pretty :: (CountableDimensions cols rows, Show e) => Matrix e cols rows -> String
812+pretty :: (CountableDims cols rows, Show e) => Matrix e cols rows -> String
833pretty m = concat
813pretty m = concat
834 [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"
814 [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"
835 , unlines
815 , unlines
@@ -858,12 +838,11 @@ pretty m = concat
858 (safeGet i j m)
838 (safeGet i j m)
860-- | Matrix pretty printer
840-- | Matrix pretty printer
861−prettyPrint :: (CountableDimensions cols rows, Show e) => Matrix e cols rows -> IO ()
841+prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()
862prettyPrint = putStrLn . pretty
842prettyPrint = putStrLn . pretty
864-- | Zip two matrices with a given binary function
844-- | Zip two matrices with a given binary function
865zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
845zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
866−zipWithM _ Empty Empty = Empty
867zipWithM f (One a) (One b) = One (f a b)
846zipWithM f (One a) (One b) = One (f a b)
868zipWithM f (Join a b) (Join c d) = Join (zipWithM f a c) (zipWithM f b d)
847zipWithM f (Join a b) (Join c d) = Join (zipWithM f a c) (zipWithM f b d)
869zipWithM f (Fork a b) (Fork c d) = Fork (zipWithM f a c) (zipWithM f b d)
848zipWithM f (Fork a b) (Fork c d) = Fork (zipWithM f a c) (zipWithM f b d)
@@ -888,14 +867,12 @@ fromBool False = nat 0
889-- | Relational negation
868-- | Relational negation
890negateM :: Relation cols rows -> Relation cols rows
869negateM :: Relation cols rows -> Relation cols rows
891−negateM Empty = Empty
892negateM (One (Nat p)) = One (Nat (negate p))
870negateM (One (Nat p)) = One (Nat (negate p))
893negateM (Join a b) = Join (negateM a) (negateM b)
871negateM (Join a b) = Join (negateM a) (negateM b)
894negateM (Fork a b) = Fork (negateM a) (negateM b)
872negateM (Fork a b) = Fork (negateM a) (negateM b)
896-- | Relational addition
874-- | Relational addition
897orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
875orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
898−orM Empty Empty = Empty
899orM (One a) (One b) = One (fromBool (toBool a || toBool b))
876orM (One a) (One b) = One (fromBool (toBool a || toBool b))
900orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
877orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
901orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
878orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
@@ -904,7 +881,6 @@ orM x@(Join _ _) y@(Fork _ _) = orM (abideJF x) y
905-- | Relational multiplication
882-- | Relational multiplication
906andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
883andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
907−andM Empty Empty = Empty
908andM (One a) (One b) = One (fromBool (toBool a && toBool b))
884andM (One a) (One b) = One (fromBool (toBool a && toBool b))
909andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
885andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
910andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
886andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
@@ -913,7 +889,6 @@ andM x@(Join _ _) y@(Fork _ _) = andM (abideJF x) y
914-- | Relational subtraction
890-- | Relational subtraction
915subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
891subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
916−subM Empty Empty = Empty
917subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
892subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
918subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
893subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
919subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
894subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
@@ -922,7 +897,6 @@ subM x@(Join _ _) y@(Fork _ _) = subM (abideJF x) y
923-- | Matrix relational composition.
898-- | Matrix relational composition.
924compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
899compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
925−compRel Empty Empty = Empty
926compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
900compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
927compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
901compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
928compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
902compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
@@ -930,7 +904,6 @@ compRel c (Join a b) = Join (compRel c a) (compRel c b) -- Join fusion
931-- | Matrix relational right division
905-- | Matrix relational right division
932divR :: Relation b c -> Relation b a -> Relation a c
906divR :: Relation b c -> Relation b a -> Relation a c
933−divR Empty Empty = Empty
934divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
907divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
935divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
908divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
936divR (Fork a b) c = Fork (divR a c) (divR b c)
909divR (Fork a b) c = Fork (divR a c) (divR b c)
@@ -953,58 +926,24 @@ divS s r = divL r s `intersection` divR (tr r) (tr s)
953fromFRel' ::
926fromFRel' ::
954 forall a b cols rows.
927 forall a b cols rows.
955 ( Liftable Boolean a b,
928 ( Liftable Boolean a b,
956− CountableDimensions cols rows,
929+ CountableDims cols rows,
957− FromLists Boolean rows cols
930+ FL rows cols
959 (a -> b) ->
932 (a -> b) ->
960 Relation cols rows
933 Relation cols rows
961−fromFRel' f =
934+fromFRel' = fromF'
962− let minA = minBound @a
966− ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
967− rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
968− elementsA = take ccols [minA .. maxA]
969− elementsB = take rrows [minB .. maxB]
970− combinations = (,) <$> elementsA <*> elementsB
971− combAp = map snd . sort . map (\(a, b) -> if f a == b
972− then ((fromEnum a, fromEnum b), nat 1)
973− else ((fromEnum a, fromEnum b), nat 0)) $ combinations
974− mList = buildList combAp rrows
975− in tr $ fromLists mList
978− buildList l r = take r l : buildList (drop r l) r
980-- | Lifts functions to relations with dimensions matching @a@ and @b@
936-- | Lifts functions to relations with dimensions matching @a@ and @b@
981-- cardinality's.
937-- cardinality's.
982fromFRel ::
938fromFRel ::
983 forall a b.
939 forall a b.
984 ( Liftable Boolean a b,
940 ( Liftable Boolean a b,
985− CountableDimensionsN a b,
941+ CountableDimsN a b,
986− FromLists Boolean (Normalize b) (Normalize a)
942+ FLN b a
988 (a -> b) ->
944 (a -> b) ->
989 Relation (Normalize a) (Normalize b)
945 Relation (Normalize a) (Normalize b)
990−fromFRel f =
946+fromFRel = fromFRel'
991− let minA = minBound @a
995− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
996− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
997− elementsA = take ccols [minA .. maxA]
998− elementsB = take rrows [minB .. maxB]
999− combinations = (,) <$> elementsA <*> elementsB
1000− combAp = map snd . sort . map (\(a, b) -> if f a == b
1001− then ((fromEnum a, fromEnum b), nat 1)
1002− else ((fromEnum a, fromEnum b), nat 0)) $ combinations
1003− mList = buildList combAp rrows
1004− in tr $ fromLists mList
1006− buildList [] _ = []
1007− buildList l r = take r l : buildList (drop r l) r
1009-- | Lifts a relation function to a Boolean Matrix
948-- | Lifts a relation function to a Boolean Matrix
@@ -1014,17 +953,17 @@ toRel ::
1017− CountableDimensionsN a b,
956+ CountableDims a b,
1018− FromListsN Boolean b a
957+ FLN b a
1020 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
959 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
1021toRel f =
960toRel f =
1022 let minA = minBound @a
961 let minA = minBound @a
1023 maxA = maxBound @a
962 maxA = maxBound @a
1024 minB = minBound @b
963 minB = minBound @b
1025 maxB = maxBound @b
964 maxB = maxBound @b
1026− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
965+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count a))
1027− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
966+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count b))
1028 elementsA = take ccols [minA .. maxA]
967 elementsA = take ccols [minA .. maxA]
1029 elementsB = take rrows [minB .. maxB]
968 elementsB = take rrows [minB .. maxB]
1030 combinations = (,) <$> elementsA <*> elementsB
969 combinations = (,) <$> elementsA <*> elementsB