@@ -30,7 +30,7 @@
3030-- motivation behind the library, the underlying theory, and implementation details.
3131--
3232-- This module offers many of the combinators mentioned in the work of
33−-- Macedo (2012) and Oliveira (2012).
33+-- Macedo (2012) and Oliveira (2012).
3434--
3535-- This is an Internal module and it is no supposed to be imported.
3636--
@@ -43,14 +43,23 @@ module LAoP.Matrix.Internal
4343 --
4444 -- There exists two type families that make it easier to write
4545 -- matrix dimensions: 'FromNat' and 'Count'. This approach
46− -- leads to a very straightforward implementation
47− -- of LAoP combinators.
46+ -- leads to a very straightforward implementation
47+ -- of LAoP combinators.
4848
4949 -- * Type safe matrix representation
5050 Matrix (..),
5151
52+ -- * Constraint type aliases
53+ Countable,
54+ CountableDims,
55+ CountableN,
56+ CountableDimsN,
57+ FL,
58+ FLN,
59+ Liftable,
60+ Trivial,
61+
5262 -- * Primitives
53− empty,
5463 one,
5564 join,
5665 fork,
@@ -66,6 +75,7 @@ module LAoP.Matrix.Internal
6675 toLists,
6776 toList,
6877 matrixBuilder,
78+ matrixBuilder',
6979 row,
7080 col,
7181 zeros,
@@ -76,7 +86,9 @@ module LAoP.Matrix.Internal
7686 -- * Misc
7787 -- ** Get dimensions
7888 columns,
89+ columns',
7990 rows,
91+ rows',
8092
8193 -- ** Matrix Transposition
8294 tr,
@@ -118,6 +130,7 @@ module LAoP.Matrix.Internal
118130
119131 -- | Note that given the restrictions imposed it is not possible to
120132 -- implement the standard type classes present in standard Haskell.
133+
121134 -- *** Matrix pairing projections
122135 fstM,
123136 sndM,
@@ -163,17 +176,17 @@ import Data.Kind
163176import Data.List
164177import Data.Maybe
165178import Data.Proxy
179+import Data.Typeable
166180import Data.Void
167181import GHC.TypeLits
168182import Data.Type.Equality
169183import GHC.Generics
170184import Control.DeepSeq
171−import Control.Category
172−import Prelude hiding ((.))
185+import Prelude hiding (id, (.))
186+import qualified Prelude (id, (.))
173187
174188-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
175189data Matrix e cols rows where
176− Empty :: Matrix e Void Void
177190 One :: e -> Matrix e () ()
178191 Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
179192 Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
@@ -203,7 +216,6 @@ type family Count (d :: Type) :: Nat where
203216--
204217-- Thanks to Li-Yao Xia this type family is super fast.
205218type family FromNat (n :: Nat) :: Type where
206− FromNat 0 = Void
207219 FromNat 1 = ()
208220 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
209221
@@ -220,29 +232,26 @@ type family Normalize (d :: Type) :: Type where
220232-- | Constraint type synonyms to keep the type signatures less convoluted
221233type Countable a = KnownNat (Count a)
222234type CountableN a = KnownNat (Count (Normalize a))
223−type CountableDimensions a b = (Countable a, Countable b)
224−type CountableDimensionsN a b = (CountableN a, CountableN b)
225−type FromListsN e a b = FromLists e (Normalize a) (Normalize b)
235+type CountableDims a b = (Countable a, Countable b)
236+type CountableDimsN a b = (CountableN a, CountableN b)
237+type FL a b = FromLists a b
238+type FLN a b = FromLists (Normalize a) (Normalize b)
226239type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
227240type Trivial a = FromNat (Count a) ~ a
228241
229−-- | It isn't possible to implement the 'id' function so it's
230−-- implementation is 'undefined'. However 'comp' can be and this partial
231−-- class implementation exists just to make the code more readable.
232−--
233−-- Please use 'iden' instead.
242+-- | It is possible to implement a constrained version of the category type
243+-- class.
234244instance (Num e) => Category (Matrix e) where
235− id = undefined
236− (.) = comp
245+ type Object (Matrix e) a = (FL a a, Countable a)
246+ id = iden
247+ (.) = comp
237248
238249instance NFData e => NFData (Matrix e cols rows) where
239− rnf Empty = ()
240250 rnf (One e) = rnf e
241251 rnf (Join a b) = rnf a `seq` rnf b
242252 rnf (Fork a b) = rnf a `seq` rnf b
243253
244254instance Eq e => Eq (Matrix e cols rows) where
245− Empty == Empty = True
246255 (One a) == (One b) = a == b
247256 (Join a b) == (Join c d) = a == c && b == d
248257 (Fork a b) == (Fork c d) = a == c && b == d
@@ -250,25 +259,21 @@ instance Eq e => Eq (Matrix e cols rows) where
250259 x@(Join _ _) == y@(Fork _ _) = abideJF x == y
251260
252261instance Num e => Num (Matrix e cols rows) where
253−
254262 a + b = zipWithM (+) a b
255263
256264 a - b = zipWithM (-) a b
257265
258266 a * b = zipWithM (*) a b
259267
260− abs Empty = Empty
261268 abs (One a) = One (abs a)
262269 abs (Join a b) = Join (abs a) (abs b)
263270 abs (Fork a b) = Fork (abs a) (abs b)
264271
265− signum Empty = Empty
266272 signum (One a) = One (signum a)
267273 signum (Join a b) = Join (signum a) (signum b)
268274 signum (Fork a b) = Fork (signum a) (signum b)
269275
270276instance Ord e => Ord (Matrix e cols rows) where
271− Empty <= Empty = True
272277 (One a) <= (One b) = a <= b
273278 (Join a b) <= (Join c d) = (a <= c) && (b <= d)
274279 (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
@@ -277,10 +282,6 @@ instance Ord e => Ord (Matrix e cols rows) where
277282
278283-- Primitives
279284
280−-- | Empty matrix constructor
281−empty :: Matrix e Void Void
282−empty = Empty
283−
284285-- | Unit matrix constructor
285286one :: e -> Matrix e () ()
286287one = One
@@ -311,40 +312,39 @@ infixl 2 ===
311312--
312313-- Given that it is not possible to branch on types at the term level type
313314-- classes are needed very much like an inductive definition but on types.
314−class FromLists e cols rows where
315+class FromLists cols rows where
315316 -- | Build a matrix out of a list of list of elements. Throws a runtime
316317 -- error if the dimensions do not match.
317318 fromLists :: [[e]] -> Matrix e cols rows
318319
319−instance FromLists e Void Void where
320− fromLists [] = Empty
321− fromLists _ = error "Wrong dimensions"
322−
323−instance {-# OVERLAPPING #-} FromLists e () () where
320+instance FromLists () () where
324321 fromLists [[e]] = One e
325322 fromLists _ = error "Wrong dimensions"
326323
327−instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
324+instance (FromLists cols ()) => FromLists (Either () cols) () where
328325 fromLists [h : t] = Join (One h) (fromLists [t])
329326 fromLists _ = error "Wrong dimensions"
330327
331−instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), Countable a) => FromLists e (Either a b) () where
328+instance {-# OVERLAPPABLE #-}
329+ (FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () where
332330 fromLists [l] =
333331 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
334332 in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
335333 fromLists _ = error "Wrong dimensions"
336334
337−instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
335+instance (FromLists () rows) => FromLists () (Either () rows) where
338336 fromLists ([h] : t) = Fork (One h) (fromLists t)
339337 fromLists _ = error "Wrong dimensions"
340338
341−instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, Countable a) => FromLists e () (Either a b) where
342− fromLists l@([_] : _) =
339+instance {-# OVERLAPPABLE #-}
340+ (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where
341+ fromLists l@([_] : _) =
343342 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
344343 in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
345344 fromLists _ = error "Wrong dimensions"
346345
347−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
348348 fromLists l@(h : t) =
349349 let lh = length h
350350 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
@@ -354,24 +354,44 @@ instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a
354354 else error "Not all rows have the same length"
355355
356356-- | Matrix builder function. Constructs a matrix provided with
357−-- a construction function.
358−matrixBuilder ::
357+-- a construction function that operates with indices.
358+matrixBuilder' ::
359359 forall e cols rows.
360− ( FromLists e cols rows,
361− CountableDimensions cols rows
360+ ( FL cols rows,
361+ CountableDims cols rows
362362 ) => ((Int, Int) -> e) -> Matrix e cols rows
363−matrixBuilder f =
363+matrixBuilder' f =
364364 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
365365 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
366366 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
367367 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
368368
369+-- | Matrix builder function. Constructs a matrix provided with
370+-- a construction function that operates with arbitrary types.
371+matrixBuilder ::
372+ forall e a b.
373+ ( FLN a b,
374+ Enum a,
375+ Enum b,
376+ Bounded a,
377+ Bounded b,
378+ Eq a,
379+ Countable b
380+ ) => ((a, b) -> e) -> Matrix e (Normalize a) (Normalize b)
381+matrixBuilder f =
382+ let r = fromInteger $ natVal (Proxy :: Proxy (Count b))
383+ positions = [(a, b) | a <- [minBound .. maxBound], b <- [minBound .. maxBound]]
384+ in fromLists . map (map f) . transpose . buildList r $ positions
385+ where
386+ buildList _ [] = []
387+ buildList r l = take r l : buildList r (drop r l)
388+
369389-- | Constructs a column vector matrix
370−col :: (FromLists e () rows) => [e] -> Matrix e () rows
390+col :: (FL () rows) => [e] -> Matrix e () rows
371391col = fromLists . map (: [])
372392
373393-- | Constructs a row vector matrix
374−row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
394+row :: (FL cols ()) => [e] -> Matrix e cols ()
375395row = fromLists . (: [])
376396
377397-- | Lifts functions to matrices with arbitrary dimensions.
@@ -381,8 +401,8 @@ row = fromLists . (: [])
381401fromF' ::
382402 forall a b cols rows e.
383403 ( Liftable e a b,
384− CountableDimensions cols rows,
385− FromLists e rows cols
404+ CountableDims cols rows,
405+ FL rows cols
386406 ) =>
387407 (a -> b) ->
388408 Matrix e cols rows
@@ -410,35 +430,17 @@ fromF' f =
410430fromF ::
411431 forall a b e.
412432 ( Liftable e a b,
413− CountableDimensionsN a b,
414− FromListsN e b a
433+ CountableDimsN a b,
434+ FLN b a
415435 ) =>
416436 (a -> b) ->
417437 Matrix e (Normalize a) (Normalize b)
418−fromF f =
419− let minA = minBound @a
420− maxA = maxBound @a
421− minB = minBound @b
422− maxB = maxBound @b
423− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
424− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
425− elementsA = take ccols [minA .. maxA]
426− elementsB = take rrows [minB .. maxB]
427− combinations = (,) <$> elementsA <*> elementsB
428− combAp = map snd . sort . map (\(a, b) -> if f a == b
429− then ((fromEnum a, fromEnum b), 1)
430− else ((fromEnum a, fromEnum b), 0)) $ combinations
431− mList = buildList combAp rrows
432− in tr $ fromLists mList
433− where
434− buildList [] _ = []
435− buildList l r = take r l : buildList (drop r l) r
438+fromF = fromF'
436439
437440-- Conversion
438441
439442-- | Converts a matrix to a list of lists of elements.
440443toLists :: Matrix e cols rows -> [[e]]
441−toLists Empty = []
442444toLists (One e) = [[e]]
443445toLists (Fork l r) = toLists l ++ toLists r
444446toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
@@ -450,28 +452,28 @@ toList = concat . toLists
450452-- Zeros Matrix
451453
452454-- | The zero matrix. A matrix wholly filled with zeros.
453−zeros :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows
454−zeros = matrixBuilder (const 0)
455+zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
456+zeros = matrixBuilder' (const 0)
455457
456458-- Ones Matrix
457459
458460-- | The ones matrix. A matrix wholly filled with ones.
459461--
460462-- Also known as T (Top) matrix.
461−ones :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows
462−ones = matrixBuilder (const 1)
463+ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
464+ones = matrixBuilder' (const 1)
463465
464466-- Const Matrix
465467
466468-- | The constant matrix constructor. A matrix wholly filled with a given
467469-- value.
468−constant :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => e -> Matrix e cols rows
469−constant e = matrixBuilder (const e)
470+constant :: (Num e, FL cols rows, CountableDims cols rows) => e -> Matrix e cols rows
471+constant e = matrixBuilder' (const e)
470472
471473-- Bang Matrix
472474
473475-- | The T (Top) row vector matrix.
474−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 ()
475477bang =
476478 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
477479 in fromLists [take c [1, 1 ..]]
@@ -479,8 +481,8 @@ bang =
479481-- iden Matrix
480482
481483-- | iden matrix.
482−iden :: (Num e, FromLists e cols cols, Countable cols) => Matrix e cols cols
483−iden = matrixBuilder (bool 0 1 . uncurry (==))
484+iden :: forall e cols . (Num e, FL cols cols, Countable cols) => Matrix e cols cols
485+iden = matrixBuilder' (bool 0 1 . uncurry (==))
484486{-# NOINLINE iden #-}
485487
486488-- Matrix composition (MMM)
@@ -490,13 +492,12 @@ iden = matrixBuilder (bool 0 1 . uncurry (==))
490492-- This definition takes advantage of divide-and-conquer and fusion laws
491493-- from LAoP.
492494comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
493−comp Empty Empty = Empty
494495comp (One a) (One b) = One (a * b)
495496comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
496497comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
497498comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
498499{-# NOINLINE comp #-}
499−{-# RULES
500+{-# RULES
500501 "comp/iden1" forall m. comp m iden = m ;
501502 "comp/iden2" forall m. comp iden m = m
502503#-}
@@ -506,7 +507,6 @@ comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
506507infixl 7 .|
507508-- | Scalar multiplication of matrices.
508509(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
509−(.|) _ Empty = Empty
510510(.|) e (One a) = One (e * a)
511511(.|) e (Join a b) = Join (e .| a) (e .| b)
512512(.|) e (Fork a b) = Fork (e .| a) (e .| b)
@@ -516,7 +516,6 @@ infixl 7 .|
516516infixl 7 ./
517517-- | Scalar multiplication of matrices.
518518(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
519−(./) Empty _ = Empty
520519(./) (One a) e = One (a / e)
521520(./) (Join a b) e = Join (a ./ e) (b ./ e)
522521(./) (Fork a b) e = Fork (a ./ e) (b ./ e)
@@ -524,51 +523,59 @@ infixl 7 ./
524523-- Projections
525524
526525-- | Biproduct first component projection
527−p1 :: forall e m n. (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e (Either m n) m
528−p1 =
529− let iden = iden :: Matrix e m m
530− zero = zeros :: Matrix e n m
531− in join iden zero
526+p1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e (Either m n) m
527+p1 = join id zeros
532528
533529-- | Biproduct second component projection
534−p2 :: forall e m n. (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e (Either m n) n
535−p2 =
536− let iden = iden :: Matrix e n n
537− zero = zeros :: Matrix e m n
538− in join zero iden
530+p2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e (Either m n) n
531+p2 = join zeros id
539532
540533-- Injections
541534
542535-- | Biproduct first component injection
543−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)
544537i1 = tr p1
545538
546539-- | Biproduct second component injection
547−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)
548541i2 = tr p2
549542
550543-- Dimensions
551544
552545-- | Obtain the number of rows.
553546--
554−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
555−-- dimensions in constant time.
556−--
557−-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
558−-- exchange for performance.
547+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
548+-- dimensions in constant time. For a version that doesn't require the
549+-- constraint see 'rows''.
559550rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
560551rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
561552
553+-- | Obtain the number of rows in an inefficient manner, but without any
554+-- constraints.
555+--
556+-- For a more efficient version see 'rows'.
557+rows' :: Matrix e cols rows -> Int
558+rows' (One _) = 1
559+rows' (Join lhs _) = rows' lhs
560+rows' (Fork top bottom) = rows' top + rows' bottom
561+
562562-- | Obtain the number of columns.
563−--
564−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
565−-- dimensions in constant time.
566563--
567−-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
568−-- exchange for performance.
564+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
565+-- dimensions in constant time. For a version that doesn't require the
566+-- constraint see 'columns''.
569567columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
570568columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
571569
570+-- | Obtain the number of columns in an inefficient manner, but without any
571+-- constraints.
572+--
573+-- For a more efficient version see 'columns'.
574+columns' :: Matrix e cols rows -> Int
575+columns' (One _) = 1
576+columns' (Join lhs rhs) = columns' lhs + columns' rhs
577+columns' (Fork top _) = columns' top
578+
572579-- Coproduct Bifunctor
573580
574581infixl 5 -|-
@@ -577,11 +584,11 @@ infixl 5 -|-
577584(-|-) ::
578585 forall e n k m j.
579586 ( Num e,
580− CountableDimensions j k,
581− FromLists e k k,
582− FromLists e j k,
583− FromLists e k j,
584− FromLists e j j
587+ CountableDims j k,
588+ FL k k,
589+ FL j k,
590+ FL k j,
591+ FL j j
585592 ) =>
586593 Matrix e n k ->
587594 Matrix e m j ->
@@ -594,11 +601,11 @@ infixl 5 -|-
594601fstM ::
595602 forall e m k .
596603 ( Num e,
597− CountableDimensions k m,
598− FromLists e (Normalize (m, k)) m,
604+ CountableDims k m,
605+ FL (Normalize (m, k)) m,
599606 CountableN (m, k)
600607 ) => Matrix e (Normalize (m, k)) m
601−fstM = matrixBuilder f
608+fstM = matrixBuilder' f
602609 where
603610 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
604611 f (x, y)
@@ -609,11 +616,11 @@ fstM = matrixBuilder f
609616sndM ::
610617 forall e m k .
611618 ( Num e,
612− CountableDimensions k m,
613− FromLists e (Normalize (m, k)) k,
619+ CountableDims k m,
620+ FL (Normalize (m, k)) k,
614621 CountableN (m, k)
615622 ) => Matrix e (Normalize (m, k)) k
616−sndM = matrixBuilder f
623+sndM = matrixBuilder' f
617624 where
618625 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
619626 f (x, y)
@@ -623,7 +630,7 @@ sndM = matrixBuilder f
623630-- | Khatri Rao Matrix product also known as matrix pairing.
624631--
625632-- NOTE: That this is not a true categorical product, see for instance:
626−--
633+--
627634-- @
628635-- | fstM . kr a b == a
629636-- kr a b ==> |
@@ -634,15 +641,15 @@ sndM = matrixBuilder f
634641kr ::
635642 forall e cols a b.
636643 ( Num e,
637− CountableDimensions a b,
644+ CountableDims a b,
638645 CountableN (a, b),
639− FromLists e (Normalize (a, b)) a,
640− FromLists e (Normalize (a, b)) b
646+ FL (Normalize (a, b)) a,
647+ FL (Normalize (a, b)) b
641648 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
642649kr a b =
643650 let fstM' = fstM @e @a @b
644651 sndM' = sndM @e @a @b
645− in tr fstM' . a * tr sndM' . b
652+ in (tr fstM' . a) * (tr sndM' . b)
646653
647654-- Product Bifunctor (Kronecker)
648655
@@ -652,14 +659,14 @@ infixl 4 ><
652659(><) ::
653660 forall e m p n q.
654661 ( Num e,
655− CountableDimensions m n,
656− CountableDimensions p q,
657− CountableDimensionsN (m, n) (p, q),
658− FromLists e (Normalize (m, n)) m,
659− FromLists e (Normalize (m, n)) n,
660− FromLists e (Normalize (p, q)) p,
661− FromLists e (Normalize (p, q)) q
662− )
662+ CountableDims m n,
663+ CountableDims p q,
664+ CountableDimsN (m, n) (p, q),
665+ FL (Normalize (m, n)) m,
666+ FL (Normalize (m, n)) n,
667+ FL (Normalize (p, q)) p,
668+ FL (Normalize (p, q)) q
669+ )
663670 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
664671(><) a b =
665672 let fstM' = fstM @e @m @n
@@ -677,7 +684,6 @@ infixl 4 ><
677684-- @
678685abideJF :: Matrix e cols rows -> Matrix e cols rows
679686abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
680−abideJF Empty = Empty
681687abideJF (One e) = One e
682688abideJF (Join a b) = Join (abideJF a) (abideJF b)
683689abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
@@ -691,7 +697,6 @@ abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
691697-- @
692698abideFJ :: Matrix e cols rows -> Matrix e cols rows
693699abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law
694−abideFJ Empty = Empty
695700abideFJ (One e) = One e
696701abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
697702abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
@@ -700,7 +705,6 @@ abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
700705
701706-- | Matrix transposition.
702707tr :: Matrix e cols rows -> Matrix e rows cols
703−tr Empty = Empty
704708tr (One e) = One e
705709tr (Join a b) = Fork (tr a) (tr b)
706710tr (Fork a b) = Join (tr a) (tr b)
@@ -709,32 +713,32 @@ tr (Fork a b) = Join (tr a) (tr b)
709713
710714-- | Selective functors 'select' operator equivalent inspired by the
711715-- ArrowMonad solution presented in the paper.
712−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
713717select (Fork a b) y = y . a + b -- Divide-and-conquer law
714718select (Join (Fork a c) (Fork b d)) y = join (y . a + c) (y . b + d) -- Pattern matching + DnC law
715−select m y = join y iden . m
719+select m y = join y id . m
716720
717721branch ::
718722 ( Num e,
719− CountableDimensions a b,
720− CountableDimensions c (Either b c),
721− FromLists e c b,
722− FromLists e a b,
723− FromLists e a a,
724− FromLists e b b,
725− FromLists e c c,
726− FromLists e b a,
727− FromLists e b c,
728− FromLists e (Either b c) b,
729− FromLists e (Either b c) c
723+ CountableDims a b,
724+ CountableDims c (Either b c),
725+ FL c b,
726+ FL a b,
727+ FL a a,
728+ FL b b,
729+ FL c c,
730+ FL b a,
731+ FL b c,
732+ FL (Either b c) b,
733+ FL (Either b c) c
730734 )
731735 => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c
732736branch x l r = f x `select` g l `select` r
733737 where
734− 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)
735739 => Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
736740 f m = fork (tr i1) (i1 . tr i2) . m
737− 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)
738742 g m = i2 . m
739743
740744-- McCarthy's Conditional
@@ -743,9 +747,9 @@ branch x l r = f x `select` g l `select` r
743747cond ::
744748 ( Trivial cols,
745749 Countable cols,
746− FromLists e () cols,
747− FromLists e cols (),
748− FromLists e cols cols,
750+ FL () cols,
751+ FL cols (),
752+ FL cols cols,
749753 Bounded a,
750754 Enum a,
751755 Num e,
@@ -758,9 +762,9 @@ cond p f g = join f g . grd p
758762grd ::
759763 ( Trivial q,
760764 Countable q,
761− FromLists e () q,
762− FromLists e q (),
763− FromLists e q q,
765+ FL () q,
766+ FL q (),
767+ FL q q,
764768 Bounded a,
765769 Enum a,
766770 Num e,
@@ -774,14 +778,14 @@ corr ::
774778 forall e a q .
775779 ( Trivial q,
776780 Countable q,
777− FromLists e () q,
778− FromLists e q (),
779− FromLists e q q,
781+ FL () q,
782+ FL q (),
783+ FL q q,
780784 Liftable e a Bool
781785 )
782786 => (a -> Bool) -> Matrix e q q
783787corr p = let f = fromF' p :: Matrix e q ()
784− in kr f (iden :: Matrix e q q)
788+ in kr f (id :: Matrix e q q)
785789
786790-- Pretty print
787791
@@ -805,7 +809,7 @@ prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
805809 fill str = replicate (widest - length str - 2) ' ' ++ str
806810
807811-- | Matrix pretty printer
808−pretty :: (CountableDimensions cols rows, Show e) => Matrix e cols rows -> String
812+pretty :: (CountableDims cols rows, Show e) => Matrix e cols rows -> String
809813pretty m = concat
810814 [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"
811815 , unlines
@@ -834,12 +838,11 @@ pretty m = concat
834838 (safeGet i j m)
835839
836840-- | Matrix pretty printer
837−prettyPrint :: (CountableDimensions cols rows, Show e) => Matrix e cols rows -> IO ()
841+prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()
838842prettyPrint = putStrLn . pretty
839843
840844-- | Zip two matrices with a given binary function
841845zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
842−zipWithM _ Empty Empty = Empty
843846zipWithM f (One a) (One b) = One (f a b)
844847zipWithM f (Join a b) (Join c d) = Join (zipWithM f a c) (zipWithM f b d)
845848zipWithM f (Fork a b) (Fork c d) = Fork (zipWithM f a c) (zipWithM f b d)
@@ -864,14 +867,12 @@ fromBool False = nat 0
864867
865868-- | Relational negation
866869negateM :: Relation cols rows -> Relation cols rows
867−negateM Empty = Empty
868870negateM (One (Nat p)) = One (Nat (negate p))
869871negateM (Join a b) = Join (negateM a) (negateM b)
870872negateM (Fork a b) = Fork (negateM a) (negateM b)
871873
872874-- | Relational addition
873875orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
874−orM Empty Empty = Empty
875876orM (One a) (One b) = One (fromBool (toBool a || toBool b))
876877orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
877878orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
@@ -880,7 +881,6 @@ orM x@(Join _ _) y@(Fork _ _) = orM (abideJF x) y
880881
881882-- | Relational multiplication
882883andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
883−andM Empty Empty = Empty
884884andM (One a) (One b) = One (fromBool (toBool a && toBool b))
885885andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
886886andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
@@ -889,7 +889,6 @@ andM x@(Join _ _) y@(Fork _ _) = andM (abideJF x) y
889889
890890-- | Relational subtraction
891891subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
892−subM Empty Empty = Empty
893892subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
894893subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
895894subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
@@ -898,7 +897,6 @@ subM x@(Join _ _) y@(Fork _ _) = subM (abideJF x) y
898897
899898-- | Matrix relational composition.
900899compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
901−compRel Empty Empty = Empty
902900compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
903901compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
904902compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
@@ -906,7 +904,6 @@ compRel c (Join a b) = Join (compRel c a) (compRel c b) -- Join fusion
906904
907905-- | Matrix relational right division
908906divR :: Relation b c -> Relation b a -> Relation a c
909−divR Empty Empty = Empty
910907divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
911908divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
912909divR (Fork a b) c = Fork (divR a c) (divR b c)
@@ -929,58 +926,24 @@ divS s r = divL r s `intersection` divR (tr r) (tr s)
929926fromFRel' ::
930927 forall a b cols rows.
931928 ( Liftable Boolean a b,
932− CountableDimensions cols rows,
933− FromLists Boolean rows cols
929+ CountableDims cols rows,
930+ FL rows cols
934931 ) =>
935932 (a -> b) ->
936933 Relation cols rows
937−fromFRel' f =
938− let minA = minBound @a
939− maxA = maxBound @a
940− minB = minBound @b
941− maxB = maxBound @b
942− ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
943− rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
944− elementsA = take ccols [minA .. maxA]
945− elementsB = take rrows [minB .. maxB]
946− combinations = (,) <$> elementsA <*> elementsB
947− combAp = map snd . sort . map (\(a, b) -> if f a == b
948− then ((fromEnum a, fromEnum b), nat 1)
949− else ((fromEnum a, fromEnum b), nat 0)) $ combinations
950− mList = buildList combAp rrows
951− in tr $ fromLists mList
952− where
953− buildList [] _ = []
954− buildList l r = take r l : buildList (drop r l) r
934+fromFRel' = fromF'
955935
956936-- | Lifts functions to relations with dimensions matching @a@ and @b@
957937-- cardinality's.
958938fromFRel ::
959939 forall a b.
960940 ( Liftable Boolean a b,
961− CountableDimensionsN a b,
962− FromLists Boolean (Normalize b) (Normalize a)
941+ CountableDimsN a b,
942+ FLN b a
963943 ) =>
964944 (a -> b) ->
965945 Relation (Normalize a) (Normalize b)
966−fromFRel f =
967− let minA = minBound @a
968− maxA = maxBound @a
969− minB = minBound @b
970− maxB = maxBound @b
971− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
972− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
973− elementsA = take ccols [minA .. maxA]
974− elementsB = take rrows [minB .. maxB]
975− combinations = (,) <$> elementsA <*> elementsB
976− combAp = map snd . sort . map (\(a, b) -> if f a == b
977− then ((fromEnum a, fromEnum b), nat 1)
978− else ((fromEnum a, fromEnum b), nat 0)) $ combinations
979− mList = buildList combAp rrows
980− in tr $ fromLists mList
981− where
982− buildList [] _ = []
983− buildList l r = take r l : buildList (drop r l) r
946+fromFRel = fromFRel'
984947
985948-- | Lifts a relation function to a Boolean Matrix
986949toRel ::
@@ -990,17 +953,17 @@ toRel ::
990953 Enum a,
991954 Enum b,
992955 Eq b,
993− CountableDimensionsN a b,
994− FromListsN Boolean b a
995− )
956+ CountableDims a b,
957+ FLN b a
958+ )
996959 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
997960toRel f =
998961 let minA = minBound @a
999962 maxA = maxBound @a
1000963 minB = minBound @b
1001964 maxB = maxBound @b
1002− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
1003− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
965+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count a))
966+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count b))
1004967 elementsA = take ccols [minA .. maxA]
1005968 elementsB = take rrows [minB .. maxB]
1006969 combinations = (,) <$> elementsA <*> elementsB