@@ -1,4 +1,6 @@
1+{-# LANGUAGE StrictData #-}
12{-# LANGUAGE TypeFamilyDependencies #-}
3+{-# LANGUAGE ConstraintKinds #-}
24{-# LANGUAGE AllowAmbiguousTypes #-}
35{-# LANGUAGE DataKinds #-}
46{-# LANGUAGE FlexibleContexts #-}
@@ -28,7 +30,7 @@
2830-- motivation behind the library, the underlying theory, and implementation details.
2931--
3032-- This module offers many of the combinators mentioned in the work of
31−-- Macedo (2012) and Oliveira (2012).
33+-- Macedo (2012) and Oliveira (2012).
3234--
3335-- This is an Internal module and it is no supposed to be imported.
3436--
@@ -41,17 +43,26 @@ module LAoP.Matrix.Internal
4143 --
4244 -- There exists two type families that make it easier to write
4345 -- matrix dimensions: 'FromNat' and 'Count'. This approach
44− -- leads to a very straightforward implementation
45− -- of LAoP combinators.
46+ -- leads to a very straightforward implementation
47+ -- of LAoP combinators.
4648
4749 -- * Type safe matrix representation
4850 Matrix (..),
4951
52+ -- * Constraint type aliases
53+ Countable,
54+ CountableDims,
55+ CountableN,
56+ CountableDimsN,
57+ FL,
58+ FLN,
59+ Liftable,
60+ Trivial,
61+
5062 -- * Primitives
51− empty,
5263 one,
53− junc,
54− split,
64+ join,
65+ fork,
5566
5667 -- * Auxiliary type families
5768 FromNat,
@@ -64,6 +75,7 @@ module LAoP.Matrix.Internal
6475 toLists,
6576 toList,
6677 matrixBuilder,
78+ matrixBuilder',
6779 row,
6880 col,
6981 zeros,
@@ -74,28 +86,38 @@ module LAoP.Matrix.Internal
7486 -- * Misc
7587 -- ** Get dimensions
7688 columns,
89+ columns',
7790 rows,
91+ rows',
7892
7993 -- ** Matrix Transposition
8094 tr,
8195
96+ -- ** Scalar multiplication/division of matrices
97+ (.|),
98+ (./),
99+
82100 -- ** Selective operator
83− select,
101+ select,
102+ branch,
84103
85104 -- ** McCarthy's Conditional
86105 cond,
87106
88107 -- ** Matrix "abiding"
89− abideJS,
90− abideSJ,
108+ abideJF,
109+ abideFJ,
110+
111+ -- ** Zip matrices
112+ zipWithM,
91113
92114 -- * Biproduct approach
93− -- ** Split
115+ -- ** Fork
94116 (===),
95117 -- *** Projections
96118 p1,
97119 p2,
98− -- ** Junc
120+ -- ** Join
99121 (|||),
100122 -- *** Injections
101123 i1,
@@ -108,12 +130,13 @@ module LAoP.Matrix.Internal
108130
109131 -- | Note that given the restrictions imposed it is not possible to
110132 -- implement the standard type classes present in standard Haskell.
133+
111134 -- *** Matrix pairing projections
112− kp1,
113− kp2,
135+ fstM,
136+ sndM,
114137
115138 -- *** Matrix pairing
116− khatri,
139+ kr,
117140
118141 -- * Matrix composition and lifting
119142
@@ -121,10 +144,10 @@ module LAoP.Matrix.Internal
121144
122145 -- | Note that given the restrictions imposed it is not possible to
123146 -- implement the standard type classes present in standard Haskell.
124− identity,
147+ iden,
125148 comp,
126− fromF,
127149 fromF',
150+ fromF,
128151
129152 -- * Matrix printing
130153 pretty,
@@ -151,21 +174,22 @@ import LAoP.Utils.Internal
151174import Data.Bool
152175import Data.Kind
153176import Data.List
177+import Data.Maybe
154178import Data.Proxy
179+import Data.Typeable
155180import Data.Void
156181import GHC.TypeLits
157182import Data.Type.Equality
158183import GHC.Generics
159184import Control.DeepSeq
160−import Control.Category
161−import Prelude hiding ((.))
185+import Prelude hiding (id, (.))
186+import qualified Prelude (id, (.))
162187
163188-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
164189data Matrix e cols rows where
165− Empty :: Matrix e Void Void
166190 One :: e -> Matrix e () ()
167− Junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
168− Split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
191+ 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)
169193
170194deriving instance (Show e) => Show (Matrix e cols rows)
171195
@@ -175,221 +199,214 @@ deriving instance (Show e) => Show (Matrix e cols rows)
175199-- 'Generic' instance.
176200type family Count (d :: Type) :: Nat where
177201 Count (Natural n m) = (m - n) + 1
178− Count (Either a b) = (+) (Count a) (Count b)
179− Count (a, b) = (*) (Count a) (Count b)
180− Count (a -> b) = (^) (Count b) (Count a)
202+ Count (List a) = (^) 2 (Count a)
203+ Count (Either a b) = (+) (Count a) (Count b)
204+ Count (a, b) = (*) (Count a) (Count b)
205+ Count (a -> b) = (^) (Count b) (Count a)
181206 -- Generics
182− Count (M1 _ _ f p) = Count (f p)
183− Count (K1 _ _ _) = 1
184− Count (V1 _) = 0
185− Count (U1 _) = 1
207+ Count (M1 _ _ f p) = Count (f p)
208+ Count (K1 _ _ _) = 1
209+ Count (V1 _) = 0
210+ Count (U1 _) = 1
186211 Count ((:*:) a b p) = Count (a p) * Count (b p)
187212 Count ((:+:) a b p) = Count (a p) + Count (b p)
188− Count d = Count (Rep d R)
213+ Count d = Count (Rep d R)
189214
190215-- | Type family that computes of a given type dimension from a given natural
191216--
192217-- Thanks to Li-Yao Xia this type family is super fast.
193218type family FromNat (n :: Nat) :: Type where
194− FromNat 0 = Void
195219 FromNat 1 = ()
196220 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
197221
198222type family FromNat' (b :: Bool) (m :: Type) :: Type where
199− FromNat' 'True m = Either m m
223+ FromNat' 'True m = Either m m
200224 FromNat' 'False m = Either () (Either m m)
201225
202226-- | Type family that normalizes the representation of a given data
203227-- structure
204228type family Normalize (d :: Type) :: Type where
205− Normalize d = FromNat (Count d)
206−
207−-- | It isn't possible to implement the 'id' function so it's
208−-- implementation is 'undefined'. However 'comp' can be and this partial
209−-- class implementation exists just to make the code more readable.
210−--
211−-- Please use 'identity' instead.
229+ Normalize (Either a b) = Either (Normalize a) (Normalize b)
230+ Normalize d = FromNat (Count d)
231+
232+-- | Constraint type synonyms to keep the type signatures less convoluted
233+type Countable a = KnownNat (Count a)
234+type 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)
239+type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
240+type Trivial a = FromNat (Count a) ~ a
241+
242+-- | It is possible to implement a constrained version of the category type
243+-- class.
212244instance (Num e) => Category (Matrix e) where
213− id = undefined
214− (.) = comp
245+ type Object (Matrix e) a = (FL a a, Countable a)
246+ id = iden
247+ (.) = comp
215248
216249instance NFData e => NFData (Matrix e cols rows) where
217− rnf Empty = ()
218− rnf (One e) = rnf e
219− rnf (Junc a b) = rnf a `seq` rnf b
220− rnf (Split a b) = rnf a `seq` rnf b
250+ rnf (One e) = rnf e
251+ rnf (Join a b) = rnf a `seq` rnf b
252+ rnf (Fork a b) = rnf a `seq` rnf b
221253
222254instance Eq e => Eq (Matrix e cols rows) where
223− Empty == Empty = True
224− (One a) == (One b) = a == b
225− (Junc a b) == (Junc c d) = a == c && b == d
226− (Split a b) == (Split c d) = a == c && b == d
227− x@(Split _ _) == y@(Junc _ _) = x == abideJS y
228− x@(Junc _ _) == y@(Split _ _) = abideJS x == y
255+ (One a) == (One b) = a == b
256+ (Join a b) == (Join c d) = a == c && b == d
257+ (Fork a b) == (Fork c d) = a == c && b == d
258+ x@(Fork _ _) == y@(Join _ _) = x == abideJF y
259+ x@(Join _ _) == y@(Fork _ _) = abideJF x == y
229260
230261instance Num e => Num (Matrix e cols rows) where
262+ a + b = zipWithM (+) a b
263+
264+ a - b = zipWithM (-) a b
265+
266+ a * b = zipWithM (*) a b
267+
268+ abs (One a) = One (abs a)
269+ abs (Join a b) = Join (abs a) (abs b)
270+ abs (Fork a b) = Fork (abs a) (abs b)
231271
232− Empty + Empty = Empty
233− (One a) + (One b) = One (a + b)
234− (Junc a b) + (Junc c d) = Junc (a + c) (b + d)
235− (Split a b) + (Split c d) = Split (a + c) (b + d)
236− x@(Split _ _) + y@(Junc _ _) = x + abideJS y
237− x@(Junc _ _) + y@(Split _ _) = abideJS x + y
238−
239− Empty - Empty = Empty
240− (One a) - (One b) = One (a - b)
241− (Junc a b) - (Junc c d) = Junc (a - c) (b - d)
242− (Split a b) - (Split c d) = Split (a - c) (b - d)
243− x@(Split _ _) - y@(Junc _ _) = x - abideJS y
244− x@(Junc _ _) - y@(Split _ _) = abideJS x - y
245−
246− Empty * Empty = Empty
247− (One a) * (One b) = One (a * b)
248− (Junc a b) * (Junc c d) = Junc (a * c) (b * d)
249− (Split a b) * (Split c d) = Split (a * c) (b * d)
250− x@(Split _ _) * y@(Junc _ _) = x * abideJS y
251− x@(Junc _ _) * y@(Split _ _) = abideJS x * y
252−
253− abs Empty = Empty
254− abs (One a) = One (abs a)
255− abs (Junc a b) = Junc (abs a) (abs b)
256− abs (Split a b) = Split (abs a) (abs b)
257−
258− signum Empty = Empty
259− signum (One a) = One (signum a)
260− signum (Junc a b) = Junc (signum a) (signum b)
261− signum (Split a b) = Split (signum a) (signum b)
272+ signum (One a) = One (signum a)
273+ signum (Join a b) = Join (signum a) (signum b)
274+ signum (Fork a b) = Fork (signum a) (signum b)
262275
263276instance Ord e => Ord (Matrix e cols rows) where
264− Empty <= Empty = True
265− (One a) <= (One b) = a <= b
266− (Junc a b) <= (Junc c d) = (a <= c) && (b <= d)
267− (Split a b) <= (Split c d) = (a <= c) && (b <= d)
268− x@(Split _ _) <= y@(Junc _ _) = x <= abideJS y
269− x@(Junc _ _) <= y@(Split _ _) = abideJS x <= y
277+ (One a) <= (One b) = a <= b
278+ (Join a b) <= (Join c d) = (a <= c) && (b <= d)
279+ (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
280+ x@(Fork _ _) <= y@(Join _ _) = x <= abideJF y
281+ x@(Join _ _) <= y@(Fork _ _) = abideJF x <= y
270282
271283-- Primitives
272284
273−-- | Empty matrix constructor
274−empty :: Matrix e Void Void
275−empty = Empty
276−
277285-- | Unit matrix constructor
278286one :: e -> Matrix e () ()
279287one = One
280288
281−-- | Matrix 'Junc' constructor
282−junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
283−junc = Junc
289+-- | Matrix 'Join' constructor
290+join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
291+join = Join
284292
285293infixl 3 |||
286294
287−-- | Matrix 'Junc' constructor
295+-- | Matrix 'Join' constructor
288296(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
289−(|||) = Junc
297+(|||) = Join
290298
291−-- | Matrix 'Split' constructor
292−split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
293−split = Split
299+-- | Matrix 'Fork' constructor
300+fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
301+fork = Fork
294302
295303infixl 2 ===
296304
297−-- | Matrix 'Split' constructor
305+-- | Matrix 'Fork' constructor
298306(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
299−(===) = Split
307+(===) = Fork
300308
301309-- Construction
302310
303311-- | Type class for defining the 'fromList' conversion function.
304312--
305313-- Given that it is not possible to branch on types at the term level type
306−-- classes are needed bery much like an inductive definition but on types.
307−class FromLists e cols rows where
314+-- classes are needed very much like an inductive definition but on types.
315+class FromLists cols rows where
308316 -- | Build a matrix out of a list of list of elements. Throws a runtime
309317 -- error if the dimensions do not match.
310318 fromLists :: [[e]] -> Matrix e cols rows
311319
312−instance FromLists e Void Void where
313− fromLists [] = Empty
314− fromLists _ = error "Wrong dimensions"
315−
316−instance {-# OVERLAPPING #-} FromLists e () () where
320+instance FromLists () () where
317321 fromLists [[e]] = One e
318322 fromLists _ = error "Wrong dimensions"
319323
320−instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
321− fromLists [h : t] = Junc (One h) (fromLists [t])
324+instance (FromLists cols ()) => FromLists (Either () cols) () where
325+ fromLists [h : t] = Join (One h) (fromLists [t])
322326 fromLists _ = error "Wrong dimensions"
323327
324−instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), KnownNat (Count a)) => FromLists e (Either a b) () where
325− fromLists [l] =
328+instance {-# OVERLAPPABLE #-}
329+ (FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () where
330+ fromLists [l] =
326331 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
327− in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])
332+ in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
328333 fromLists _ = error "Wrong dimensions"
329334
330−instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
331− fromLists ([h] : t) = Split (One h) (fromLists t)
335+instance (FromLists () rows) => FromLists () (Either () rows) where
336+ fromLists ([h] : t) = Fork (One h) (fromLists t)
332337 fromLists _ = error "Wrong dimensions"
333338
334−instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, KnownNat (Count a)) => FromLists e () (Either a b) where
335− fromLists l@([_] : _) =
339+instance {-# OVERLAPPABLE #-}
340+ (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where
341+ fromLists l@([_] : _) =
336342 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
337− in Split (fromLists (take rowsA l)) (fromLists (drop rowsA l))
343+ in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
338344 fromLists _ = error "Wrong dimensions"
339345
340−instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a b) d, KnownNat (Count 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
341348 fromLists l@(h : t) =
342349 let lh = length h
343350 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
344− condition = all (== lh) (map length t)
351+ condition = all ((== lh) . length) t
345352 in if lh > 0 && condition
346− then Split (fromLists (take rowsC l)) (fromLists (drop rowsC l))
353+ then Fork (fromLists (take rowsC l)) (fromLists (drop rowsC l))
347354 else error "Not all rows have the same length"
348355
349356-- | Matrix builder function. Constructs a matrix provided with
350−-- a construction function.
351−matrixBuilder ::
357+-- a construction function that operates with indices.
358+matrixBuilder' ::
352359 forall e cols rows.
353− ( FromLists e cols rows,
354− KnownNat (Count cols),
355− KnownNat (Count rows)
356− ) =>
357− ((Int, Int) -> e) ->
358− Matrix e cols rows
359−matrixBuilder f =
360+ ( FL cols rows,
361+ CountableDims cols rows
362+ ) => ((Int, Int) -> e) -> Matrix e cols rows
363+matrixBuilder' f =
360364 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
361365 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
362366 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
363367 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
364368
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+
365389-- | Constructs a column vector matrix
366−col :: (FromLists e () rows) => [e] -> Matrix e () rows
390+col :: (FL () rows) => [e] -> Matrix e () rows
367391col = fromLists . map (: [])
368392
369393-- | Constructs a row vector matrix
370−row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
394+row :: (FL cols ()) => [e] -> Matrix e cols ()
371395row = fromLists . (: [])
372396
373397-- | Lifts functions to matrices with arbitrary dimensions.
374398--
375399-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
376400-- types @a@ or @b@ allows.
377−fromF ::
401+fromF' ::
378402 forall a b cols rows e.
379− ( Bounded a,
380− Bounded b,
381− Enum a,
382− Enum b,
383− Eq b,
384− Num e,
385− Ord e,
386− KnownNat (Count cols),
387− KnownNat (Count rows),
388− FromLists e rows cols
403+ ( Liftable e a b,
404+ CountableDims cols rows,
405+ FL rows cols
389406 ) =>
390407 (a -> b) ->
391408 Matrix e cols rows
392−fromF f =
409+fromF' f =
393410 let minA = minBound @a
394411 maxA = maxBound @a
395412 minB = minBound @b
@@ -399,8 +416,8 @@ fromF f =
399416 elementsA = take ccols [minA .. maxA]
400417 elementsB = take rrows [minB .. maxB]
401418 combinations = (,) <$> elementsA <*> elementsB
402− combAp = map snd . sort . map (\(a, b) -> if f a == b
403− then ((fromEnum a, fromEnum b), 1)
419+ combAp = map snd . sort . map (\(a, b) -> if f a == b
420+ then ((fromEnum a, fromEnum b), 1)
404421 else ((fromEnum a, fromEnum b), 0)) $ combinations
405422 mList = buildList combAp rrows
406423 in tr $ fromLists mList
@@ -410,48 +427,23 @@ fromF f =
410427
411428-- | Lifts functions to matrices with dimensions matching @a@ and @b@
412429-- cardinality's.
413−fromF' ::
430+fromF ::
414431 forall a b e.
415− ( Bounded a,
416− Bounded b,
417− Enum a,
418− Enum b,
419− Eq b,
420− Num e,
421− Ord e,
422− KnownNat (Count (Normalize a)),
423− KnownNat (Count (Normalize b)),
424− FromLists e (Normalize b) (Normalize a)
432+ ( Liftable e a b,
433+ CountableDimsN a b,
434+ FLN b a
425435 ) =>
426436 (a -> b) ->
427437 Matrix e (Normalize a) (Normalize b)
428−fromF' f =
429− let minA = minBound @a
430− maxA = maxBound @a
431− minB = minBound @b
432− maxB = maxBound @b
433− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
434− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
435− elementsA = take ccols [minA .. maxA]
436− elementsB = take rrows [minB .. maxB]
437− combinations = (,) <$> elementsA <*> elementsB
438− combAp = map snd . sort . map (\(a, b) -> if f a == b
439− then ((fromEnum a, fromEnum b), 1)
440− else ((fromEnum a, fromEnum b), 0)) $ combinations
441− mList = buildList combAp rrows
442− in tr $ fromLists mList
443− where
444− buildList [] _ = []
445− buildList l r = take r l : buildList (drop r l) r
438+fromF = fromF'
446439
447440-- Conversion
448441
449442-- | Converts a matrix to a list of lists of elements.
450443toLists :: Matrix e cols rows -> [[e]]
451−toLists Empty = []
452444toLists (One e) = [[e]]
453−toLists (Split l r) = toLists l ++ toLists r
454−toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
445+toLists (Fork l r) = toLists l ++ toLists r
446+toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
455447
456448-- | Converts a matrix to a list of elements.
457449toList :: Matrix e cols rows -> [e]
@@ -460,37 +452,38 @@ toList = concat . toLists
460452-- Zeros Matrix
461453
462454-- | The zero matrix. A matrix wholly filled with zeros.
463−zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
464−zeros = matrixBuilder (const 0)
455+zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
456+zeros = matrixBuilder' (const 0)
465457
466458-- Ones Matrix
467459
468460-- | The ones matrix. A matrix wholly filled with ones.
469461--
470462-- Also known as T (Top) matrix.
471−ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
472−ones = matrixBuilder (const 1)
463+ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
464+ones = matrixBuilder' (const 1)
473465
474466-- Const Matrix
475467
476468-- | The constant matrix constructor. A matrix wholly filled with a given
477469-- value.
478−constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows
479−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)
480472
481473-- Bang Matrix
482474
483475-- | The T (Top) row vector matrix.
484−bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()
476+bang :: forall e cols. (Num e, Enum e, FL cols (), Countable cols) => Matrix e cols ()
485477bang =
486478 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
487479 in fromLists [take c [1, 1 ..]]
488480
489−-- Identity Matrix
481+-- iden Matrix
490482
491−-- | Identity matrix.
492−identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols
493−identity = matrixBuilder (bool 0 1 . uncurry (==))
483+-- | 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 (==))
486+{-# NOINLINE iden #-}
494487
495488-- Matrix composition (MMM)
496489
@@ -499,60 +492,90 @@ identity = matrixBuilder (bool 0 1 . uncurry (==))
499492-- This definition takes advantage of divide-and-conquer and fusion laws
500493-- from LAoP.
501494comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
502−comp Empty Empty = Empty
503−comp (One a) (One b) = One (a * b)
504−comp (Junc a b) (Split c d) = comp a c + comp b d -- Divide-and-conquer law
505−comp (Split a b) c = Split (comp a c) (comp b c) -- Split fusion law
506−comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc fusion law
495+comp (One a) (One b) = One (a * b)
496+comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
497+comp (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
499+{-# NOINLINE comp #-}
500+{-# RULES
501+ "comp/iden1" forall m. comp m iden = m ;
502+ "comp/iden2" forall m. comp iden m = m
503+#-}
504+
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)
507522
508523-- Projections
509524
510525-- | Biproduct first component projection
511−p1 :: forall e m n. (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e (Either m n) m
512−p1 =
513− let iden = identity :: Matrix e m m
514− zero = zeros :: Matrix e n m
515− in junc 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
516528
517529-- | Biproduct second component projection
518−p2 :: forall e m n. (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e (Either m n) n
519−p2 =
520− let iden = identity :: Matrix e n n
521− zero = zeros :: Matrix e m n
522− in junc 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
523532
524533-- Injections
525534
526535-- | Biproduct first component injection
527−i1 :: (Num e, KnownNat (Count n), KnownNat (Count 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)
528537i1 = tr p1
529538
530539-- | Biproduct second component injection
531−i2 :: (Num e, KnownNat (Count n), KnownNat (Count 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)
532541i2 = tr p2
533542
534543-- Dimensions
535544
536545-- | Obtain the number of rows.
537546--
538−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
539−-- dimensions in constant time.
540−--
541−-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
542−-- exchange for performance.
543−rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int
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''.
550+rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
544551rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
545552
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+
546562-- | Obtain the number of columns.
547−--
548−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
549−-- dimensions in constant time.
550563--
551−-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
552−-- exchange for performance.
553−columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int
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''.
567+columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
554568columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
555569
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+
556579-- Coproduct Bifunctor
557580
558581infixl 5 -|-
@@ -561,157 +584,172 @@ infixl 5 -|-
561584(-|-) ::
562585 forall e n k m j.
563586 ( Num e,
564− KnownNat (Count j),
565− KnownNat (Count k),
566− FromLists e k k,
567− FromLists e j k,
568− FromLists e k j,
569− FromLists e j j
587+ CountableDims j k,
588+ FL k k,
589+ FL j k,
590+ FL k j,
591+ FL j j
570592 ) =>
571593 Matrix e n k ->
572594 Matrix e m j ->
573595 Matrix e (Either n m) (Either k j)
574−(-|-) a b = Junc (i1 . a) (i2 . b)
596+(-|-) a b = Join (i1 . a) (i2 . b)
575597
576598-- Khatri Rao Product and projections
577599
578600-- | Khatri Rao product first component projection matrix.
579−kp1 ::
601+fstM ::
580602 forall e m k .
581603 ( Num e,
582− KnownNat (Count k),
583− FromLists e (FromNat (Count m * Count k)) m,
584− KnownNat (Count m),
585− KnownNat (Count (Normalize (m, k)))
604+ CountableDims k m,
605+ FL (Normalize (m, k)) m,
606+ CountableN (m, k)
586607 ) => Matrix e (Normalize (m, k)) m
587−kp1 = matrixBuilder f
608+fstM = matrixBuilder' f
588609 where
589610 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
590611 f (x, y)
591612 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
592− | otherwise = 0
613+ | otherwise = 0
593614
594615-- | Khatri Rao product second component projection matrix.
595−kp2 ::
616+sndM ::
596617 forall e m k .
597618 ( Num e,
598− KnownNat (Count k),
599− FromLists e (FromNat (Count m * Count k)) k,
600− KnownNat (Count m),
601− KnownNat (Count (Normalize (m, k)))
619+ CountableDims k m,
620+ FL (Normalize (m, k)) k,
621+ CountableN (m, k)
602622 ) => Matrix e (Normalize (m, k)) k
603−kp2 = matrixBuilder f
623+sndM = matrixBuilder' f
604624 where
605625 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
606626 f (x, y)
607627 | x == y || mod (y - x) offset == 0 = 1
608− | otherwise = 0
628+ | otherwise = 0
609629
610630-- | Khatri Rao Matrix product also known as matrix pairing.
611631--
612632-- NOTE: That this is not a true categorical product, see for instance:
613−--
633+--
614634-- @
615−-- | kp1 . khatri a b == a
616−-- khatri a b ==> |
617−-- | kp2 . khatri a b == b
635+-- | fstM . kr a b == a
636+-- kr a b ==> |
637+-- | sndM . kr a b == b
618638-- @
619639--
620640-- __Emphasis__ on the implication symbol.
621−khatri ::
622− forall e cols a b.
641+kr ::
642+ forall e cols a b.
623643 ( Num e,
624− KnownNat (Count a),
625− KnownNat (Count b),
626− KnownNat (Count (Normalize (a, b))),
627− FromLists e (Normalize (a, b)) a,
628− FromLists e (Normalize (a, b)) b
644+ CountableDims a b,
645+ CountableN (a, b),
646+ FL (Normalize (a, b)) a,
647+ FL (Normalize (a, b)) b
629648 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
630−khatri a b =
631− let kp1' = kp1 @e @a @b
632− kp2' = kp2 @e @a @b
633− in (tr kp1') . a * (tr kp2') . b
649+kr a b =
650+ let fstM' = fstM @e @a @b
651+ sndM' = sndM @e @a @b
652+ in (tr fstM' . a) * (tr sndM' . b)
634653
635654-- Product Bifunctor (Kronecker)
636655
637656infixl 4 ><
638657
639658-- | Matrix product functor also known as kronecker product
640−(><) ::
641− forall e m p n q.
659+(><) ::
660+ forall e m p n q.
642661 ( Num e,
643− KnownNat (Count m),
644− KnownNat (Count n),
645− KnownNat (Count p),
646− KnownNat (Count q),
647− KnownNat (Count (Normalize (m, n))),
648− FromLists e (Normalize (m, n)) m,
649− FromLists e (Normalize (m, n)) n,
650− KnownNat (Count (Normalize (p, q))),
651− FromLists e (Normalize (p, q)) p,
652− FromLists e (Normalize (p, q)) q
653− )
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+ )
654670 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
655671(><) a b =
656− let kp1' = kp1 @e @m @n
657− kp2' = kp2 @e @m @n
658− in khatri (a . kp1') (b . kp2')
672+ let fstM' = fstM @e @m @n
673+ sndM' = sndM @e @m @n
674+ in kr (a . fstM') (b . sndM')
659675
660−-- Matrix abide Junc Split
676+-- Matrix abide Join Fork
661677
662−-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
663−--
678+-- | Matrix "abiding" following the 'Join'-'Fork' exchange law.
679+--
664680-- Law:
665681--
666682-- @
667−-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
683+-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
668684-- @
669−abideJS :: Matrix e cols rows -> Matrix e cols rows
670−abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law
671−abideJS Empty = Empty
672−abideJS (One e) = One e
673−abideJS (Junc a b) = Junc (abideJS a) (abideJS b)
674−abideJS (Split a b) = Split (abideJS a) (abideJS b)
685+abideJF :: 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
687+abideJF (One e) = One e
688+abideJF (Join a b) = Join (abideJF a) (abideJF b)
689+abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
675690
676−-- Matrix abide Split Junc
691+-- Matrix abide Fork Join
677692
678−-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
679−--
693+-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
694+--
680695-- @
681−-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
696+-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
682697-- @
683−abideSJ :: Matrix e cols rows -> Matrix e cols rows
684−abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law
685−abideSJ Empty = Empty
686−abideSJ (One e) = One e
687−abideSJ (Junc a b) = Junc (abideSJ a) (abideSJ b)
688−abideSJ (Split a b) = Split (abideSJ a) (abideSJ b)
698+abideFJ :: 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
700+abideFJ (One e) = One e
701+abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
702+abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
689703
690704-- Matrix transposition
691705
692706-- | Matrix transposition.
693707tr :: Matrix e cols rows -> Matrix e rows cols
694−tr Empty = Empty
695−tr (One e) = One e
696−tr (Junc a b) = Split (tr a) (tr b)
697−tr (Split a b) = Junc (tr a) (tr b)
708+tr (One e) = One e
709+tr (Join a b) = Fork (tr a) (tr b)
710+tr (Fork a b) = Join (tr a) (tr b)
698711
699712-- Selective 'select' operator
700713
701714-- | Selective functors 'select' operator equivalent inspired by the
702715-- ArrowMonad solution presented in the paper.
703−select :: (Num e, FromLists e b b, KnownNat (Count b)) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
704−select m y = junc y identity . m
716+select :: (Num e, FL 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
718+select (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
720+
721+branch ::
722+ ( 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
734+ )
735+ => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c
736+branch x l r = f x `select` g l `select` r
737+ 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)
739+ => Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
740+ 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)
742+ g m = i2 . m
705743
706744-- McCarthy's Conditional
707745
708746-- | McCarthy's Conditional expresses probabilistic choice.
709747cond ::
710− ( cols ~ FromNat (Count cols),
711− KnownNat (Count cols),
712− FromLists e () cols,
713− FromLists e cols (),
714− FromLists e cols cols,
748+ ( Trivial cols,
749+ Countable cols,
750+ FL () cols,
751+ FL cols (),
752+ FL cols cols,
715753 Bounded a,
716754 Enum a,
717755 Num e,
@@ -719,14 +757,14 @@ cond ::
719757 )
720758 =>
721759 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
722−cond p f g = junc f g . grd p
723−
724−grd ::
725− ( q ~ FromNat (Count q),
726− KnownNat (Count q),
727− FromLists e () q,
728− FromLists e q (),
729− FromLists e q q,
760+cond p f g = join f g . grd p
761+
762+grd ::
763+ ( Trivial q,
764+ Countable q,
765+ FL () q,
766+ FL q (),
767+ FL q q,
730768 Bounded a,
731769 Enum a,
732770 Num e,
@@ -734,63 +772,86 @@ grd ::
734772 )
735773 =>
736774 (a -> Bool) -> Matrix e q (Either q q)
737−grd f = split (corr f) (corr (not . f))
738−
739−corr ::
740− forall e a q .
741− ( q ~ FromNat (Count q),
742− KnownNat (Count q),
743− FromLists e () q,
744− FromLists e q (),
745− FromLists e q q,
746− Bounded a,
747− Enum a,
748− Num e,
749− Ord e
750− )
775+grd f = fork (corr f) (corr (not . f))
776+
777+corr ::
778+ forall e a q .
779+ ( Trivial q,
780+ Countable q,
781+ FL () q,
782+ FL q (),
783+ FL q q,
784+ Liftable e a Bool
785+ )
751786 => (a -> Bool) -> Matrix e q q
752−corr p = let f = fromF p :: Matrix e q ()
753− in khatri f (identity :: Matrix e q q)
787+corr p = let f = fromF' p :: Matrix e q ()
788+ in kr f (id :: Matrix e q q)
754789
755790-- Pretty print
756791
757792prettyAux :: Show e => [[e]] -> [[e]] -> String
758793prettyAux [] _ = ""
759−prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
794+prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
760795 where
761796 v = fmap show m
762797 widest = maximum $ fmap length v
763798 fill str = replicate (widest - length str - 2) ' ' ++ str
764−prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
799+prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
765800 where
766− v = fmap show m
767− widest = maximum $ fmap length v
801+ v = fmap show m
802+ widest = maximum $ fmap length v
768803 fill str = replicate (widest - length str - 2) ' ' ++ str
769−prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
804+prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
770805 prettyAux t l
771806 where
772− v = fmap show l
773− widest = maximum $ fmap length v
807+ v = fmap show l
808+ widest = maximum $ fmap length v
774809 fill str = replicate (widest - length str - 2) ' ' ++ str
775810
776811-- | Matrix pretty printer
777−pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String
778−pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
779− prettyAux (toLists m) (toLists m) ++
780− "└ " ++ unwords (replicate (columns m) blank) ++ " ┘"
781− where
782− v = fmap show (toList m)
783− widest = maximum $ fmap length v
812+pretty :: (CountableDims cols rows, Show e) => Matrix e cols rows -> String
813+pretty m = concat
814+ [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"
815+ , unlines
816+ [ "│ " ++ unwords (fmap (\j -> fill $ show $ getElem i j m) [1..columns m]) ++ " │" | i <- [1..rows m] ]
817+ , "└ ", unwords (replicate (columns m) blank), " ┘"
818+ ]
819+ where
820+ strings = map show (toList m)
821+ widest = maximum $ map length strings
784822 fill str = replicate (widest - length str) ' ' ++ str
785− blank = fill ""
823+ blank = fill ""
824+ safeGet i j m
825+ | i > rows m || j > columns m || i < 1 || j < 1 = Nothing
826+ | otherwise = Just $ unsafeGet i j m (toList m)
827+ unsafeGet i j m l = l !! encode (columns m) (i,j)
828+ encode m (i,j) = (i-1)*m + j - 1
829+ getElem i j m =
830+ fromMaybe
831+ (error $
832+ "getElem: Trying to get the "
833+ ++ show (i, j)
834+ ++ " element from a "
835+ ++ show (rows m) ++ "x" ++ show (columns m)
836+ ++ " matrix."
837+ )
838+ (safeGet i j m)
786839
787840-- | Matrix pretty printer
788−prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()
841+prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()
789842prettyPrint = putStrLn . pretty
790843
844+-- | Zip two matrices with a given binary function
845+zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
846+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)
848+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)
850+zipWithM f x@(Join _ _) y@(Fork _ _) = zipWithM f (abideJF x) y
851+
791852-- Relational operators functions
792853
793−type Boolean = Natural 0 1
854+type Boolean = Natural 0 1
794855type Relation a b = Matrix Boolean a b
795856
796857-- | Helper conversion function
@@ -806,54 +867,47 @@ fromBool False = nat 0
806867
807868-- | Relational negation
808869negateM :: Relation cols rows -> Relation cols rows
809−negateM Empty = Empty
810−negateM (One (Nat 0)) = One (Nat 1)
811−negateM (One (Nat 1)) = One (Nat 0)
812−negateM (Junc a b) = Junc (negateM a) (negateM b)
813−negateM (Split a b) = Split (negateM a) (negateM b)
870+negateM (One (Nat p)) = One (Nat (negate p))
871+negateM (Join a b) = Join (negateM a) (negateM b)
872+negateM (Fork a b) = Fork (negateM a) (negateM b)
814873
815874-- | Relational addition
816875orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
817−orM Empty Empty = Empty
818−orM (One a) (One b) = One (fromBool (toBool a || toBool b))
819−orM (Junc a b) (Junc c d) = Junc (orM a c) (orM b d)
820−orM (Split a b) (Split c d) = Split (orM a c) (orM b d)
821−orM x@(Split _ _) y@(Junc _ _) = orM x (abideJS y)
822−orM x@(Junc _ _) y@(Split _ _) = orM (abideJS x) y
876+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)
878+orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
879+orM x@(Fork _ _) y@(Join _ _) = orM x (abideJF y)
880+orM x@(Join _ _) y@(Fork _ _) = orM (abideJF x) y
823881
824882-- | Relational multiplication
825883andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
826−andM Empty Empty = Empty
827−andM (One a) (One b) = One (fromBool (toBool a && toBool b))
828−andM (Junc a b) (Junc c d) = Junc (andM a c) (andM b d)
829−andM (Split a b) (Split c d) = Split (andM a c) (andM b d)
830−andM x@(Split _ _) y@(Junc _ _) = andM x (abideJS y)
831−andM x@(Junc _ _) y@(Split _ _) = andM (abideJS x) y
884+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)
886+andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
887+andM x@(Fork _ _) y@(Join _ _) = andM x (abideJF y)
888+andM x@(Join _ _) y@(Fork _ _) = andM (abideJF x) y
832889
833890-- | Relational subtraction
834891subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
835−subM Empty Empty = Empty
836−subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
837−subM (Junc a b) (Junc c d) = Junc (subM a c) (subM b d)
838−subM (Split a b) (Split c d) = Split (subM a c) (subM b d)
839−subM x@(Split _ _) y@(Junc _ _) = subM x (abideJS y)
840−subM x@(Junc _ _) y@(Split _ _) = subM (abideJS x) y
892+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)
894+subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
895+subM x@(Fork _ _) y@(Join _ _) = subM x (abideJF y)
896+subM x@(Join _ _) y@(Fork _ _) = subM (abideJF x) y
841897
842898-- | Matrix relational composition.
843899compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
844−compRel Empty Empty = Empty
845−compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
846−compRel (Junc a b) (Split c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
847−compRel (Split a b) c = Split (compRel a c) (compRel b c) -- Split fusion law
848−compRel c (Junc a b) = Junc (compRel c a) (compRel c b) -- Junc fusion law
900+compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
901+compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
902+compRel (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
849904
850905-- | Matrix relational right division
851906divR :: Relation b c -> Relation b a -> Relation a c
852−divR Empty Empty = Empty
853907divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
854−divR (Junc a b) (Junc c d) = andM (divR a c) (divR b d)
855−divR (Split a b) c = Split (divR a c) (divR b c)
856−divR c (Split a b) = Junc (divR c a) (divR c b)
908+divR (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)
910+divR c (Fork a b) = Join (divR c a) (divR c b)
857911
858912-- | Matrix relational left division
859913divL :: Relation c b -> Relation a b -> Relation a c
@@ -869,97 +923,52 @@ divS s r = divL r s `intersection` divR (tr r) (tr s)
869923--
870924-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
871925-- types @a@ or @b@ allows.
872−fromFRel ::
926+fromFRel' ::
873927 forall a b cols rows.
874− ( Bounded a,
875− Bounded b,
876− Enum a,
877− Enum b,
878− Eq b,
879− KnownNat (Count cols),
880− KnownNat (Count rows),
881− FromLists (Natural 0 1) rows cols
928+ ( Liftable Boolean a b,
929+ CountableDims cols rows,
930+ FL rows cols
882931 ) =>
883932 (a -> b) ->
884933 Relation cols rows
885−fromFRel f =
886− let minA = minBound @a
887− maxA = maxBound @a
888− minB = minBound @b
889− maxB = maxBound @b
890− ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
891− rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
892− elementsA = take ccols [minA .. maxA]
893− elementsB = take rrows [minB .. maxB]
894− combinations = (,) <$> elementsA <*> elementsB
895− combAp = map snd . sort . map (\(a, b) -> if f a == b
896− then ((fromEnum a, fromEnum b), nat 1)
897− else ((fromEnum a, fromEnum b), nat 0)) $ combinations
898− mList = buildList combAp rrows
899− in tr $ fromLists mList
900− where
901− buildList [] _ = []
902− buildList l r = take r l : buildList (drop r l) r
934+fromFRel' = fromF'
903935
904936-- | Lifts functions to relations with dimensions matching @a@ and @b@
905937-- cardinality's.
906−fromFRel' ::
938+fromFRel ::
907939 forall a b.
908− ( Bounded a,
909− Bounded b,
910− Enum a,
911− Enum b,
912− Eq b,
913− KnownNat (Count (Normalize a)),
914− KnownNat (Count (Normalize b)),
915− FromLists (Natural 0 1) (Normalize b) (Normalize a)
940+ ( Liftable Boolean a b,
941+ CountableDimsN a b,
942+ FLN b a
916943 ) =>
917944 (a -> b) ->
918945 Relation (Normalize a) (Normalize b)
919−fromFRel' f =
920− let minA = minBound @a
921− maxA = maxBound @a
922− minB = minBound @b
923− maxB = maxBound @b
924− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
925− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
926− elementsA = take ccols [minA .. maxA]
927− elementsB = take rrows [minB .. maxB]
928− combinations = (,) <$> elementsA <*> elementsB
929− combAp = map snd . sort . map (\(a, b) -> if f a == b
930− then ((fromEnum a, fromEnum b), nat 1)
931− else ((fromEnum a, fromEnum b), nat 0)) $ combinations
932− mList = buildList combAp rrows
933− in tr $ fromLists mList
934− where
935− buildList [] _ = []
936− buildList l r = take r l : buildList (drop r l) r
946+fromFRel = fromFRel'
937947
938948-- | Lifts a relation function to a Boolean Matrix
939−toRel ::
949+toRel ::
940950 forall a b.
941951 ( Bounded a,
942952 Bounded b,
943953 Enum a,
944954 Enum b,
945955 Eq b,
946− KnownNat (Count (Normalize a)),
947− KnownNat (Count (Normalize b)),
948− FromLists (Natural 0 1) (Normalize b) (Normalize a)
949− )
956+ CountableDims a b,
957+ FLN b a
958+ )
950959 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
951960toRel f =
952961 let minA = minBound @a
953962 maxA = maxBound @a
954963 minB = minBound @b
955964 maxB = maxBound @b
956− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
957− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
965+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count a))
966+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count b))
958967 elementsA = take ccols [minA .. maxA]
959968 elementsB = take rrows [minB .. maxB]
960969 combinations = (,) <$> elementsA <*> elementsB
961− combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
962− then ((fromEnum a, fromEnum b), nat 1)
970+ combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
971+ then ((fromEnum a, fromEnum b), nat 1)
963972 else ((fromEnum a, fromEnum b), nat 0)) $ combinations
964973 mList = buildList combAp rrows
965974 in tr $ fromLists mList