@@ -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,23 +43,14 @@ 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−
6252 -- * Primitives
53+ empty,
6354 one,
6455 join,
6556 fork,
@@ -75,7 +66,6 @@ module LAoP.Matrix.Internal
7566 toLists,
7667 toList,
7768 matrixBuilder,
78− matrixBuilder',
7969 row,
8070 col,
8171 zeros,
@@ -86,17 +76,11 @@ module LAoP.Matrix.Internal
8676 -- * Misc
8777 -- ** Get dimensions
8878 columns,
89− columns',
9079 rows,
91− rows',
9280
9381 -- ** Matrix Transposition
9482 tr,
9583
96− -- ** Scalar multiplication/division of matrices
97− (.|),
98− (./),
99−
10084 -- ** Selective operator
10185 select,
10286 branch,
@@ -130,7 +114,6 @@ module LAoP.Matrix.Internal
130114
131115 -- | Note that given the restrictions imposed it is not possible to
132116 -- implement the standard type classes present in standard Haskell.
133−
134117 -- *** Matrix pairing projections
135118 fstM,
136119 sndM,
@@ -176,17 +159,17 @@ import Data.Kind
176159import Data.List
177160import Data.Maybe
178161import Data.Proxy
179−import Data.Typeable
180162import Data.Void
181163import GHC.TypeLits
182164import Data.Type.Equality
183165import GHC.Generics
184166import Control.DeepSeq
185−import Prelude hiding (id, (.))
186−import qualified Prelude (id, (.))
167+import Control.Category
168+import Prelude hiding ((.))
187169
188170-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
189171data Matrix e cols rows where
172+ Empty :: Matrix e Void Void
190173 One :: e -> Matrix e () ()
191174 Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
192175 Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
@@ -216,6 +199,7 @@ type family Count (d :: Type) :: Nat where
216199--
217200-- Thanks to Li-Yao Xia this type family is super fast.
218201type family FromNat (n :: Nat) :: Type where
202+ FromNat 0 = Void
219203 FromNat 1 = ()
220204 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
221205
@@ -232,26 +216,29 @@ type family Normalize (d :: Type) :: Type where
232216-- | Constraint type synonyms to keep the type signatures less convoluted
233217type Countable a = KnownNat (Count a)
234218type CountableN a = KnownNat (Count (Normalize a))
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)
219+type CountableDimensions a b = (Countable a, Countable b)
220+type CountableDimensionsN a b = (CountableN a, CountableN b)
221+type FromListsN e a b = FromLists e (Normalize a) (Normalize b)
239222type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
240223type Trivial a = FromNat (Count a) ~ a
241224
242−-- | It is possible to implement a constrained version of the category type
243−-- class.
225+-- | It isn't possible to implement the 'id' function so it's
226+-- implementation is 'undefined'. However 'comp' can be and this partial
227+-- class implementation exists just to make the code more readable.
228+--
229+-- Please use 'iden' instead.
244230instance (Num e) => Category (Matrix e) where
245− type Object (Matrix e) a = (FL a a, Countable a)
246− id = iden
247− (.) = comp
231+ id = undefined
232+ (.) = comp
248233
249234instance NFData e => NFData (Matrix e cols rows) where
235+ rnf Empty = ()
250236 rnf (One e) = rnf e
251237 rnf (Join a b) = rnf a `seq` rnf b
252238 rnf (Fork a b) = rnf a `seq` rnf b
253239
254240instance Eq e => Eq (Matrix e cols rows) where
241+ Empty == Empty = True
255242 (One a) == (One b) = a == b
256243 (Join a b) == (Join c d) = a == c && b == d
257244 (Fork a b) == (Fork c d) = a == c && b == d
@@ -259,21 +246,25 @@ instance Eq e => Eq (Matrix e cols rows) where
259246 x@(Join _ _) == y@(Fork _ _) = abideJF x == y
260247
261248instance Num e => Num (Matrix e cols rows) where
249+
262250 a + b = zipWithM (+) a b
263251
264252 a - b = zipWithM (-) a b
265253
266254 a * b = zipWithM (*) a b
267255
256+ abs Empty = Empty
268257 abs (One a) = One (abs a)
269258 abs (Join a b) = Join (abs a) (abs b)
270259 abs (Fork a b) = Fork (abs a) (abs b)
271260
261+ signum Empty = Empty
272262 signum (One a) = One (signum a)
273263 signum (Join a b) = Join (signum a) (signum b)
274264 signum (Fork a b) = Fork (signum a) (signum b)
275265
276266instance Ord e => Ord (Matrix e cols rows) where
267+ Empty <= Empty = True
277268 (One a) <= (One b) = a <= b
278269 (Join a b) <= (Join c d) = (a <= c) && (b <= d)
279270 (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
@@ -282,6 +273,10 @@ instance Ord e => Ord (Matrix e cols rows) where
282273
283274-- Primitives
284275
276+-- | Empty matrix constructor
277+empty :: Matrix e Void Void
278+empty = Empty
279+
285280-- | Unit matrix constructor
286281one :: e -> Matrix e () ()
287282one = One
@@ -312,86 +307,67 @@ infixl 2 ===
312307--
313308-- Given that it is not possible to branch on types at the term level type
314309-- classes are needed very much like an inductive definition but on types.
315−class FromLists cols rows where
310+class FromLists e cols rows where
316311 -- | Build a matrix out of a list of list of elements. Throws a runtime
317312 -- error if the dimensions do not match.
318313 fromLists :: [[e]] -> Matrix e cols rows
319314
320−instance FromLists () () where
315+instance FromLists e Void Void where
316+ fromLists [] = Empty
317+ fromLists _ = error "Wrong dimensions"
318+
319+instance {-# OVERLAPPING #-} FromLists e () () where
321320 fromLists [[e]] = One e
322321 fromLists _ = error "Wrong dimensions"
323322
324−instance (FromLists cols ()) => FromLists (Either () cols) () where
323+instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
325324 fromLists [h : t] = Join (One h) (fromLists [t])
326325 fromLists _ = error "Wrong dimensions"
327326
328−instance {-# OVERLAPPABLE #-}
329− (FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () where
327+instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), Countable a) => FromLists e (Either a b) () where
330328 fromLists [l] =
331329 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
332330 in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
333331 fromLists _ = error "Wrong dimensions"
334332
335−instance (FromLists () rows) => FromLists () (Either () rows) where
333+instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
336334 fromLists ([h] : t) = Fork (One h) (fromLists t)
337335 fromLists _ = error "Wrong dimensions"
338336
339−instance {-# OVERLAPPABLE #-}
340− (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where
341− fromLists l@([_] : _) =
337+instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, Countable a) => FromLists e () (Either a b) where
338+ fromLists l@([_] : _) =
342339 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
343340 in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
344341 fromLists _ = error "Wrong dimensions"
345342
346−instance (FromLists (Either a b) c, FromLists (Either a b) d, Countable c)
347− => FromLists (Either a b) (Either c d) where
343+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
348344 fromLists l@(h : t) =
349345 let lh = length h
350346 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
351− condition = all ((== lh) . length) t
347+ condition = all (== lh) (map length t)
352348 in if lh > 0 && condition
353349 then Fork (fromLists (take rowsC l)) (fromLists (drop rowsC l))
354350 else error "Not all rows have the same length"
355351
356352-- | Matrix builder function. Constructs a matrix provided with
357−-- a construction function that operates with indices.
358−matrixBuilder' ::
353+-- a construction function.
354+matrixBuilder ::
359355 forall e cols rows.
360− ( FL cols rows,
361− CountableDims cols rows
356+ ( FromLists e cols rows,
357+ CountableDimensions cols rows
362358 ) => ((Int, Int) -> e) -> Matrix e cols rows
363−matrixBuilder' f =
359+matrixBuilder f =
364360 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
365361 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
366362 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
367363 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
368364
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−
389365-- | Constructs a column vector matrix
390−col :: (FL () rows) => [e] -> Matrix e () rows
366+col :: (FromLists e () rows) => [e] -> Matrix e () rows
391367col = fromLists . map (: [])
392368
393369-- | Constructs a row vector matrix
394−row :: (FL cols ()) => [e] -> Matrix e cols ()
370+row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
395371row = fromLists . (: [])
396372
397373-- | Lifts functions to matrices with arbitrary dimensions.
@@ -401,8 +377,8 @@ row = fromLists . (: [])
401377fromF' ::
402378 forall a b cols rows e.
403379 ( Liftable e a b,
404− CountableDims cols rows,
405− FL rows cols
380+ CountableDimensions cols rows,
381+ FromLists e rows cols
406382 ) =>
407383 (a -> b) ->
408384 Matrix e cols rows
@@ -430,17 +406,35 @@ fromF' f =
430406fromF ::
431407 forall a b e.
432408 ( Liftable e a b,
433− CountableDimsN a b,
434− FLN b a
409+ CountableDimensionsN a b,
410+ FromListsN e b a
435411 ) =>
436412 (a -> b) ->
437413 Matrix e (Normalize a) (Normalize b)
438−fromF = fromF'
414+fromF f =
415+ let minA = minBound @a
416+ maxA = maxBound @a
417+ minB = minBound @b
418+ maxB = maxBound @b
419+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
420+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
421+ elementsA = take ccols [minA .. maxA]
422+ elementsB = take rrows [minB .. maxB]
423+ combinations = (,) <$> elementsA <*> elementsB
424+ combAp = map snd . sort . map (\(a, b) -> if f a == b
425+ then ((fromEnum a, fromEnum b), 1)
426+ else ((fromEnum a, fromEnum b), 0)) $ combinations
427+ mList = buildList combAp rrows
428+ in tr $ fromLists mList
429+ where
430+ buildList [] _ = []
431+ buildList l r = take r l : buildList (drop r l) r
439432
440433-- Conversion
441434
442435-- | Converts a matrix to a list of lists of elements.
443436toLists :: Matrix e cols rows -> [[e]]
437+toLists Empty = []
444438toLists (One e) = [[e]]
445439toLists (Fork l r) = toLists l ++ toLists r
446440toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
@@ -452,28 +446,28 @@ toList = concat . toLists
452446-- Zeros Matrix
453447
454448-- | The zero matrix. A matrix wholly filled with zeros.
455−zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
456−zeros = matrixBuilder' (const 0)
449+zeros :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows
450+zeros = matrixBuilder (const 0)
457451
458452-- Ones Matrix
459453
460454-- | The ones matrix. A matrix wholly filled with ones.
461455--
462456-- Also known as T (Top) matrix.
463−ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
464−ones = matrixBuilder' (const 1)
457+ones :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows
458+ones = matrixBuilder (const 1)
465459
466460-- Const Matrix
467461
468462-- | The constant matrix constructor. A matrix wholly filled with a given
469463-- value.
470−constant :: (Num e, FL cols rows, CountableDims cols rows) => e -> Matrix e cols rows
471−constant e = matrixBuilder' (const e)
464+constant :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => e -> Matrix e cols rows
465+constant e = matrixBuilder (const e)
472466
473467-- Bang Matrix
474468
475469-- | The T (Top) row vector matrix.
476−bang :: forall e cols. (Num e, Enum e, FL cols (), Countable cols) => Matrix e cols ()
470+bang :: forall e cols. (Num e, Enum e, FromLists e cols (), Countable cols) => Matrix e cols ()
477471bang =
478472 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
479473 in fromLists [take c [1, 1 ..]]
@@ -481,8 +475,8 @@ bang =
481475-- iden Matrix
482476
483477-- | iden matrix.
484−iden :: forall e cols . (Num e, FL cols cols, Countable cols) => Matrix e cols cols
485−iden = matrixBuilder' (bool 0 1 . uncurry (==))
478+iden :: (Num e, FromLists e cols cols, Countable cols) => Matrix e cols cols
479+iden = matrixBuilder (bool 0 1 . uncurry (==))
486480{-# NOINLINE iden #-}
487481
488482-- Matrix composition (MMM)
@@ -492,90 +486,65 @@ iden = matrixBuilder' (bool 0 1 . uncurry (==))
492486-- This definition takes advantage of divide-and-conquer and fusion laws
493487-- from LAoP.
494488comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
489+comp Empty Empty = Empty
495490comp (One a) (One b) = One (a * b)
496491comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
497492comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
498493comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
499494{-# NOINLINE comp #-}
500−{-# RULES
495+{-# RULES
501496 "comp/iden1" forall m. comp m iden = m ;
502497 "comp/iden2" forall m. comp iden m = m
503498#-}
504499
505−-- Scalar multiplication of matrices
506−
507−infixl 7 .|
508−-- | Scalar multiplication of matrices.
509−(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
510−(.|) e (One a) = One (e * a)
511−(.|) e (Join a b) = Join (e .| a) (e .| b)
512−(.|) e (Fork a b) = Fork (e .| a) (e .| b)
513−
514−-- Scalar division of matrices
515−
516−infixl 7 ./
517−-- | Scalar multiplication of matrices.
518−(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
519−(./) (One a) e = One (a / e)
520−(./) (Join a b) e = Join (a ./ e) (b ./ e)
521−(./) (Fork a b) e = Fork (a ./ e) (b ./ e)
522−
523500-- Projections
524501
525502-- | Biproduct first component projection
526−p1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e (Either m n) m
527−p1 = join id zeros
503+p1 :: forall e m n. (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e (Either m n) m
504+p1 =
505+ let iden = iden :: Matrix e m m
506+ zero = zeros :: Matrix e n m
507+ in join iden zero
528508
529509-- | Biproduct second component projection
530−p2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e (Either m n) n
531−p2 = join zeros id
510+p2 :: forall e m n. (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e (Either m n) n
511+p2 =
512+ let iden = iden :: Matrix e n n
513+ zero = zeros :: Matrix e m n
514+ in join zero iden
532515
533516-- Injections
534517
535518-- | Biproduct first component injection
536−i1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e m (Either m n)
519+i1 :: (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
537520i1 = tr p1
538521
539522-- | Biproduct second component injection
540−i2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e n (Either m n)
523+i2 :: (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
541524i2 = tr p2
542525
543526-- Dimensions
544527
545528-- | Obtain the number of rows.
546529--
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''.
530+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
531+-- dimensions in constant time.
532+--
533+-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
534+-- exchange for performance.
550535rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
551536rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
552537
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−
562538-- | Obtain the number of columns.
539+--
540+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
541+-- dimensions in constant time.
563542--
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''.
543+-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
544+-- exchange for performance.
567545columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
568546columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
569547
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−
579548-- Coproduct Bifunctor
580549
581550infixl 5 -|-
@@ -584,11 +553,11 @@ infixl 5 -|-
584553(-|-) ::
585554 forall e n k m j.
586555 ( Num e,
587− CountableDims j k,
588− FL k k,
589− FL j k,
590− FL k j,
591− FL j j
556+ CountableDimensions j k,
557+ FromLists e k k,
558+ FromLists e j k,
559+ FromLists e k j,
560+ FromLists e j j
592561 ) =>
593562 Matrix e n k ->
594563 Matrix e m j ->
@@ -601,11 +570,11 @@ infixl 5 -|-
601570fstM ::
602571 forall e m k .
603572 ( Num e,
604− CountableDims k m,
605− FL (Normalize (m, k)) m,
573+ CountableDimensions k m,
574+ FromLists e (Normalize (m, k)) m,
606575 CountableN (m, k)
607576 ) => Matrix e (Normalize (m, k)) m
608−fstM = matrixBuilder' f
577+fstM = matrixBuilder f
609578 where
610579 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
611580 f (x, y)
@@ -616,11 +585,11 @@ fstM = matrixBuilder' f
616585sndM ::
617586 forall e m k .
618587 ( Num e,
619− CountableDims k m,
620− FL (Normalize (m, k)) k,
588+ CountableDimensions k m,
589+ FromLists e (Normalize (m, k)) k,
621590 CountableN (m, k)
622591 ) => Matrix e (Normalize (m, k)) k
623−sndM = matrixBuilder' f
592+sndM = matrixBuilder f
624593 where
625594 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
626595 f (x, y)
@@ -630,7 +599,7 @@ sndM = matrixBuilder' f
630599-- | Khatri Rao Matrix product also known as matrix pairing.
631600--
632601-- NOTE: That this is not a true categorical product, see for instance:
633−--
602+--
634603-- @
635604-- | fstM . kr a b == a
636605-- kr a b ==> |
@@ -641,15 +610,15 @@ sndM = matrixBuilder' f
641610kr ::
642611 forall e cols a b.
643612 ( Num e,
644− CountableDims a b,
613+ CountableDimensions a b,
645614 CountableN (a, b),
646− FL (Normalize (a, b)) a,
647− FL (Normalize (a, b)) b
615+ FromLists e (Normalize (a, b)) a,
616+ FromLists e (Normalize (a, b)) b
648617 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
649618kr a b =
650619 let fstM' = fstM @e @a @b
651620 sndM' = sndM @e @a @b
652− in (tr fstM' . a) * (tr sndM' . b)
621+ in tr fstM' . a * tr sndM' . b
653622
654623-- Product Bifunctor (Kronecker)
655624
@@ -659,14 +628,14 @@ infixl 4 ><
659628(><) ::
660629 forall e m p n q.
661630 ( Num e,
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− )
631+ CountableDimensions m n,
632+ CountableDimensions p q,
633+ CountableDimensionsN (m, n) (p, q),
634+ FromLists e (Normalize (m, n)) m,
635+ FromLists e (Normalize (m, n)) n,
636+ FromLists e (Normalize (p, q)) p,
637+ FromLists e (Normalize (p, q)) q
638+ )
670639 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
671640(><) a b =
672641 let fstM' = fstM @e @m @n
@@ -684,6 +653,7 @@ infixl 4 ><
684653-- @
685654abideJF :: Matrix e cols rows -> Matrix e cols rows
686655abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
656+abideJF Empty = Empty
687657abideJF (One e) = One e
688658abideJF (Join a b) = Join (abideJF a) (abideJF b)
689659abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
@@ -697,6 +667,7 @@ abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
697667-- @
698668abideFJ :: Matrix e cols rows -> Matrix e cols rows
699669abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law
670+abideFJ Empty = Empty
700671abideFJ (One e) = One e
701672abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
702673abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
@@ -705,6 +676,7 @@ abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
705676
706677-- | Matrix transposition.
707678tr :: Matrix e cols rows -> Matrix e rows cols
679+tr Empty = Empty
708680tr (One e) = One e
709681tr (Join a b) = Fork (tr a) (tr b)
710682tr (Fork a b) = Join (tr a) (tr b)
@@ -713,32 +685,32 @@ tr (Fork a b) = Join (tr a) (tr b)
713685
714686-- | Selective functors 'select' operator equivalent inspired by the
715687-- ArrowMonad solution presented in the paper.
716−select :: (Num e, FL b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
688+select :: (Num e, FromLists e b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
717689select (Fork a b) y = y . a + b -- Divide-and-conquer law
718690select (Join (Fork a c) (Fork b d)) y = join (y . a + c) (y . b + d) -- Pattern matching + DnC law
719−select m y = join y id . m
691+select m y = join y iden . m
720692
721693branch ::
722694 ( Num e,
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
695+ CountableDimensions a b,
696+ CountableDimensions c (Either b c),
697+ FromLists e c b,
698+ FromLists e a b,
699+ FromLists e a a,
700+ FromLists e b b,
701+ FromLists e c c,
702+ FromLists e b a,
703+ FromLists e b c,
704+ FromLists e (Either b c) b,
705+ FromLists e (Either b c) c
734706 )
735707 => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c
736708branch x l r = f x `select` g l `select` r
737709 where
738− f :: (Num e, Countable a, CountableDims b c, FL a b, FL c b, FL b b, FL b a, FL a a)
710+ 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)
739711 => Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
740712 f m = fork (tr i1) (i1 . tr i2) . m
741− g :: (Num e, CountableDims b c, FL b c, FL c c) => Matrix e a c -> Matrix e a (Either b c)
713+ g :: (Num e, CountableDimensions b c, FromLists e b c, FromLists e c c) => Matrix e a c -> Matrix e a (Either b c)
742714 g m = i2 . m
743715
744716-- McCarthy's Conditional
@@ -747,9 +719,9 @@ branch x l r = f x `select` g l `select` r
747719cond ::
748720 ( Trivial cols,
749721 Countable cols,
750− FL () cols,
751− FL cols (),
752− FL cols cols,
722+ FromLists e () cols,
723+ FromLists e cols (),
724+ FromLists e cols cols,
753725 Bounded a,
754726 Enum a,
755727 Num e,
@@ -762,9 +734,9 @@ cond p f g = join f g . grd p
762734grd ::
763735 ( Trivial q,
764736 Countable q,
765− FL () q,
766− FL q (),
767− FL q q,
737+ FromLists e () q,
738+ FromLists e q (),
739+ FromLists e q q,
768740 Bounded a,
769741 Enum a,
770742 Num e,
@@ -778,14 +750,14 @@ corr ::
778750 forall e a q .
779751 ( Trivial q,
780752 Countable q,
781− FL () q,
782− FL q (),
783− FL q q,
753+ FromLists e () q,
754+ FromLists e q (),
755+ FromLists e q q,
784756 Liftable e a Bool
785757 )
786758 => (a -> Bool) -> Matrix e q q
787759corr p = let f = fromF' p :: Matrix e q ()
788− in kr f (id :: Matrix e q q)
760+ in kr f (iden :: Matrix e q q)
789761
790762-- Pretty print
791763
@@ -809,7 +781,7 @@ prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
809781 fill str = replicate (widest - length str - 2) ' ' ++ str
810782
811783-- | Matrix pretty printer
812−pretty :: (CountableDims cols rows, Show e) => Matrix e cols rows -> String
784+pretty :: (CountableDimensions cols rows, Show e) => Matrix e cols rows -> String
813785pretty m = concat
814786 [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"
815787 , unlines
@@ -838,11 +810,12 @@ pretty m = concat
838810 (safeGet i j m)
839811
840812-- | Matrix pretty printer
841−prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()
813+prettyPrint :: (CountableDimensions cols rows, Show e) => Matrix e cols rows -> IO ()
842814prettyPrint = putStrLn . pretty
843815
844816-- | Zip two matrices with a given binary function
845817zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
818+zipWithM _ Empty Empty = Empty
846819zipWithM f (One a) (One b) = One (f a b)
847820zipWithM f (Join a b) (Join c d) = Join (zipWithM f a c) (zipWithM f b d)
848821zipWithM f (Fork a b) (Fork c d) = Fork (zipWithM f a c) (zipWithM f b d)
@@ -867,12 +840,14 @@ fromBool False = nat 0
867840
868841-- | Relational negation
869842negateM :: Relation cols rows -> Relation cols rows
843+negateM Empty = Empty
870844negateM (One (Nat p)) = One (Nat (negate p))
871845negateM (Join a b) = Join (negateM a) (negateM b)
872846negateM (Fork a b) = Fork (negateM a) (negateM b)
873847
874848-- | Relational addition
875849orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
850+orM Empty Empty = Empty
876851orM (One a) (One b) = One (fromBool (toBool a || toBool b))
877852orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
878853orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
@@ -881,6 +856,7 @@ orM x@(Join _ _) y@(Fork _ _) = orM (abideJF x) y
881856
882857-- | Relational multiplication
883858andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
859+andM Empty Empty = Empty
884860andM (One a) (One b) = One (fromBool (toBool a && toBool b))
885861andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
886862andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
@@ -889,6 +865,7 @@ andM x@(Join _ _) y@(Fork _ _) = andM (abideJF x) y
889865
890866-- | Relational subtraction
891867subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
868+subM Empty Empty = Empty
892869subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
893870subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
894871subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
@@ -897,6 +874,7 @@ subM x@(Join _ _) y@(Fork _ _) = subM (abideJF x) y
897874
898875-- | Matrix relational composition.
899876compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
877+compRel Empty Empty = Empty
900878compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
901879compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
902880compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
@@ -904,6 +882,7 @@ compRel c (Join a b) = Join (compRel c a) (compRel c b) -- Join fusion
904882
905883-- | Matrix relational right division
906884divR :: Relation b c -> Relation b a -> Relation a c
885+divR Empty Empty = Empty
907886divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
908887divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
909888divR (Fork a b) c = Fork (divR a c) (divR b c)
@@ -926,24 +905,58 @@ divS s r = divL r s `intersection` divR (tr r) (tr s)
926905fromFRel' ::
927906 forall a b cols rows.
928907 ( Liftable Boolean a b,
929− CountableDims cols rows,
930− FL rows cols
908+ CountableDimensions cols rows,
909+ FromLists Boolean rows cols
931910 ) =>
932911 (a -> b) ->
933912 Relation cols rows
934−fromFRel' = fromF'
913+fromFRel' f =
914+ let minA = minBound @a
915+ maxA = maxBound @a
916+ minB = minBound @b
917+ maxB = maxBound @b
918+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
919+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
920+ elementsA = take ccols [minA .. maxA]
921+ elementsB = take rrows [minB .. maxB]
922+ combinations = (,) <$> elementsA <*> elementsB
923+ combAp = map snd . sort . map (\(a, b) -> if f a == b
924+ then ((fromEnum a, fromEnum b), nat 1)
925+ else ((fromEnum a, fromEnum b), nat 0)) $ combinations
926+ mList = buildList combAp rrows
927+ in tr $ fromLists mList
928+ where
929+ buildList [] _ = []
930+ buildList l r = take r l : buildList (drop r l) r
935931
936932-- | Lifts functions to relations with dimensions matching @a@ and @b@
937933-- cardinality's.
938934fromFRel ::
939935 forall a b.
940936 ( Liftable Boolean a b,
941− CountableDimsN a b,
942− FLN b a
937+ CountableDimensionsN a b,
938+ FromLists Boolean (Normalize b) (Normalize a)
943939 ) =>
944940 (a -> b) ->
945941 Relation (Normalize a) (Normalize b)
946−fromFRel = fromFRel'
942+fromFRel f =
943+ let minA = minBound @a
944+ maxA = maxBound @a
945+ minB = minBound @b
946+ maxB = maxBound @b
947+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
948+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
949+ elementsA = take ccols [minA .. maxA]
950+ elementsB = take rrows [minB .. maxB]
951+ combinations = (,) <$> elementsA <*> elementsB
952+ combAp = map snd . sort . map (\(a, b) -> if f a == b
953+ then ((fromEnum a, fromEnum b), nat 1)
954+ else ((fromEnum a, fromEnum b), nat 0)) $ combinations
955+ mList = buildList combAp rrows
956+ in tr $ fromLists mList
957+ where
958+ buildList [] _ = []
959+ buildList l r = take r l : buildList (drop r l) r
947960
948961-- | Lifts a relation function to a Boolean Matrix
949962toRel ::
@@ -953,17 +966,17 @@ toRel ::
953966 Enum a,
954967 Enum b,
955968 Eq b,
956− CountableDims a b,
957− FLN b a
958− )
969+ CountableDimensionsN a b,
970+ FromListsN Boolean b a
971+ )
959972 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
960973toRel f =
961974 let minA = minBound @a
962975 maxA = maxBound @a
963976 minB = minBound @b
964977 maxB = maxBound @b
965− ccols = fromInteger $ natVal (Proxy :: Proxy (Count a))
966− rrows = fromInteger $ natVal (Proxy :: Proxy (Count b))
978+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
979+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
967980 elementsA = take ccols [minA .. maxA]
968981 elementsB = take rrows [minB .. maxB]
969982 combinations = (,) <$> elementsA <*> elementsB