@@ -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,14 @@ 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
62 -- * Primitives
52 -- * Primitives
@@ -75,7 +66,6 @@ module LAoP.Matrix.Internal
77 matrixBuilder,
68 matrixBuilder,
@@ -86,17 +76,11 @@ module LAoP.Matrix.Internal
87 -- ** Get dimensions
77 -- ** Get dimensions
93 -- ** Matrix Transposition
81 -- ** Matrix Transposition
96− -- ** Scalar multiplication/division of matrices
100 -- ** Selective operator
84 -- ** Selective operator
@@ -105,8 +89,8 @@ module LAoP.Matrix.Internal
107 -- ** Matrix "abiding"
91 -- ** Matrix "abiding"
108− abideJF,
92+ abideJS,
109− abideFJ,
93+ abideSJ,
111 -- ** Zip matrices
95 -- ** Zip matrices
112 zipWithM,
96 zipWithM,
@@ -130,13 +114,12 @@ module LAoP.Matrix.Internal
131 -- | Note that given the restrictions imposed it is not possible to
115 -- | Note that given the restrictions imposed it is not possible to
132 -- implement the standard type classes present in standard Haskell.
116 -- implement the standard type classes present in standard Haskell.
134 -- *** Matrix pairing projections
117 -- *** Matrix pairing projections
138 -- *** Matrix pairing
121 -- *** Matrix pairing
141 -- * Matrix composition and lifting
124 -- * Matrix composition and lifting
@@ -176,17 +159,17 @@ import Data.Kind
176import Data.List
159import Data.List
177import Data.Maybe
160import Data.Maybe
178import Data.Proxy
161import Data.Proxy
180import Data.Void
162import Data.Void
181import GHC.TypeLits
163import GHC.TypeLits
182import Data.Type.Equality
164import Data.Type.Equality
183import GHC.Generics
165import GHC.Generics
184import Control.DeepSeq
166import Control.DeepSeq
167+import Control.Category
185−import Prelude hiding (id, (.))
168+import Prelude hiding ((.))
186−import qualified Prelude (id, (.))
188-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
170-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
189data Matrix e cols rows where
171data Matrix e cols rows where
172+ Empty :: Matrix e Void Void
190 One :: e -> Matrix e () ()
173 One :: e -> Matrix e () ()
191 Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
174 Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
192 Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
175 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
217-- Thanks to Li-Yao Xia this type family is super fast.
200-- Thanks to Li-Yao Xia this type family is super fast.
218type family FromNat (n :: Nat) :: Type where
201type family FromNat (n :: Nat) :: Type where
219 FromNat 1 = ()
203 FromNat 1 = ()
220 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
204 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
@@ -232,56 +216,67 @@ type family Normalize (d :: Type) :: Type where
232-- | Constraint type synonyms to keep the type signatures less convoluted
216-- | Constraint type synonyms to keep the type signatures less convoluted
233type Countable a = KnownNat (Count a)
217type Countable a = KnownNat (Count a)
234type CountableN a = KnownNat (Count (Normalize a))
218type CountableN a = KnownNat (Count (Normalize a))
235−type CountableDims a b = (Countable a, Countable b)
219+type CountableDimensions a b = (Countable a, Countable b)
236−type CountableDimsN a b = (CountableN a, CountableN b)
220+type CountableDimensionsN a b = (CountableN a, CountableN b)
237−type FL a b = FromLists a b
238−type FLN a b = FromLists (Normalize a) (Normalize b)
221+type FromListsN e a b = FromLists e (Normalize a) (Normalize b)
239type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
222type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
240type Trivial a = FromNat (Count a) ~ a
223type Trivial a = FromNat (Count a) ~ a
242−-- | It is possible to implement a constrained version of the category type
225+-- | It isn't possible to implement the 'id' function so it's
243−-- class.
226+-- implementation is 'undefined'. However 'comp' can be and this partial
227+-- class implementation exists just to make the code more readable.
229+-- Please use 'iden' instead.
244instance (Num e) => Category (Matrix e) where
230instance (Num e) => Category (Matrix e) where
245− type Object (Matrix e) a = (FL a a, Countable a)
231+ id = undefined
247− (.) = comp
232+ (.) = comp
249instance NFData e => NFData (Matrix e cols rows) where
234instance NFData e => NFData (Matrix e cols rows) where
250− rnf (One e) = rnf e
236+ rnf (One e) = rnf e
251 rnf (Join a b) = rnf a `seq` rnf b
237 rnf (Join a b) = rnf a `seq` rnf b
252 rnf (Fork a b) = rnf a `seq` rnf b
238 rnf (Fork a b) = rnf a `seq` rnf b
254instance Eq e => Eq (Matrix e cols rows) where
240instance Eq e => Eq (Matrix e cols rows) where
241+ Empty == Empty = True
255− (One a) == (One b) = a == b
242+ (One a) == (One b) = a == b
256− (Join a b) == (Join c d) = a == c && b == d
243+ (Join a b) == (Join c d) = a == c && b == d
257− (Fork a b) == (Fork c d) = a == c && b == d
244+ (Fork a b) == (Fork c d) = a == c && b == d
258− x@(Fork _ _) == y@(Join _ _) = x == abideJF y
245+ x@(Fork _ _) == y@(Join _ _) = x == abideJS y
259− x@(Join _ _) == y@(Fork _ _) = abideJF x == y
246+ x@(Join _ _) == y@(Fork _ _) = abideJS x == y
261instance Num e => Num (Matrix e cols rows) where
248instance Num e => Num (Matrix e cols rows) where
262 a + b = zipWithM (+) a b
250 a + b = zipWithM (+) a b
264 a - b = zipWithM (-) a b
252 a - b = zipWithM (-) a b
266 a * b = zipWithM (*) a b
254 a * b = zipWithM (*) a b
268− abs (One a) = One (abs a)
257+ abs (One a) = One (abs a)
269− abs (Join a b) = Join (abs a) (abs b)
258+ abs (Join a b) = Join (abs a) (abs b)
270 abs (Fork a b) = Fork (abs a) (abs b)
259 abs (Fork a b) = Fork (abs a) (abs b)
261+ signum Empty = Empty
272− signum (One a) = One (signum a)
262+ signum (One a) = One (signum a)
273− signum (Join a b) = Join (signum a) (signum b)
263+ signum (Join a b) = Join (signum a) (signum b)
274 signum (Fork a b) = Fork (signum a) (signum b)
264 signum (Fork a b) = Fork (signum a) (signum b)
276instance Ord e => Ord (Matrix e cols rows) where
266instance Ord e => Ord (Matrix e cols rows) where
267+ Empty <= Empty = True
277− (One a) <= (One b) = a <= b
268+ (One a) <= (One b) = a <= b
278− (Join a b) <= (Join c d) = (a <= c) && (b <= d)
269+ (Join a b) <= (Join c d) = (a <= c) && (b <= d)
279− (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
270+ (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
280− x@(Fork _ _) <= y@(Join _ _) = x <= abideJF y
271+ x@(Fork _ _) <= y@(Join _ _) = x <= abideJS y
281− x@(Join _ _) <= y@(Fork _ _) = abideJF x <= y
272+ x@(Join _ _) <= y@(Fork _ _) = abideJS x <= y
283-- Primitives
274-- Primitives
276+-- | Empty matrix constructor
277+empty :: Matrix e Void Void
285-- | Unit matrix constructor
280-- | Unit matrix constructor
286one :: e -> Matrix e () ()
281one :: e -> Matrix e () ()
@@ -312,86 +307,69 @@ infixl 2 ===
313-- Given that it is not possible to branch on types at the term level type
308-- Given that it is not possible to branch on types at the term level type
314-- classes are needed very much like an inductive definition but on types.
309-- 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
316 -- | Build a matrix out of a list of list of elements. Throws a runtime
311 -- | Build a matrix out of a list of list of elements. Throws a runtime
317 -- error if the dimensions do not match.
312 -- error if the dimensions do not match.
318 fromLists :: [[e]] -> Matrix e cols rows
313 fromLists :: [[e]] -> Matrix e cols rows
320−instance FromLists () () where
315+instance FromLists e Void Void where
316+ fromLists [] = Empty
317+ fromLists _ = error "Wrong dimensions"
319+instance {-# OVERLAPPING #-} FromLists e () () where
321 fromLists [[e]] = One e
320 fromLists [[e]] = One e
322 fromLists _ = error "Wrong dimensions"
321 fromLists _ = error "Wrong dimensions"
324−instance (FromLists cols ()) => FromLists (Either () cols) () where
323+instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
325 fromLists [h : t] = Join (One h) (fromLists [t])
324 fromLists [h : t] = Join (One h) (fromLists [t])
326 fromLists _ = error "Wrong dimensions"
325 fromLists _ = error "Wrong dimensions"
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
330− fromLists [l] =
328+ fromLists [l] =
331 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
329 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
332 in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
330 in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
333 fromLists _ = error "Wrong dimensions"
331 fromLists _ = error "Wrong dimensions"
335−instance (FromLists () rows) => FromLists () (Either () rows) where
333+instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
336 fromLists ([h] : t) = Fork (One h) (fromLists t)
334 fromLists ([h] : t) = Fork (One h) (fromLists t)
337 fromLists _ = error "Wrong dimensions"
335 fromLists _ = error "Wrong dimensions"
339−instance {-# OVERLAPPABLE #-}
340− (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where
337+instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, Countable a) => FromLists e () (Either a b) where
341− fromLists l@([_] : _) =
338+ fromLists l@([_] : _) =
342 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
339 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
343 in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
340 in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
344 fromLists _ = error "Wrong dimensions"
341 fromLists _ = error "Wrong dimensions"
346−instance (FromLists (Either a b) c, FromLists (Either a b) d, Countable c)
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
347− => FromLists (Either a b) (Either c d) where
348 fromLists l@(h : t) =
344 fromLists l@(h : t) =
349 let lh = length h
345 let lh = length h
350 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
346 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
351− condition = all ((== lh) . length) t
347+ condition = all (== lh) (map length t)
352 in if lh > 0 && condition
348 in if lh > 0 && condition
353 then Fork (fromLists (take rowsC l)) (fromLists (drop rowsC l))
349 then Fork (fromLists (take rowsC l)) (fromLists (drop rowsC l))
354 else error "Not all rows have the same length"
350 else error "Not all rows have the same length"
356-- | Matrix builder function. Constructs a matrix provided with
352-- | Matrix builder function. Constructs a matrix provided with
357−-- a construction function that operates with indices.
353+-- a construction function.
358−matrixBuilder' ::
354+matrixBuilder ::
359 forall e cols rows.
355 forall e cols rows.
360− ( FL cols rows,
356+ ( FromLists e cols rows,
361− CountableDims cols rows
357+ CountableDimensions cols rows
359+ ((Int, Int) -> e) ->
362− ) => ((Int, Int) -> e) -> Matrix e cols rows
360+ Matrix e cols rows
363−matrixBuilder' f =
361+matrixBuilder f =
364 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
362 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
365 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
363 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
366 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
364 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
367 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
365 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
369−-- | Matrix builder function. Constructs a matrix provided with
370−-- a construction function that operates with arbitrary types.
380− ) => ((a, b) -> e) -> Matrix e (Normalize a) (Normalize b)
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
387− buildList r l = take r l : buildList r (drop r l)
389-- | Constructs a column vector matrix
367-- | Constructs a column vector matrix
390−col :: (FL () rows) => [e] -> Matrix e () rows
368+col :: (FromLists e () rows) => [e] -> Matrix e () rows
391col = fromLists . map (: [])
369col = fromLists . map (: [])
393-- | Constructs a row vector matrix
371-- | Constructs a row vector matrix
394−row :: (FL cols ()) => [e] -> Matrix e cols ()
372+row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
395row = fromLists . (: [])
373row = fromLists . (: [])
397-- | Lifts functions to matrices with arbitrary dimensions.
375-- | Lifts functions to matrices with arbitrary dimensions.
@@ -401,8 +379,8 @@ row = fromLists . (: [])
402 forall a b cols rows e.
380 forall a b cols rows e.
403 ( Liftable e a b,
381 ( Liftable e a b,
404− CountableDims cols rows,
382+ CountableDimensions cols rows,
405− FL rows cols
383+ FromLists e rows cols
407 (a -> b) ->
385 (a -> b) ->
408 Matrix e cols rows
386 Matrix e cols rows
@@ -416,8 +394,8 @@ fromF' f =
416 elementsA = take ccols [minA .. maxA]
394 elementsA = take ccols [minA .. maxA]
417 elementsB = take rrows [minB .. maxB]
395 elementsB = take rrows [minB .. maxB]
418 combinations = (,) <$> elementsA <*> elementsB
396 combinations = (,) <$> elementsA <*> elementsB
419− combAp = map snd . sort . map (\(a, b) -> if f a == b
397+ combAp = map snd . sort . map (\(a, b) -> if f a == b
420− then ((fromEnum a, fromEnum b), 1)
398+ then ((fromEnum a, fromEnum b), 1)
421 else ((fromEnum a, fromEnum b), 0)) $ combinations
399 else ((fromEnum a, fromEnum b), 0)) $ combinations
422 mList = buildList combAp rrows
400 mList = buildList combAp rrows
423 in tr $ fromLists mList
401 in tr $ fromLists mList
@@ -430,17 +408,35 @@ fromF' f =
431 forall a b e.
409 forall a b e.
432 ( Liftable e a b,
410 ( Liftable e a b,
433− CountableDimsN a b,
411+ CountableDimensionsN a b,
434− FLN b a
412+ FromListsN e b a
436 (a -> b) ->
414 (a -> b) ->
437 Matrix e (Normalize a) (Normalize b)
415 Matrix e (Normalize a) (Normalize b)
438−fromF = fromF'
416+fromF f =
417+ let minA = minBound @a
421+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
422+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
423+ elementsA = take ccols [minA .. maxA]
424+ elementsB = take rrows [minB .. maxB]
425+ combinations = (,) <$> elementsA <*> elementsB
426+ combAp = map snd . sort . map (\(a, b) -> if f a == b
427+ then ((fromEnum a, fromEnum b), 1)
428+ else ((fromEnum a, fromEnum b), 0)) $ combinations
429+ mList = buildList combAp rrows
430+ in tr $ fromLists mList
433+ buildList l r = take r l : buildList (drop r l) r
440-- Conversion
435-- Conversion
442-- | Converts a matrix to a list of lists of elements.
437-- | Converts a matrix to a list of lists of elements.
443toLists :: Matrix e cols rows -> [[e]]
438toLists :: Matrix e cols rows -> [[e]]
444toLists (One e) = [[e]]
440toLists (One e) = [[e]]
445toLists (Fork l r) = toLists l ++ toLists r
441toLists (Fork l r) = toLists l ++ toLists r
446toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
442toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
@@ -452,28 +448,28 @@ toList = concat . toLists
452-- Zeros Matrix
448-- Zeros Matrix
454-- | The zero matrix. A matrix wholly filled with zeros.
450-- | The zero matrix. A matrix wholly filled with zeros.
455−zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
451+zeros :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows
456−zeros = matrixBuilder' (const 0)
452+zeros = matrixBuilder (const 0)
458-- Ones Matrix
454-- Ones Matrix
460-- | The ones matrix. A matrix wholly filled with ones.
456-- | The ones matrix. A matrix wholly filled with ones.
462-- Also known as T (Top) matrix.
458-- Also known as T (Top) matrix.
463−ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
459+ones :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows
464−ones = matrixBuilder' (const 1)
460+ones = matrixBuilder (const 1)
466-- Const Matrix
462-- Const Matrix
468-- | The constant matrix constructor. A matrix wholly filled with a given
464-- | The constant matrix constructor. A matrix wholly filled with a given
470−constant :: (Num e, FL cols rows, CountableDims cols rows) => e -> Matrix e cols rows
466+constant :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => e -> Matrix e cols rows
471−constant e = matrixBuilder' (const e)
467+constant e = matrixBuilder (const e)
473-- Bang Matrix
469-- Bang Matrix
475-- | The T (Top) row vector matrix.
471-- | The T (Top) row vector matrix.
476−bang :: forall e cols. (Num e, Enum e, FL cols (), Countable cols) => Matrix e cols ()
472+bang :: forall e cols. (Num e, Enum e, FromLists e cols (), Countable cols) => Matrix e cols ()
478 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
474 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
479 in fromLists [take c [1, 1 ..]]
475 in fromLists [take c [1, 1 ..]]
@@ -481,8 +477,8 @@ bang =
481-- iden Matrix
477-- iden Matrix
483-- | iden matrix.
479-- | iden matrix.
484−iden :: forall e cols . (Num e, FL cols cols, Countable cols) => Matrix e cols cols
480+iden :: (Num e, FromLists e cols cols, Countable cols) => Matrix e cols cols
485−iden = matrixBuilder' (bool 0 1 . uncurry (==))
481+iden = matrixBuilder (bool 0 1 . uncurry (==))
486{-# NOINLINE iden #-}
482{-# NOINLINE iden #-}
488-- Matrix composition (MMM)
484-- Matrix composition (MMM)
@@ -492,90 +488,65 @@ iden = matrixBuilder' (bool 0 1 . uncurry (==))
492-- This definition takes advantage of divide-and-conquer and fusion laws
488-- This definition takes advantage of divide-and-conquer and fusion laws
493-- from LAoP.
489-- from LAoP.
494comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
490comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
491+comp Empty Empty = Empty
495−comp (One a) (One b) = One (a * b)
492+comp (One a) (One b) = One (a * b)
496comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
493comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
497comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
494comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
498−comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
495+comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
499{-# NOINLINE comp #-}
496{-# NOINLINE comp #-}
500−{-# RULES
497+{-# RULES
501 "comp/iden1" forall m. comp m iden = m ;
498 "comp/iden1" forall m. comp m iden = m ;
502 "comp/iden2" forall m. comp iden m = m
499 "comp/iden2" forall m. comp iden m = m
505−-- Scalar multiplication of matrices
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)
514−-- Scalar division of matrices
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)
523-- Projections
502-- Projections
525-- | Biproduct first component projection
504-- | Biproduct first component projection
526−p1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e (Either m n) m
505+p1 :: forall e m n. (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e (Either m n) m
527−p1 = join id zeros
506+p1 =
507+ let iden = iden :: Matrix e m m
508+ zero = zeros :: Matrix e n m
529-- | Biproduct second component projection
511-- | Biproduct second component projection
530−p2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e (Either m n) n
512+p2 :: forall e m n. (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e (Either m n) n
531−p2 = join zeros id
513+p2 =
514+ let iden = iden :: Matrix e n n
515+ zero = zeros :: Matrix e m n
533-- Injections
518-- Injections
535-- | Biproduct first component injection
520-- | Biproduct first component injection
536−i1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e m (Either m n)
521+i1 :: (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
537i1 = tr p1
522i1 = tr p1
539-- | Biproduct second component injection
524-- | Biproduct second component injection
540−i2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e n (Either m n)
525+i2 :: (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
541i2 = tr p2
526i2 = tr p2
543-- Dimensions
528-- Dimensions
545-- | Obtain the number of rows.
530-- | Obtain the number of rows.
547−-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
532+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
548−-- dimensions in constant time. For a version that doesn't require the
533+-- dimensions in constant time.
549−-- constraint see 'rows''.
534+--
535+-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
536+-- exchange for performance.
550rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
537rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
551rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
538rows _ = 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
562-- | Obtain the number of columns.
540-- | Obtain the number of columns.
542+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
543+-- dimensions in constant time.
564−-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
545+-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
565−-- dimensions in constant time. For a version that doesn't require the
546+-- exchange for performance.
566−-- constraint see 'columns''.
567columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
547columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
568columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
548columns _ = 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
579-- Coproduct Bifunctor
550-- Coproduct Bifunctor
581infixl 5 -|-
552infixl 5 -|-
@@ -584,11 +555,11 @@ infixl 5 -|-
585 forall e n k m j.
556 forall e n k m j.
587− CountableDims j k,
558+ CountableDimensions j k,
588− FL k k,
559+ FromLists e k k,
589− FL j k,
560+ FromLists e j k,
590− FL k j,
561+ FromLists e k j,
591− FL j j
562+ FromLists e j j
593 Matrix e n k ->
564 Matrix e n k ->
594 Matrix e m j ->
565 Matrix e m j ->
@@ -598,147 +569,150 @@ infixl 5 -|-
598-- Khatri Rao Product and projections
569-- Khatri Rao Product and projections
600-- | Khatri Rao product first component projection matrix.
571-- | Khatri Rao product first component projection matrix.
602 forall e m k .
573 forall e m k .
604− CountableDims k m,
575+ CountableDimensions k m,
605− FL (Normalize (m, k)) m,
576+ FromLists e (Normalize (m, k)) m,
606 CountableN (m, k)
577 CountableN (m, k)
607 ) => Matrix e (Normalize (m, k)) m
578 ) => Matrix e (Normalize (m, k)) m
608−fstM = matrixBuilder' f
579+fstM = matrixBuilder f
610 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
581 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
612 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
583 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
613− | otherwise = 0
584+ | otherwise = 0
615-- | Khatri Rao product second component projection matrix.
586-- | Khatri Rao product second component projection matrix.
617 forall e m k .
588 forall e m k .
619− CountableDims k m,
590+ CountableDimensions k m,
620− FL (Normalize (m, k)) k,
591+ FromLists e (Normalize (m, k)) k,
621 CountableN (m, k)
592 CountableN (m, k)
622 ) => Matrix e (Normalize (m, k)) k
593 ) => Matrix e (Normalize (m, k)) k
623−sndM = matrixBuilder' f
594+sndM = matrixBuilder f
625 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
596 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
627 | x == y || mod (y - x) offset == 0 = 1
598 | x == y || mod (y - x) offset == 0 = 1
628− | otherwise = 0
599+ | otherwise = 0
630-- | Khatri Rao Matrix product also known as matrix pairing.
601-- | Khatri Rao Matrix product also known as matrix pairing.
632-- NOTE: That this is not a true categorical product, see for instance:
603-- NOTE: That this is not a true categorical product, see for instance:
635−-- | fstM . kr a b == a
606+-- | fstM . khatri a b == a
636−-- kr a b ==> |
607+-- khatri a b ==> |
637−-- | sndM . kr a b == b
608+-- | sndM . khatri a b == b
640-- __Emphasis__ on the implication symbol.
611-- __Emphasis__ on the implication symbol.
642− forall e cols a b.
613+ forall e cols a b.
644− CountableDims a b,
615+ CountableDimensions a b,
645 CountableN (a, b),
616 CountableN (a, b),
646− FL (Normalize (a, b)) a,
617+ FromLists e (Normalize (a, b)) a,
647− FL (Normalize (a, b)) b
618+ FromLists e (Normalize (a, b)) b
648 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
619 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
649−kr a b =
620+khatri a b =
650 let fstM' = fstM @e @a @b
621 let fstM' = fstM @e @a @b
651 sndM' = sndM @e @a @b
622 sndM' = sndM @e @a @b
652− in (tr fstM' . a) * (tr sndM' . b)
623+ in (tr fstM') . a * (tr sndM') . b
654-- Product Bifunctor (Kronecker)
625-- Product Bifunctor (Kronecker)
656infixl 4 ><
627infixl 4 ><
658-- | Matrix product functor also known as kronecker product
629-- | Matrix product functor also known as kronecker product
660− forall e m p n q.
631+ forall e m p n q.
662− CountableDims m n,
633+ CountableDimensions m n,
663− CountableDims p q,
634+ CountableDimensions p q,
664− CountableDimsN (m, n) (p, q),
635+ CountableDimensionsN (m, n) (p, q),
665− FL (Normalize (m, n)) m,
636+ FromLists e (Normalize (m, n)) m,
666− FL (Normalize (m, n)) n,
637+ FromLists e (Normalize (m, n)) n,
667− FL (Normalize (p, q)) p,
638+ FromLists e (Normalize (p, q)) p,
668− FL (Normalize (p, q)) q
639+ FromLists e (Normalize (p, q)) q
670 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
641 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
671(><) a b =
642(><) a b =
672 let fstM' = fstM @e @m @n
643 let fstM' = fstM @e @m @n
673 sndM' = sndM @e @m @n
644 sndM' = sndM @e @m @n
674− in kr (a . fstM') (b . sndM')
645+ in khatri (a . fstM') (b . sndM')
676-- Matrix abide Join Fork
647-- Matrix abide Join Fork
678−-- | Matrix "abiding" following the 'Join'-'Fork' exchange law.
649+-- | Matrix "abiding" followin the 'Join'-'Fork' abide law.
683-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
654-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
685−abideJF :: Matrix e cols rows -> Matrix e cols rows
656+abideJS :: Matrix e cols rows -> Matrix e cols rows
686−abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
657+abideJS (Join (Fork a c) (Fork b d)) = Fork (Join (abideJS a) (abideJS b)) (Join (abideJS c) (abideJS d)) -- Join-Fork abide law
658+abideJS Empty = Empty
687−abideJF (One e) = One e
659+abideJS (One e) = One e
688−abideJF (Join a b) = Join (abideJF a) (abideJF b)
660+abideJS (Join a b) = Join (abideJS a) (abideJS b)
689−abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
661+abideJS (Fork a b) = Fork (abideJS a) (abideJS b)
691-- Matrix abide Fork Join
663-- Matrix abide Fork Join
693-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
665-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
696-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
668-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
698−abideFJ :: Matrix e cols rows -> Matrix e cols rows
670+abideSJ :: Matrix e cols rows -> Matrix e cols rows
699−abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law
671+abideSJ (Fork (Join a b) (Join c d)) = Join (Fork (abideSJ a) (abideSJ c)) (Fork (abideSJ b) (abideSJ d)) -- Fork-Join abide law
672+abideSJ Empty = Empty
700−abideFJ (One e) = One e
673+abideSJ (One e) = One e
701−abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
674+abideSJ (Join a b) = Join (abideSJ a) (abideSJ b)
702−abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
675+abideSJ (Fork a b) = Fork (abideSJ a) (abideSJ b)
704-- Matrix transposition
677-- Matrix transposition
706-- | Matrix transposition.
679-- | Matrix transposition.
707tr :: Matrix e cols rows -> Matrix e rows cols
680tr :: Matrix e cols rows -> Matrix e rows cols
708−tr (One e) = One e
682+tr (One e) = One e
709−tr (Join a b) = Fork (tr a) (tr b)
683+tr (Join a b) = Fork (tr a) (tr b)
710tr (Fork a b) = Join (tr a) (tr b)
684tr (Fork a b) = Join (tr a) (tr b)
712-- Selective 'select' operator
686-- Selective 'select' operator
714-- | Selective functors 'select' operator equivalent inspired by the
688-- | Selective functors 'select' operator equivalent inspired by the
715-- ArrowMonad solution presented in the paper.
689-- 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
690+select :: (Num e, FromLists e b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
717−select (Fork a b) y = y . a + b -- Divide-and-conquer law
691+select (Fork a b) y = y . a + b -- Divide-and-conquer law
718select (Join (Fork a c) (Fork b d)) y = join (y . a + c) (y . b + d) -- Pattern matching + DnC law
692select (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
693+select m y = join y iden . m
723− CountableDims a b,
697+ CountableDimensions a b,
724− CountableDims c (Either b c),
698+ CountableDimensions c (Either b c),
725− FL c b,
699+ FromLists e c b,
726− FL a b,
700+ FromLists e a b,
727− FL a a,
701+ FromLists e a a,
728− FL b b,
702+ FromLists e b b,
729− FL c c,
703+ FromLists e c c,
730− FL b a,
704+ FromLists e b a,
731− FL b c,
705+ FromLists e b c,
732− FL (Either b c) b,
706+ FromLists e (Either b c) b,
733− FL (Either b c) c
707+ FromLists e (Either b c) c
735 => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c
709 => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c
736branch x l r = f x `select` g l `select` r
710branch x l r = f x `select` g l `select` r
738− f :: (Num e, Countable a, CountableDims b c, FL a b, FL c b, FL b b, FL b a, FL a a)
712+ 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)
739 => Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
713 => Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
740 f m = fork (tr i1) (i1 . tr i2) . m
714 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)
715+ g :: (Num e, CountableDimensions b c, FromLists e b c, FromLists e c c) => Matrix e a c -> Matrix e a (Either b c)
742 g m = i2 . m
716 g m = i2 . m
744-- McCarthy's Conditional
718-- McCarthy's Conditional
@@ -747,9 +721,9 @@ branch x l r = f x `select` g l `select` r
748 ( Trivial cols,
722 ( Trivial cols,
749 Countable cols,
723 Countable cols,
750− FL () cols,
724+ FromLists e () cols,
751− FL cols (),
725+ FromLists e cols (),
752− FL cols cols,
726+ FromLists e cols cols,
753 Bounded a,
727 Bounded a,
@@ -759,12 +733,12 @@ cond ::
759 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
733 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
760cond p f g = join f g . grd p
734cond p f g = join f g . grd p
763 ( Trivial q,
737 ( Trivial q,
764 Countable q,
738 Countable q,
765− FL () q,
739+ FromLists e () q,
766− FL q (),
740+ FromLists e q (),
767− FL q q,
741+ FromLists e q q,
768 Bounded a,
742 Bounded a,
@@ -774,42 +748,42 @@ grd ::
774 (a -> Bool) -> Matrix e q (Either q q)
748 (a -> Bool) -> Matrix e q (Either q q)
775grd f = fork (corr f) (corr (not . f))
749grd f = fork (corr f) (corr (not . f))
778− forall e a q .
752+ forall e a q .
779 ( Trivial q,
753 ( Trivial q,
780 Countable q,
754 Countable q,
781− FL () q,
755+ FromLists e () q,
782− FL q (),
756+ FromLists e q (),
783− FL q q,
757+ FromLists e q q,
784 Liftable e a Bool
758 Liftable e a Bool
786 => (a -> Bool) -> Matrix e q q
760 => (a -> Bool) -> Matrix e q q
787corr p = let f = fromF' p :: Matrix e q ()
761corr p = let f = fromF' p :: Matrix e q ()
788− in kr f (id :: Matrix e q q)
762+ in khatri f (iden :: Matrix e q q)
790-- Pretty print
764-- Pretty print
792prettyAux :: Show e => [[e]] -> [[e]] -> String
766prettyAux :: Show e => [[e]] -> [[e]] -> String
793prettyAux [] _ = ""
767prettyAux [] _ = ""
794−prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
768+prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
796 v = fmap show m
770 v = fmap show m
797 widest = maximum $ fmap length v
771 widest = maximum $ fmap length v
798 fill str = replicate (widest - length str - 2) ' ' ++ str
772 fill str = replicate (widest - length str - 2) ' ' ++ str
799−prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
773+prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
801− v = fmap show m
775+ v = fmap show m
802− widest = maximum $ fmap length v
776+ widest = maximum $ fmap length v
803 fill str = replicate (widest - length str - 2) ' ' ++ str
777 fill str = replicate (widest - length str - 2) ' ' ++ str
804−prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
778+prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
805 prettyAux t l
779 prettyAux t l
807− v = fmap show l
781+ v = fmap show l
808− widest = maximum $ fmap length v
782+ widest = maximum $ fmap length v
809 fill str = replicate (widest - length str - 2) ' ' ++ str
783 fill str = replicate (widest - length str - 2) ' ' ++ str
811-- | Matrix pretty printer
785-- | Matrix pretty printer
812−pretty :: (CountableDims cols rows, Show e) => Matrix e cols rows -> String
786+pretty :: (CountableDimensions cols rows, Show e) => Matrix e cols rows -> String
813pretty m = concat
787pretty m = concat
814 [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"
788 [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"
815 , unlines
789 , unlines
@@ -817,16 +791,16 @@ pretty m = concat
817 , "└ ", unwords (replicate (columns m) blank), " ┘"
791 , "└ ", unwords (replicate (columns m) blank), " ┘"
820− strings = map show (toList m)
794+ strings = map show (toList m)
821− widest = maximum $ map length strings
795+ widest = maximum $ map length strings
822 fill str = replicate (widest - length str) ' ' ++ str
796 fill str = replicate (widest - length str) ' ' ++ str
823− blank = fill ""
797+ blank = fill ""
824 safeGet i j m
798 safeGet i j m
825 | i > rows m || j > columns m || i < 1 || j < 1 = Nothing
799 | i > rows m || j > columns m || i < 1 || j < 1 = Nothing
826 | otherwise = Just $ unsafeGet i j m (toList m)
800 | otherwise = Just $ unsafeGet i j m (toList m)
827 unsafeGet i j m l = l !! encode (columns m) (i,j)
801 unsafeGet i j m l = l !! encode (columns m) (i,j)
828− encode m (i,j) = (i-1)*m + j - 1
802+ encode m (i,j) = (i-1)*m + j - 1
829− getElem i j m =
803+ getElem i j m =
830 fromMaybe
804 fromMaybe
832 "getElem: Trying to get the "
806 "getElem: Trying to get the "
@@ -838,20 +812,21 @@ pretty m = concat
838 (safeGet i j m)
812 (safeGet i j m)
840-- | Matrix pretty printer
814-- | Matrix pretty printer
841−prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()
815+prettyPrint :: (CountableDimensions cols rows, Show e) => Matrix e cols rows -> IO ()
842prettyPrint = putStrLn . pretty
816prettyPrint = putStrLn . pretty
844-- | Zip two matrices with a given binary function
818-- | Zip two matrices with a given binary function
845zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
819zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
820+zipWithM f Empty Empty = Empty
846−zipWithM f (One a) (One b) = One (f a b)
821+zipWithM f (One a) (One b) = One (f a b)
847−zipWithM f (Join a b) (Join c d) = Join (zipWithM f a c) (zipWithM f b d)
822+zipWithM f (Join a b) (Join c d) = Join (zipWithM f a c) (zipWithM f b d)
848−zipWithM f (Fork a b) (Fork c d) = Fork (zipWithM f a c) (zipWithM f b d)
823+zipWithM f (Fork a b) (Fork c d) = Fork (zipWithM f a c) (zipWithM f b d)
849−zipWithM f x@(Fork _ _) y@(Join _ _) = zipWithM f x (abideJF y)
824+zipWithM f x@(Fork _ _) y@(Join _ _) = zipWithM f x (abideJS y)
850−zipWithM f x@(Join _ _) y@(Fork _ _) = zipWithM f (abideJF x) y
825+zipWithM f x@(Join _ _) y@(Fork _ _) = zipWithM f (abideJS x) y
852-- Relational operators functions
827-- Relational operators functions
854−type Boolean = Natural 0 1
829+type Boolean = Natural 0 1
855type Relation a b = Matrix Boolean a b
830type Relation a b = Matrix Boolean a b
857-- | Helper conversion function
832-- | Helper conversion function
@@ -867,47 +842,54 @@ fromBool False = nat 0
868-- | Relational negation
843-- | Relational negation
869negateM :: Relation cols rows -> Relation cols rows
844negateM :: Relation cols rows -> Relation cols rows
845+negateM Empty = Empty
870−negateM (One (Nat p)) = One (Nat (negate p))
846+negateM (One (Nat 0)) = One (Nat 1)
847+negateM (One (Nat 1)) = One (Nat 0)
871negateM (Join a b) = Join (negateM a) (negateM b)
848negateM (Join a b) = Join (negateM a) (negateM b)
872−negateM (Fork a b) = Fork (negateM a) (negateM b)
849+negateM (Fork a b) = Fork (negateM a) (negateM b)
874-- | Relational addition
851-- | Relational addition
875orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
852orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
853+orM Empty Empty = Empty
876−orM (One a) (One b) = One (fromBool (toBool a || toBool b))
854+orM (One a) (One b) = One (fromBool (toBool a || toBool b))
877−orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
855+orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
878−orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
856+orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
879−orM x@(Fork _ _) y@(Join _ _) = orM x (abideJF y)
857+orM x@(Fork _ _) y@(Join _ _) = orM x (abideJS y)
880−orM x@(Join _ _) y@(Fork _ _) = orM (abideJF x) y
858+orM x@(Join _ _) y@(Fork _ _) = orM (abideJS x) y
882-- | Relational multiplication
860-- | Relational multiplication
883andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
861andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
862+andM Empty Empty = Empty
884−andM (One a) (One b) = One (fromBool (toBool a && toBool b))
863+andM (One a) (One b) = One (fromBool (toBool a && toBool b))
885−andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
864+andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
886−andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
865+andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
887−andM x@(Fork _ _) y@(Join _ _) = andM x (abideJF y)
866+andM x@(Fork _ _) y@(Join _ _) = andM x (abideJS y)
888−andM x@(Join _ _) y@(Fork _ _) = andM (abideJF x) y
867+andM x@(Join _ _) y@(Fork _ _) = andM (abideJS x) y
890-- | Relational subtraction
869-- | Relational subtraction
891subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
870subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
871+subM Empty Empty = Empty
892−subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
872+subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
893−subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
873+subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
894−subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
874+subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
895−subM x@(Fork _ _) y@(Join _ _) = subM x (abideJF y)
875+subM x@(Fork _ _) y@(Join _ _) = subM x (abideJS y)
896−subM x@(Join _ _) y@(Fork _ _) = subM (abideJF x) y
876+subM x@(Join _ _) y@(Fork _ _) = subM (abideJS x) y
898-- | Matrix relational composition.
878-- | Matrix relational composition.
899compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
879compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
880+compRel Empty Empty = Empty
900−compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
881+compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
901compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
882compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
902compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
883compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
903−compRel c (Join a b) = Join (compRel c a) (compRel c b) -- Join fusion law
884+compRel c (Join a b) = Join (compRel c a) (compRel c b) -- Join fusion law
905-- | Matrix relational right division
886-- | Matrix relational right division
906divR :: Relation b c -> Relation b a -> Relation a c
887divR :: Relation b c -> Relation b a -> Relation a c
888+divR Empty Empty = Empty
907divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
889divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
908divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
890divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
909−divR (Fork a b) c = Fork (divR a c) (divR b c)
891+divR (Fork a b) c = Fork (divR a c) (divR b c)
910−divR c (Fork a b) = Join (divR c a) (divR c b)
892+divR c (Fork a b) = Join (divR c a) (divR c b)
912-- | Matrix relational left division
894-- | Matrix relational left division
913divL :: Relation c b -> Relation a b -> Relation a c
895divL :: Relation c b -> Relation a b -> Relation a c
@@ -926,49 +908,83 @@ divS s r = divL r s `intersection` divR (tr r) (tr s)
926fromFRel' ::
908fromFRel' ::
927 forall a b cols rows.
909 forall a b cols rows.
928 ( Liftable Boolean a b,
910 ( Liftable Boolean a b,
929− CountableDims cols rows,
911+ CountableDimensions cols rows,
930− FL rows cols
912+ FromLists Boolean rows cols
932 (a -> b) ->
914 (a -> b) ->
933 Relation cols rows
915 Relation cols rows
934−fromFRel' = fromF'
916+fromFRel' f =
917+ let minA = minBound @a
921+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
922+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
923+ elementsA = take ccols [minA .. maxA]
924+ elementsB = take rrows [minB .. maxB]
925+ combinations = (,) <$> elementsA <*> elementsB
926+ combAp = map snd . sort . map (\(a, b) -> if f a == b
927+ then ((fromEnum a, fromEnum b), nat 1)
928+ else ((fromEnum a, fromEnum b), nat 0)) $ combinations
929+ mList = buildList combAp rrows
930+ in tr $ fromLists mList
933+ buildList l r = take r l : buildList (drop r l) r
936-- | Lifts functions to relations with dimensions matching @a@ and @b@
935-- | Lifts functions to relations with dimensions matching @a@ and @b@
937-- cardinality's.
936-- cardinality's.
938fromFRel ::
937fromFRel ::
939 forall a b.
938 forall a b.
940 ( Liftable Boolean a b,
939 ( Liftable Boolean a b,
941− CountableDimsN a b,
940+ CountableDimensionsN a b,
942− FLN b a
941+ FromLists Boolean (Normalize b) (Normalize a)
944 (a -> b) ->
943 (a -> b) ->
945 Relation (Normalize a) (Normalize b)
944 Relation (Normalize a) (Normalize b)
946−fromFRel = fromFRel'
945+fromFRel f =
946+ let minA = minBound @a
950+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
951+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
952+ elementsA = take ccols [minA .. maxA]
953+ elementsB = take rrows [minB .. maxB]
954+ combinations = (,) <$> elementsA <*> elementsB
955+ combAp = map snd . sort . map (\(a, b) -> if f a == b
956+ then ((fromEnum a, fromEnum b), nat 1)
957+ else ((fromEnum a, fromEnum b), nat 0)) $ combinations
958+ mList = buildList combAp rrows
959+ in tr $ fromLists mList
962+ buildList l r = take r l : buildList (drop r l) r
948-- | Lifts a relation function to a Boolean Matrix
964-- | Lifts a relation function to a Boolean Matrix
950 forall a b.
966 forall a b.
951 ( Bounded a,
967 ( Bounded a,
952 Bounded b,
968 Bounded b,
956− CountableDims a b,
972+ CountableDimensionsN a b,
957− FLN b a
973+ FromListsN Boolean b a
959 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
975 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
961 let minA = minBound @a
977 let minA = minBound @a
962 maxA = maxBound @a
978 maxA = maxBound @a
963 minB = minBound @b
979 minB = minBound @b
964 maxB = maxBound @b
980 maxB = maxBound @b
965− ccols = fromInteger $ natVal (Proxy :: Proxy (Count a))
981+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
966− rrows = fromInteger $ natVal (Proxy :: Proxy (Count b))
982+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
967 elementsA = take ccols [minA .. maxA]
983 elementsA = take ccols [minA .. maxA]
968 elementsB = take rrows [minB .. maxB]
984 elementsB = take rrows [minB .. maxB]
969 combinations = (,) <$> elementsA <*> elementsB
985 combinations = (,) <$> elementsA <*> elementsB
970− combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
986+ combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
971− then ((fromEnum a, fromEnum b), nat 1)
987+ then ((fromEnum a, fromEnum b), nat 1)
972 else ((fromEnum a, fromEnum b), nat 0)) $ combinations
988 else ((fromEnum a, fromEnum b), nat 0)) $ combinations
973 mList = buildList combAp rrows
989 mList = buildList combAp rrows
974 in tr $ fromLists mList
990 in tr $ fromLists mList