@@ -1,3 +1,4 @@
1+{-# LANGUAGE StrictData #-}
1{-# LANGUAGE TypeFamilyDependencies #-}
2{-# LANGUAGE TypeFamilyDependencies #-}
2{-# LANGUAGE ConstraintKinds #-}
3{-# LANGUAGE ConstraintKinds #-}
3{-# LANGUAGE AllowAmbiguousTypes #-}
4{-# LANGUAGE AllowAmbiguousTypes #-}
@@ -29,7 +30,7 @@
29-- motivation behind the library, the underlying theory, and implementation details.
30-- motivation behind the library, the underlying theory, and implementation details.
31-- 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
32−-- Macedo (2012) and Oliveira (2012).
33+-- Macedo (2012) and Oliveira (2012).
34-- 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.
@@ -42,17 +43,26 @@ module LAoP.Matrix.Internal
43 -- There exists two type families that make it easier to write
44 -- There exists two type families that make it easier to write
44 -- matrix dimensions: 'FromNat' and 'Count'. This approach
45 -- matrix dimensions: 'FromNat' and 'Count'. This approach
45− -- leads to a very straightforward implementation
46+ -- leads to a very straightforward implementation
46− -- of LAoP combinators.
47+ -- of LAoP combinators.
48 -- * Type safe matrix representation
49 -- * Type safe matrix representation
49 Matrix (..),
50 Matrix (..),
52+ -- * Constraint type aliases
51 -- * Primitives
62 -- * Primitives
57 -- * Auxiliary type families
67 -- * Auxiliary type families
@@ -65,6 +75,7 @@ module LAoP.Matrix.Internal
67 matrixBuilder,
77 matrixBuilder,
@@ -75,28 +86,38 @@ module LAoP.Matrix.Internal
76 -- ** Get dimensions
87 -- ** Get dimensions
80 -- ** Matrix Transposition
93 -- ** Matrix Transposition
96+ -- ** Scalar multiplication/division of matrices
83 -- ** Selective operator
100 -- ** Selective operator
86 -- ** McCarthy's Conditional
104 -- ** McCarthy's Conditional
89 -- ** Matrix "abiding"
107 -- ** Matrix "abiding"
90− abideJS,
108+ abideJF,
91− abideSJ,
109+ abideFJ,
93 -- * Biproduct approach
114 -- * Biproduct approach
94− -- ** Split
115+ -- ** Fork
96 -- *** Projections
117 -- *** Projections
99− -- ** Junc
120+ -- ** Join
101 -- *** Injections
122 -- *** Injections
@@ -109,12 +130,13 @@ module LAoP.Matrix.Internal
110 -- | Note that given the restrictions imposed it is not possible to
131 -- | Note that given the restrictions imposed it is not possible to
111 -- implement the standard type classes present in standard Haskell.
132 -- implement the standard type classes present in standard Haskell.
112 -- *** Matrix pairing projections
134 -- *** Matrix pairing projections
116 -- *** Matrix pairing
138 -- *** Matrix pairing
119 -- * Matrix composition and lifting
141 -- * Matrix composition and lifting
@@ -122,10 +144,10 @@ module LAoP.Matrix.Internal
123 -- | Note that given the restrictions imposed it is not possible to
145 -- | Note that given the restrictions imposed it is not possible to
124 -- implement the standard type classes present in standard Haskell.
146 -- implement the standard type classes present in standard Haskell.
130 -- * Matrix printing
152 -- * Matrix printing
@@ -152,21 +174,22 @@ import LAoP.Utils.Internal
152import Data.Bool
174import Data.Bool
153import Data.Kind
175import Data.Kind
154import Data.List
176import Data.List
155import Data.Proxy
178import Data.Proxy
156import Data.Void
180import Data.Void
157import GHC.TypeLits
181import GHC.TypeLits
158import Data.Type.Equality
182import Data.Type.Equality
159import GHC.Generics
183import GHC.Generics
160import Control.DeepSeq
184import Control.DeepSeq
161−import Control.Category
185+import Prelude hiding (id, (.))
162−import Prelude hiding ((.))
186+import qualified Prelude (id, (.))
164-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
188-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
165data Matrix e cols rows where
189data Matrix e cols rows where
166− Empty :: Matrix e Void Void
167 One :: e -> Matrix e () ()
190 One :: e -> Matrix e () ()
168− Junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
191+ Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
169− Split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
192+ Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
171deriving instance (Show e) => Show (Matrix e cols rows)
194deriving instance (Show e) => Show (Matrix e cols rows)
@@ -193,205 +216,197 @@ type family Count (d :: Type) :: Nat where
194-- Thanks to Li-Yao Xia this type family is super fast.
217-- Thanks to Li-Yao Xia this type family is super fast.
195type family FromNat (n :: Nat) :: Type where
218type family FromNat (n :: Nat) :: Type where
197 FromNat 1 = ()
219 FromNat 1 = ()
198 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
220 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
200type family FromNat' (b :: Bool) (m :: Type) :: Type where
222type family FromNat' (b :: Bool) (m :: Type) :: Type where
201− FromNat' 'True m = Either m m
223+ FromNat' 'True m = Either m m
202 FromNat' 'False m = Either () (Either m m)
224 FromNat' 'False m = Either () (Either m m)
204-- | Type family that normalizes the representation of a given data
226-- | Type family that normalizes the representation of a given data
205-- structure
227-- structure
206type family Normalize (d :: Type) :: Type where
228type family Normalize (d :: Type) :: Type where
229+ Normalize (Either a b) = Either (Normalize a) (Normalize b)
207− Normalize d = FromNat (Count d)
230+ Normalize d = FromNat (Count d)
209-- | Constraint type synonyms to keep the type signatures less convoluted
232-- | Constraint type synonyms to keep the type signatures less convoluted
210type Countable a = KnownNat (Count a)
233type Countable a = KnownNat (Count a)
211type CountableN a = KnownNat (Count (Normalize a))
234type CountableN a = KnownNat (Count (Normalize a))
212−type CountableDimensions a b = (Countable a, Countable b)
235+type CountableDims a b = (Countable a, Countable b)
213−type CountableDimensionsN a b = (CountableN a, CountableN b)
236+type CountableDimsN a b = (CountableN a, CountableN b)
237+type FL a b = FromLists a b
214−type FromListsN e a b = FromLists e (Normalize a) (Normalize b)
238+type FLN a b = FromLists (Normalize a) (Normalize b)
215type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
239type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
240+type Trivial a = FromNat (Count a) ~ a
217−-- | It isn't possible to implement the 'id' function so it's
242+-- | It is possible to implement a constrained version of the category type
218−-- implementation is 'undefined'. However 'comp' can be and this partial
243+-- class.
219−-- class implementation exists just to make the code more readable.
221−-- Please use 'identity' instead.
222instance (Num e) => Category (Matrix e) where
244instance (Num e) => Category (Matrix e) where
223− id = undefined
245+ type Object (Matrix e) a = (FL a a, Countable a)
224− (.) = comp
247+ (.) = comp
226instance NFData e => NFData (Matrix e cols rows) where
249instance NFData e => NFData (Matrix e cols rows) where
228− rnf (One e) = rnf e
250+ rnf (One e) = rnf e
229− rnf (Junc a b) = rnf a `seq` rnf b
251+ rnf (Join a b) = rnf a `seq` rnf b
230− rnf (Split a b) = rnf a `seq` rnf b
252+ rnf (Fork a b) = rnf a `seq` rnf b
232instance Eq e => Eq (Matrix e cols rows) where
254instance Eq e => Eq (Matrix e cols rows) where
233− Empty == Empty = True
234− (One a) == (One b) = a == b
255+ (One a) == (One b) = a == b
235− (Junc a b) == (Junc c d) = a == c && b == d
256+ (Join a b) == (Join c d) = a == c && b == d
236− (Split a b) == (Split c d) = a == c && b == d
257+ (Fork a b) == (Fork c d) = a == c && b == d
237− x@(Split _ _) == y@(Junc _ _) = x == abideJS y
258+ x@(Fork _ _) == y@(Join _ _) = x == abideJF y
238− x@(Junc _ _) == y@(Split _ _) = abideJS x == y
259+ x@(Join _ _) == y@(Fork _ _) = abideJF x == y
240instance Num e => Num (Matrix e cols rows) where
261instance Num e => Num (Matrix e cols rows) where
262+ a + b = zipWithM (+) a b
264+ a - b = zipWithM (-) a b
266+ a * b = zipWithM (*) a b
242− Empty + Empty = Empty
243− (One a) + (One b) = One (a + b)
244− (Junc a b) + (Junc c d) = Junc (a + c) (b + d)
245− (Split a b) + (Split c d) = Split (a + c) (b + d)
246− x@(Split _ _) + y@(Junc _ _) = x + abideJS y
247− x@(Junc _ _) + y@(Split _ _) = abideJS x + y
249− Empty - Empty = Empty
250− (One a) - (One b) = One (a - b)
251− (Junc a b) - (Junc c d) = Junc (a - c) (b - d)
252− (Split a b) - (Split c d) = Split (a - c) (b - d)
253− x@(Split _ _) - y@(Junc _ _) = x - abideJS y
254− x@(Junc _ _) - y@(Split _ _) = abideJS x - y
256− Empty * Empty = Empty
257− (One a) * (One b) = One (a * b)
258− (Junc a b) * (Junc c d) = Junc (a * c) (b * d)
259− (Split a b) * (Split c d) = Split (a * c) (b * d)
260− x@(Split _ _) * y@(Junc _ _) = x * abideJS y
261− x@(Junc _ _) * y@(Split _ _) = abideJS x * y
264− abs (One a) = One (abs a)
268+ abs (One a) = One (abs a)
265− abs (Junc a b) = Junc (abs a) (abs b)
269+ abs (Join a b) = Join (abs a) (abs b)
266− abs (Split a b) = Split (abs a) (abs b)
270+ abs (Fork a b) = Fork (abs a) (abs b)
268− signum Empty = Empty
269− signum (One a) = One (signum a)
272+ signum (One a) = One (signum a)
270− signum (Junc a b) = Junc (signum a) (signum b)
273+ signum (Join a b) = Join (signum a) (signum b)
271− signum (Split a b) = Split (signum a) (signum b)
274+ signum (Fork a b) = Fork (signum a) (signum b)
273instance Ord e => Ord (Matrix e cols rows) where
276instance Ord e => Ord (Matrix e cols rows) where
274− Empty <= Empty = True
275− (One a) <= (One b) = a <= b
277+ (One a) <= (One b) = a <= b
276− (Junc a b) <= (Junc c d) = (a <= c) && (b <= d)
278+ (Join a b) <= (Join c d) = (a <= c) && (b <= d)
277− (Split a b) <= (Split c d) = (a <= c) && (b <= d)
279+ (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
278− x@(Split _ _) <= y@(Junc _ _) = x <= abideJS y
280+ x@(Fork _ _) <= y@(Join _ _) = x <= abideJF y
279− x@(Junc _ _) <= y@(Split _ _) = abideJS x <= y
281+ x@(Join _ _) <= y@(Fork _ _) = abideJF x <= y
281-- Primitives
283-- Primitives
283−-- | Empty matrix constructor
284−empty :: Matrix e Void Void
287-- | Unit matrix constructor
285-- | Unit matrix constructor
288one :: e -> Matrix e () ()
286one :: e -> Matrix e () ()
291−-- | Matrix 'Junc' constructor
289+-- | Matrix 'Join' constructor
292−junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
290+join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
293−junc = Junc
291+join = Join
295infixl 3 |||
293infixl 3 |||
297−-- | Matrix 'Junc' constructor
295+-- | Matrix 'Join' constructor
298(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
296(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
299−(|||) = Junc
297+(|||) = Join
301−-- | Matrix 'Split' constructor
299+-- | Matrix 'Fork' constructor
302−split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
300+fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
303−split = Split
301+fork = Fork
305infixl 2 ===
303infixl 2 ===
307−-- | Matrix 'Split' constructor
305+-- | Matrix 'Fork' constructor
308(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
306(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
309−(===) = Split
307+(===) = Fork
311-- Construction
309-- Construction
313-- | Type class for defining the 'fromList' conversion function.
311-- | Type class for defining the 'fromList' conversion function.
315-- Given that it is not possible to branch on types at the term level type
313-- Given that it is not possible to branch on types at the term level type
316−-- classes are needed bery much like an inductive definition but on types.
314+-- classes are needed very much like an inductive definition but on types.
317−class FromLists e cols rows where
315+class FromLists cols rows where
318 -- | Build a matrix out of a list of list of elements. Throws a runtime
316 -- | Build a matrix out of a list of list of elements. Throws a runtime
319 -- error if the dimensions do not match.
317 -- error if the dimensions do not match.
320 fromLists :: [[e]] -> Matrix e cols rows
318 fromLists :: [[e]] -> Matrix e cols rows
322−instance FromLists e Void Void where
320+instance FromLists () () where
323− fromLists [] = Empty
324− fromLists _ = error "Wrong dimensions"
326−instance {-# OVERLAPPING #-} FromLists e () () where
327 fromLists [[e]] = One e
321 fromLists [[e]] = One e
328 fromLists _ = error "Wrong dimensions"
322 fromLists _ = error "Wrong dimensions"
330−instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
324+instance (FromLists cols ()) => FromLists (Either () cols) () where
331− fromLists [h : t] = Junc (One h) (fromLists [t])
325+ fromLists [h : t] = Join (One h) (fromLists [t])
332 fromLists _ = error "Wrong dimensions"
326 fromLists _ = error "Wrong dimensions"
328+instance {-# OVERLAPPABLE #-}
334−instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), Countable a) => FromLists e (Either a b) () where
329+ (FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () where
335− fromLists [l] =
330+ fromLists [l] =
336 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
331 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
337− in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])
332+ in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
338 fromLists _ = error "Wrong dimensions"
333 fromLists _ = error "Wrong dimensions"
340−instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
335+instance (FromLists () rows) => FromLists () (Either () rows) where
341− fromLists ([h] : t) = Split (One h) (fromLists t)
336+ fromLists ([h] : t) = Fork (One h) (fromLists t)
342 fromLists _ = error "Wrong dimensions"
337 fromLists _ = error "Wrong dimensions"
339+instance {-# OVERLAPPABLE #-}
344−instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, Countable a) => FromLists e () (Either a b) where
340+ (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where
345− fromLists l@([_] : _) =
341+ fromLists l@([_] : _) =
346 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
342 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
347− in Split (fromLists (take rowsA l)) (fromLists (drop rowsA l))
343+ in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
348 fromLists _ = error "Wrong dimensions"
344 fromLists _ = error "Wrong dimensions"
350−instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a b) d, Countable c) => FromLists e (Either a b) (Either c d) where
346+instance (FromLists (Either a b) c, FromLists (Either a b) d, Countable c)
347+ => FromLists (Either a b) (Either c d) where
351 fromLists l@(h : t) =
348 fromLists l@(h : t) =
352 let lh = length h
349 let lh = length h
353 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
350 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
354− condition = all (== lh) (map length t)
351+ condition = all ((== lh) . length) t
355 in if lh > 0 && condition
352 in if lh > 0 && condition
356− then Split (fromLists (take rowsC l)) (fromLists (drop rowsC l))
353+ then Fork (fromLists (take rowsC l)) (fromLists (drop rowsC l))
357 else error "Not all rows have the same length"
354 else error "Not all rows have the same length"
359-- | Matrix builder function. Constructs a matrix provided with
356-- | Matrix builder function. Constructs a matrix provided with
360−-- a construction function.
357+-- a construction function that operates with indices.
361−matrixBuilder ::
358+matrixBuilder' ::
362 forall e cols rows.
359 forall e cols rows.
363− ( FromLists e cols rows,
360+ ( FL cols rows,
364− CountableDimensions cols rows
361+ CountableDims cols rows
366− ((Int, Int) -> e) ->
367− Matrix e cols rows
362+ ) => ((Int, Int) -> e) -> Matrix e cols rows
368−matrixBuilder f =
363+matrixBuilder' f =
369 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
364 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
370 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
365 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
371 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
366 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
372 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
367 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)
374-- | Constructs a column vector matrix
389-- | Constructs a column vector matrix
375−col :: (FromLists e () rows) => [e] -> Matrix e () rows
390+col :: (FL () rows) => [e] -> Matrix e () rows
376col = fromLists . map (: [])
391col = fromLists . map (: [])
378-- | Constructs a row vector matrix
393-- | Constructs a row vector matrix
379−row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
394+row :: (FL cols ()) => [e] -> Matrix e cols ()
380row = fromLists . (: [])
395row = fromLists . (: [])
382-- | Lifts functions to matrices with arbitrary dimensions.
397-- | Lifts functions to matrices with arbitrary dimensions.
384-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
399-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
385-- types @a@ or @b@ allows.
400-- types @a@ or @b@ allows.
386−fromF ::
401+fromF' ::
387 forall a b cols rows e.
402 forall a b cols rows e.
388 ( Liftable e a b,
403 ( Liftable e a b,
389− CountableDimensions cols rows,
404+ CountableDims cols rows,
390− FromLists e rows cols
405+ FL rows cols
392 (a -> b) ->
407 (a -> b) ->
393 Matrix e cols rows
408 Matrix e cols rows
394−fromF f =
409+fromF' f =
395 let minA = minBound @a
410 let minA = minBound @a
396 maxA = maxBound @a
411 maxA = maxBound @a
397 minB = minBound @b
412 minB = minBound @b
@@ -401,8 +416,8 @@ fromF f =
401 elementsA = take ccols [minA .. maxA]
416 elementsA = take ccols [minA .. maxA]
402 elementsB = take rrows [minB .. maxB]
417 elementsB = take rrows [minB .. maxB]
403 combinations = (,) <$> elementsA <*> elementsB
418 combinations = (,) <$> elementsA <*> elementsB
404− combAp = map snd . sort . map (\(a, b) -> if f a == b
419+ combAp = map snd . sort . map (\(a, b) -> if f a == b
405− then ((fromEnum a, fromEnum b), 1)
420+ then ((fromEnum a, fromEnum b), 1)
406 else ((fromEnum a, fromEnum b), 0)) $ combinations
421 else ((fromEnum a, fromEnum b), 0)) $ combinations
407 mList = buildList combAp rrows
422 mList = buildList combAp rrows
408 in tr $ fromLists mList
423 in tr $ fromLists mList
@@ -412,41 +427,23 @@ fromF f =
413-- | Lifts functions to matrices with dimensions matching @a@ and @b@
428-- | Lifts functions to matrices with dimensions matching @a@ and @b@
414-- cardinality's.
429-- cardinality's.
415−fromF' ::
430+fromF ::
416 forall a b e.
431 forall a b e.
417 ( Liftable e a b,
432 ( Liftable e a b,
418− CountableDimensionsN a b,
433+ CountableDimsN a b,
419− FromListsN e b a
434+ FLN b a
421 (a -> b) ->
436 (a -> b) ->
422 Matrix e (Normalize a) (Normalize b)
437 Matrix e (Normalize a) (Normalize b)
423−fromF' f =
438+fromF = fromF'
424− let minA = minBound @a
428− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
429− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
430− elementsA = take ccols [minA .. maxA]
431− elementsB = take rrows [minB .. maxB]
432− combinations = (,) <$> elementsA <*> elementsB
433− combAp = map snd . sort . map (\(a, b) -> if f a == b
434− then ((fromEnum a, fromEnum b), 1)
435− else ((fromEnum a, fromEnum b), 0)) $ combinations
436− mList = buildList combAp rrows
437− in tr $ fromLists mList
440− buildList l r = take r l : buildList (drop r l) r
442-- Conversion
440-- Conversion
444-- | Converts a matrix to a list of lists of elements.
442-- | Converts a matrix to a list of lists of elements.
445toLists :: Matrix e cols rows -> [[e]]
443toLists :: Matrix e cols rows -> [[e]]
447toLists (One e) = [[e]]
444toLists (One e) = [[e]]
448−toLists (Split l r) = toLists l ++ toLists r
445+toLists (Fork l r) = toLists l ++ toLists r
449−toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
446+toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
451-- | Converts a matrix to a list of elements.
448-- | Converts a matrix to a list of elements.
452toList :: Matrix e cols rows -> [e]
449toList :: Matrix e cols rows -> [e]
@@ -455,37 +452,38 @@ toList = concat . toLists
455-- Zeros Matrix
452-- Zeros Matrix
457-- | The zero matrix. A matrix wholly filled with zeros.
454-- | The zero matrix. A matrix wholly filled with zeros.
458−zeros :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows
455+zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
459−zeros = matrixBuilder (const 0)
456+zeros = matrixBuilder' (const 0)
461-- Ones Matrix
458-- Ones Matrix
463-- | The ones matrix. A matrix wholly filled with ones.
460-- | The ones matrix. A matrix wholly filled with ones.
465-- Also known as T (Top) matrix.
462-- Also known as T (Top) matrix.
466−ones :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows
463+ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
467−ones = matrixBuilder (const 1)
464+ones = matrixBuilder' (const 1)
469-- Const Matrix
466-- Const Matrix
471-- | The constant matrix constructor. A matrix wholly filled with a given
468-- | The constant matrix constructor. A matrix wholly filled with a given
473−constant :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => e -> Matrix e cols rows
470+constant :: (Num e, FL cols rows, CountableDims cols rows) => e -> Matrix e cols rows
474−constant e = matrixBuilder (const e)
471+constant e = matrixBuilder' (const e)
476-- Bang Matrix
473-- Bang Matrix
478-- | The T (Top) row vector matrix.
475-- | The T (Top) row vector matrix.
479−bang :: forall e cols. (Num e, Enum e, FromLists e cols (), Countable cols) => Matrix e cols ()
476+bang :: forall e cols. (Num e, Enum e, FL cols (), Countable cols) => Matrix e cols ()
481 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
478 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
482 in fromLists [take c [1, 1 ..]]
479 in fromLists [take c [1, 1 ..]]
484−-- Identity Matrix
481+-- iden Matrix
486−-- | Identity matrix.
483+-- | iden matrix.
487−identity :: (Num e, FromLists e cols cols, Countable cols) => Matrix e cols cols
484+iden :: forall e cols . (Num e, FL cols cols, Countable cols) => Matrix e cols cols
488−identity = matrixBuilder (bool 0 1 . uncurry (==))
485+iden = matrixBuilder' (bool 0 1 . uncurry (==))
486+{-# NOINLINE iden #-}
490-- Matrix composition (MMM)
488-- Matrix composition (MMM)
@@ -494,60 +492,90 @@ identity = matrixBuilder (bool 0 1 . uncurry (==))
494-- This definition takes advantage of divide-and-conquer and fusion laws
492-- This definition takes advantage of divide-and-conquer and fusion laws
495-- from LAoP.
493-- from LAoP.
496comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
494comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
497−comp Empty Empty = Empty
498−comp (One a) (One b) = One (a * b)
495+comp (One a) (One b) = One (a * b)
499−comp (Junc a b) (Split c d) = comp a c + comp b d -- Divide-and-conquer law
496+comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
500−comp (Split a b) c = Split (comp a c) (comp b c) -- Split fusion law
497+comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
501−comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc fusion law
498+comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
499+{-# NOINLINE comp #-}
501+ "comp/iden1" forall m. comp m iden = m ;
502+ "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)
503-- Projections
523-- Projections
505-- | Biproduct first component projection
525-- | Biproduct first component projection
506−p1 :: forall e m n. (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e (Either m n) m
526+p1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e (Either m n) m
507−p1 =
527+p1 = join id zeros
508− let iden = identity :: Matrix e m m
509− zero = zeros :: Matrix e n m
512-- | Biproduct second component projection
529-- | Biproduct second component projection
513−p2 :: forall e m n. (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e (Either m n) n
530+p2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e (Either m n) n
514−p2 =
531+p2 = join zeros id
515− let iden = identity :: Matrix e n n
516− zero = zeros :: Matrix e m n
519-- Injections
533-- Injections
521-- | Biproduct first component injection
535-- | Biproduct first component injection
522−i1 :: (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
536+i1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e m (Either m n)
523i1 = tr p1
537i1 = tr p1
525-- | Biproduct second component injection
539-- | Biproduct second component injection
526−i2 :: (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
540+i2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e n (Either m n)
527i2 = tr p2
541i2 = tr p2
529-- Dimensions
543-- Dimensions
531-- | Obtain the number of rows.
545-- | Obtain the number of rows.
533−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
547+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
534−-- dimensions in constant time.
548+-- dimensions in constant time. For a version that doesn't require the
535−--
549+-- constraint see 'rows''.
536−-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
537−-- exchange for performance.
538rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
550rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
539rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
551rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
553+-- | Obtain the number of rows in an inefficient manner, but without any
556+-- For a more efficient version see 'rows'.
557+rows' :: Matrix e cols rows -> Int
559+rows' (Join lhs _) = rows' lhs
560+rows' (Fork top bottom) = rows' top + rows' bottom
541-- | Obtain the number of columns.
562-- | Obtain the number of columns.
543−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
544−-- dimensions in constant time.
546−-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
564+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
547−-- exchange for performance.
565+-- dimensions in constant time. For a version that doesn't require the
566+-- constraint see 'columns''.
548columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
567columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
549columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
568columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
570+-- | Obtain the number of columns in an inefficient manner, but without any
573+-- For a more efficient version see 'columns'.
574+columns' :: Matrix e cols rows -> Int
576+columns' (Join lhs rhs) = columns' lhs + columns' rhs
577+columns' (Fork top _) = columns' top
551-- Coproduct Bifunctor
579-- Coproduct Bifunctor
553infixl 5 -|-
581infixl 5 -|-
@@ -556,150 +584,172 @@ infixl 5 -|-
557 forall e n k m j.
585 forall e n k m j.
559− CountableDimensions j k,
587+ CountableDims j k,
560− FromLists e k k,
588+ FL k k,
561− FromLists e j k,
589+ FL j k,
562− FromLists e k j,
590+ FL k j,
563− FromLists e j j
591+ FL j j
565 Matrix e n k ->
593 Matrix e n k ->
566 Matrix e m j ->
594 Matrix e m j ->
567 Matrix e (Either n m) (Either k j)
595 Matrix e (Either n m) (Either k j)
568−(-|-) a b = Junc (i1 . a) (i2 . b)
596+(-|-) a b = Join (i1 . a) (i2 . b)
570-- Khatri Rao Product and projections
598-- Khatri Rao Product and projections
572-- | Khatri Rao product first component projection matrix.
600-- | Khatri Rao product first component projection matrix.
574 forall e m k .
602 forall e m k .
576− CountableDimensions k m,
604+ CountableDims k m,
577− FromLists e (Normalize (m, k)) m,
605+ FL (Normalize (m, k)) m,
578 CountableN (m, k)
606 CountableN (m, k)
579 ) => Matrix e (Normalize (m, k)) m
607 ) => Matrix e (Normalize (m, k)) m
580−kp1 = matrixBuilder f
608+fstM = matrixBuilder' f
582 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
610 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
584 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
612 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
585− | otherwise = 0
613+ | otherwise = 0
587-- | Khatri Rao product second component projection matrix.
615-- | Khatri Rao product second component projection matrix.
589 forall e m k .
617 forall e m k .
591− CountableDimensions k m,
619+ CountableDims k m,
592− FromLists e (Normalize (m, k)) k,
620+ FL (Normalize (m, k)) k,
593 CountableN (m, k)
621 CountableN (m, k)
594 ) => Matrix e (Normalize (m, k)) k
622 ) => Matrix e (Normalize (m, k)) k
595−kp2 = matrixBuilder f
623+sndM = matrixBuilder' f
597 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
625 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
599 | x == y || mod (y - x) offset == 0 = 1
627 | x == y || mod (y - x) offset == 0 = 1
600− | otherwise = 0
628+ | otherwise = 0
602-- | Khatri Rao Matrix product also known as matrix pairing.
630-- | Khatri Rao Matrix product also known as matrix pairing.
604-- NOTE: That this is not a true categorical product, see for instance:
632-- NOTE: That this is not a true categorical product, see for instance:
607−-- | kp1 . khatri a b == a
635+-- | fstM . kr a b == a
608−-- khatri a b ==> |
636+-- kr a b ==> |
609−-- | kp2 . khatri a b == b
637+-- | sndM . kr a b == b
612-- __Emphasis__ on the implication symbol.
640-- __Emphasis__ on the implication symbol.
614− forall e cols a b.
642+ forall e cols a b.
616− CountableDimensions a b,
644+ CountableDims a b,
617 CountableN (a, b),
645 CountableN (a, b),
618− FromLists e (Normalize (a, b)) a,
646+ FL (Normalize (a, b)) a,
619− FromLists e (Normalize (a, b)) b
647+ FL (Normalize (a, b)) b
620 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
648 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
621−khatri a b =
649+kr a b =
622− let kp1' = kp1 @e @a @b
650+ let fstM' = fstM @e @a @b
623− kp2' = kp2 @e @a @b
651+ sndM' = sndM @e @a @b
624− in (tr kp1') . a * (tr kp2') . b
652+ in (tr fstM' . a) * (tr sndM' . b)
626-- Product Bifunctor (Kronecker)
654-- Product Bifunctor (Kronecker)
628infixl 4 ><
656infixl 4 ><
630-- | Matrix product functor also known as kronecker product
658-- | Matrix product functor also known as kronecker product
632− forall e m p n q.
660+ forall e m p n q.
634− CountableDimensions m n,
662+ CountableDims m n,
635− CountableDimensions p q,
663+ CountableDims p q,
636− CountableDimensionsN (m, n) (p, q),
664+ CountableDimsN (m, n) (p, q),
637− FromLists e (Normalize (m, n)) m,
665+ FL (Normalize (m, n)) m,
638− FromLists e (Normalize (m, n)) n,
666+ FL (Normalize (m, n)) n,
639− FromLists e (Normalize (p, q)) p,
667+ FL (Normalize (p, q)) p,
640− FromLists e (Normalize (p, q)) q
668+ FL (Normalize (p, q)) q
642 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
670 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
643(><) a b =
671(><) a b =
644− let kp1' = kp1 @e @m @n
672+ let fstM' = fstM @e @m @n
645− kp2' = kp2 @e @m @n
673+ sndM' = sndM @e @m @n
646− in khatri (a . kp1') (b . kp2')
674+ in kr (a . fstM') (b . sndM')
648−-- Matrix abide Junc Split
676+-- Matrix abide Join Fork
650−-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
678+-- | Matrix "abiding" following the 'Join'-'Fork' exchange law.
655−-- '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)
657−abideJS :: Matrix e cols rows -> Matrix e cols rows
685+abideJF :: Matrix e cols rows -> Matrix e cols rows
658−abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law
686+abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
659−abideJS Empty = Empty
660−abideJS (One e) = One e
687+abideJF (One e) = One e
661−abideJS (Junc a b) = Junc (abideJS a) (abideJS b)
688+abideJF (Join a b) = Join (abideJF a) (abideJF b)
662−abideJS (Split a b) = Split (abideJS a) (abideJS b)
689+abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
664−-- Matrix abide Split Junc
691+-- Matrix abide Fork Join
666−-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
693+-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
669−-- '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)
671−abideSJ :: Matrix e cols rows -> Matrix e cols rows
698+abideFJ :: Matrix e cols rows -> Matrix e cols rows
672−abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law
699+abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law
673−abideSJ Empty = Empty
674−abideSJ (One e) = One e
700+abideFJ (One e) = One e
675−abideSJ (Junc a b) = Junc (abideSJ a) (abideSJ b)
701+abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
676−abideSJ (Split a b) = Split (abideSJ a) (abideSJ b)
702+abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
678-- Matrix transposition
704-- Matrix transposition
680-- | Matrix transposition.
706-- | Matrix transposition.
681tr :: Matrix e cols rows -> Matrix e rows cols
707tr :: Matrix e cols rows -> Matrix e rows cols
683−tr (One e) = One e
708+tr (One e) = One e
684−tr (Junc a b) = Split (tr a) (tr b)
709+tr (Join a b) = Fork (tr a) (tr b)
685−tr (Split a b) = Junc (tr a) (tr b)
710+tr (Fork a b) = Join (tr a) (tr b)
687-- Selective 'select' operator
712-- Selective 'select' operator
689-- | Selective functors 'select' operator equivalent inspired by the
714-- | Selective functors 'select' operator equivalent inspired by the
690-- ArrowMonad solution presented in the paper.
715-- ArrowMonad solution presented in the paper.
691−select :: (Num e, FromLists e b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
716+select :: (Num e, FL b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
692−select m y = junc y identity . m
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
724+ CountableDims c (Either b c),
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
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)
694-- McCarthy's Conditional
744-- McCarthy's Conditional
696-- | McCarthy's Conditional expresses probabilistic choice.
746-- | McCarthy's Conditional expresses probabilistic choice.
698− ( cols ~ Normalize cols,
748+ ( Trivial cols,
699 Countable cols,
749 Countable cols,
700− FromLists e () cols,
750+ FL () cols,
701− FromLists e cols (),
751+ FL cols (),
702− FromLists e cols cols,
752+ FL cols cols,
703 Bounded a,
753 Bounded a,
@@ -707,14 +757,14 @@ cond ::
709 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
759 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
710−cond p f g = junc f g . grd p
760+cond p f g = join f g . grd p
713− ( q ~ Normalize q,
763+ ( Trivial q,
714 Countable q,
764 Countable q,
715− FromLists e () q,
765+ FL () q,
716− FromLists e q (),
766+ FL q (),
717− FromLists e q q,
767+ FL q q,
718 Bounded a,
768 Bounded a,
@@ -722,60 +772,86 @@ grd ::
724 (a -> Bool) -> Matrix e q (Either q q)
774 (a -> Bool) -> Matrix e q (Either q q)
725−grd f = split (corr f) (corr (not . f))
775+grd f = fork (corr f) (corr (not . f))
728− forall e a q .
778+ forall e a q .
729− ( q ~ Normalize q,
779+ ( Trivial q,
730 Countable q,
780 Countable q,
731− FromLists e () q,
781+ FL () q,
732− FromLists e q (),
782+ FL q (),
733− FromLists e q q,
783+ FL q q,
734 Liftable e a Bool
784 Liftable e a Bool
736 => (a -> Bool) -> Matrix e q q
786 => (a -> Bool) -> Matrix e q q
737−corr p = let f = fromF p :: Matrix e q ()
787+corr p = let f = fromF' p :: Matrix e q ()
738− in khatri f (identity :: Matrix e q q)
788+ in kr f (id :: Matrix e q q)
740-- Pretty print
790-- Pretty print
742prettyAux :: Show e => [[e]] -> [[e]] -> String
792prettyAux :: Show e => [[e]] -> [[e]] -> String
743prettyAux [] _ = ""
793prettyAux [] _ = ""
744−prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
794+prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
746 v = fmap show m
796 v = fmap show m
747 widest = maximum $ fmap length v
797 widest = maximum $ fmap length v
748 fill str = replicate (widest - length str - 2) ' ' ++ str
798 fill str = replicate (widest - length str - 2) ' ' ++ str
749−prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
799+prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
751− v = fmap show m
801+ v = fmap show m
752− widest = maximum $ fmap length v
802+ widest = maximum $ fmap length v
753 fill str = replicate (widest - length str - 2) ' ' ++ str
803 fill str = replicate (widest - length str - 2) ' ' ++ str
754−prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
804+prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
755 prettyAux t l
805 prettyAux t l
757− v = fmap show l
807+ v = fmap show l
758− widest = maximum $ fmap length v
808+ widest = maximum $ fmap length v
759 fill str = replicate (widest - length str - 2) ' ' ++ str
809 fill str = replicate (widest - length str - 2) ' ' ++ str
761-- | Matrix pretty printer
811-- | Matrix pretty printer
762−pretty :: (Countable cols, Show e) => Matrix e cols rows -> String
812+pretty :: (CountableDims cols rows, Show e) => Matrix e cols rows -> String
763−pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
814+ [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"
764− prettyAux (toLists m) (toLists m) ++
815+ , unlines
816+ [ "│ " ++ unwords (fmap (\j -> fill $ show $ getElem i j m) [1..columns m]) ++ " │" | i <- [1..rows m] ]
765− "└ " ++ unwords (replicate (columns m) blank) ++ " ┘"
817+ , "└ ", unwords (replicate (columns m) blank), " ┘"
767− v = fmap show (toList m)
820+ strings = map show (toList m)
768− widest = maximum $ fmap length v
821+ widest = maximum $ map length strings
769 fill str = replicate (widest - length str) ' ' ++ str
822 fill str = replicate (widest - length str) ' ' ++ str
770− blank = fill ""
823+ blank = fill ""
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
832+ "getElem: Trying to get the "
834+ ++ " element from a "
835+ ++ show (rows m) ++ "x" ++ show (columns m)
772-- | Matrix pretty printer
840-- | Matrix pretty printer
773−prettyPrint :: (Countable cols, Show e) => Matrix e cols rows -> IO ()
841+prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()
774prettyPrint = putStrLn . pretty
842prettyPrint = putStrLn . pretty
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
776-- Relational operators functions
852-- Relational operators functions
778−type Boolean = Natural 0 1
854+type Boolean = Natural 0 1
779type Relation a b = Matrix Boolean a b
855type Relation a b = Matrix Boolean a b
781-- | Helper conversion function
857-- | Helper conversion function
@@ -791,54 +867,47 @@ fromBool False = nat 0
792-- | Relational negation
868-- | Relational negation
793negateM :: Relation cols rows -> Relation cols rows
869negateM :: Relation cols rows -> Relation cols rows
794−negateM Empty = Empty
795−negateM (One (Nat 0)) = One (Nat 1)
870+negateM (One (Nat p)) = One (Nat (negate p))
796−negateM (One (Nat 1)) = One (Nat 0)
797−negateM (Junc a b) = Junc (negateM a) (negateM b)
871+negateM (Join a b) = Join (negateM a) (negateM b)
798−negateM (Split a b) = Split (negateM a) (negateM b)
872+negateM (Fork a b) = Fork (negateM a) (negateM b)
800-- | Relational addition
874-- | Relational addition
801orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
875orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
802−orM Empty Empty = Empty
803−orM (One a) (One b) = One (fromBool (toBool a || toBool b))
876+orM (One a) (One b) = One (fromBool (toBool a || toBool b))
804−orM (Junc a b) (Junc c d) = Junc (orM a c) (orM b d)
877+orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
805−orM (Split a b) (Split c d) = Split (orM a c) (orM b d)
878+orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
806−orM x@(Split _ _) y@(Junc _ _) = orM x (abideJS y)
879+orM x@(Fork _ _) y@(Join _ _) = orM x (abideJF y)
807−orM x@(Junc _ _) y@(Split _ _) = orM (abideJS x) y
880+orM x@(Join _ _) y@(Fork _ _) = orM (abideJF x) y
809-- | Relational multiplication
882-- | Relational multiplication
810andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
883andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
811−andM Empty Empty = Empty
812−andM (One a) (One b) = One (fromBool (toBool a && toBool b))
884+andM (One a) (One b) = One (fromBool (toBool a && toBool b))
813−andM (Junc a b) (Junc c d) = Junc (andM a c) (andM b d)
885+andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
814−andM (Split a b) (Split c d) = Split (andM a c) (andM b d)
886+andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
815−andM x@(Split _ _) y@(Junc _ _) = andM x (abideJS y)
887+andM x@(Fork _ _) y@(Join _ _) = andM x (abideJF y)
816−andM x@(Junc _ _) y@(Split _ _) = andM (abideJS x) y
888+andM x@(Join _ _) y@(Fork _ _) = andM (abideJF x) y
818-- | Relational subtraction
890-- | Relational subtraction
819subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
891subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
820−subM Empty Empty = Empty
821−subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
892+subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
822−subM (Junc a b) (Junc c d) = Junc (subM a c) (subM b d)
893+subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
823−subM (Split a b) (Split c d) = Split (subM a c) (subM b d)
894+subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
824−subM x@(Split _ _) y@(Junc _ _) = subM x (abideJS y)
895+subM x@(Fork _ _) y@(Join _ _) = subM x (abideJF y)
825−subM x@(Junc _ _) y@(Split _ _) = subM (abideJS x) y
896+subM x@(Join _ _) y@(Fork _ _) = subM (abideJF x) y
827-- | Matrix relational composition.
898-- | Matrix relational composition.
828compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
899compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
829−compRel Empty Empty = Empty
830−compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
900+compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
831−compRel (Junc a b) (Split c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
901+compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
832−compRel (Split a b) c = Split (compRel a c) (compRel b c) -- Split fusion law
902+compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
833−compRel c (Junc a b) = Junc (compRel c a) (compRel c b) -- Junc fusion law
903+compRel c (Join a b) = Join (compRel c a) (compRel c b) -- Join fusion law
835-- | Matrix relational right division
905-- | Matrix relational right division
836divR :: Relation b c -> Relation b a -> Relation a c
906divR :: Relation b c -> Relation b a -> Relation a c
837−divR Empty Empty = Empty
838divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
907divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
839−divR (Junc a b) (Junc c d) = andM (divR a c) (divR b d)
908+divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
840−divR (Split a b) c = Split (divR a c) (divR b c)
909+divR (Fork a b) c = Fork (divR a c) (divR b c)
841−divR c (Split a b) = Junc (divR c a) (divR c b)
910+divR c (Fork a b) = Join (divR c a) (divR c b)
843-- | Matrix relational left division
912-- | Matrix relational left division
844divL :: Relation c b -> Relation a b -> Relation a c
913divL :: Relation c b -> Relation a b -> Relation a c
@@ -854,86 +923,52 @@ divS s r = divL r s `intersection` divR (tr r) (tr s)
855-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
924-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
856-- types @a@ or @b@ allows.
925-- types @a@ or @b@ allows.
857−fromFRel ::
926+fromFRel' ::
858 forall a b cols rows.
927 forall a b cols rows.
859 ( Liftable Boolean a b,
928 ( Liftable Boolean a b,
860− CountableDimensions cols rows,
929+ CountableDims cols rows,
861− FromLists Boolean rows cols
930+ FL rows cols
863 (a -> b) ->
932 (a -> b) ->
864 Relation cols rows
933 Relation cols rows
865−fromFRel f =
934+fromFRel' = fromF'
866− let minA = minBound @a
870− ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
871− rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
872− elementsA = take ccols [minA .. maxA]
873− elementsB = take rrows [minB .. maxB]
874− combinations = (,) <$> elementsA <*> elementsB
875− combAp = map snd . sort . map (\(a, b) -> if f a == b
876− then ((fromEnum a, fromEnum b), nat 1)
877− else ((fromEnum a, fromEnum b), nat 0)) $ combinations
878− mList = buildList combAp rrows
879− in tr $ fromLists mList
882− buildList l r = take r l : buildList (drop r l) r
884-- | Lifts functions to relations with dimensions matching @a@ and @b@
936-- | Lifts functions to relations with dimensions matching @a@ and @b@
885-- cardinality's.
937-- cardinality's.
886−fromFRel' ::
938+fromFRel ::
887 forall a b.
939 forall a b.
888 ( Liftable Boolean a b,
940 ( Liftable Boolean a b,
889− CountableDimensionsN a b,
941+ CountableDimsN a b,
890− FromLists Boolean (Normalize b) (Normalize a)
942+ FLN b a
892 (a -> b) ->
944 (a -> b) ->
893 Relation (Normalize a) (Normalize b)
945 Relation (Normalize a) (Normalize b)
894−fromFRel' f =
946+fromFRel = fromFRel'
895− let minA = minBound @a
899− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
900− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
901− elementsA = take ccols [minA .. maxA]
902− elementsB = take rrows [minB .. maxB]
903− combinations = (,) <$> elementsA <*> elementsB
904− combAp = map snd . sort . map (\(a, b) -> if f a == b
905− then ((fromEnum a, fromEnum b), nat 1)
906− else ((fromEnum a, fromEnum b), nat 0)) $ combinations
907− mList = buildList combAp rrows
908− in tr $ fromLists mList
911− buildList l r = take r l : buildList (drop r l) r
913-- | Lifts a relation function to a Boolean Matrix
948-- | Lifts a relation function to a Boolean Matrix
914−toRel ::
949+toRel ::
915 forall a b.
950 forall a b.
916 ( Bounded a,
951 ( Bounded a,
917 Bounded b,
952 Bounded b,
921− CountableDimensionsN a b,
956+ CountableDims a b,
922− FromListsN Boolean b a
957+ FLN b a
924 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
959 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
926 let minA = minBound @a
961 let minA = minBound @a
927 maxA = maxBound @a
962 maxA = maxBound @a
928 minB = minBound @b
963 minB = minBound @b
929 maxB = maxBound @b
964 maxB = maxBound @b
930− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
965+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count a))
931− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
966+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count b))
932 elementsA = take ccols [minA .. maxA]
967 elementsA = take ccols [minA .. maxA]
933 elementsB = take rrows [minB .. maxB]
968 elementsB = take rrows [minB .. maxB]
934 combinations = (,) <$> elementsA <*> elementsB
969 combinations = (,) <$> elementsA <*> elementsB
935− combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
970+ combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
936− then ((fromEnum a, fromEnum b), nat 1)
971+ then ((fromEnum a, fromEnum b), nat 1)
937 else ((fromEnum a, fromEnum b), nat 0)) $ combinations
972 else ((fromEnum a, fromEnum b), nat 0)) $ combinations
938 mList = buildList combAp rrows
973 mList = buildList combAp rrows
939 in tr $ fromLists mList
974 in tr $ fromLists mList