@@ -13,22 +13,34 @@
1313{-# LANGUAGE TypeOperators #-}
1414{-# LANGUAGE UndecidableInstances #-}
1515
16+-----------------------------------------------------------------------------
17+-- |
18+-- Module : Matrix.Type
19+-- Copyright : (c) Armando Santos 2019-2020
20+-- Maintainer : armandoifsantos@gmail.com
21+-- Stability : experimental
22+--
23+-- The LAoP discipline generalises relations and functions treating them as
24+-- Boolean matrices and in turn consider these as arrows.
25+--
26+-- __LAoP__ is a library for algebraic (inductive) construction and manipulation of matrices
27+-- in Haskell. See <https://github.com/bolt12/master-thesis my Msc Thesis> for the
28+-- motivation behind the library, the underlying theory, and implementation details.
29+--
30+-- This module offers many of the combinators mentioned in the work of
31+-- Macedo (2012) and Oliveira (2012).
32+--
33+-----------------------------------------------------------------------------
34+
1635module Matrix.Type
17− ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
18− --
19− -- LAoP generalises relations and functions treating them as
20− -- Boolean matrices and in turn consider these as arrows.
21− -- This library offers many of the combinators mentioned in the work of
22− -- Macedo (2012) and Oliveira (2012).
23− --
24− -- This definition makes use of the fact that 'Void' is
25− -- isomorphic to 0 and '()' to 1 and captures matrix
26− -- dimensions as stacks of 'Either's.
36+ ( -- | This definition makes use of the fact that 'Void' is
37+ -- isomorphic to 0 and '()' to 1 and captures matrix
38+ -- dimensions as stacks of 'Either's.
2739 --
28− -- There exists two type families that make it easier to write
29− -- matrix dimensions: 'FromNat' and 'Count'. This approach
30− -- leads to a very straightforward implementation
31− -- of LAoP combinators.
40+ -- There exists two type families that make it easier to write
41+ -- matrix dimensions: 'FromNat' and 'Count'. This approach
42+ -- leads to a very straightforward implementation
43+ -- of LAoP combinators.
3244
3345 -- * Type safe matrix representation
3446 Matrix (..),
@@ -95,9 +107,7 @@ module Matrix.Type
95107 -- | Note that given the restrictions imposed it is not possible to
96108 -- implement the standard type classes present in standard Haskell.
97109 -- *** Matrix pairing projections
98− KhatriP1,
99110 kp1,
100− KhatriP2,
101111 kp2,
102112
103113 -- *** Matrix pairing
@@ -127,8 +137,9 @@ import Data.List
127137import Data.Proxy
128138import Data.Void
129139import GHC.TypeLits
140+import GHC.Generics
130141
131−-- | Matrix data type
142+-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
132143data Matrix e cols rows where
133144 Empty :: Matrix e Void Void
134145 One :: e -> Matrix e () ()
@@ -137,17 +148,24 @@ data Matrix e cols rows where
137148
138149deriving instance (Show e) => Show (Matrix e cols rows)
139150
140−-- | Type family that computes the cardinality of a given type dimension
151+-- | Type family that computes the cardinality of a given type dimension.
152+-- It can also count the cardinality of custom types that implement the
153+-- 'Generic' instance.
141154type family Count (d :: Type) where
142− Count Void = 0
143− Count () = 1
144− Count Bool = 2
145155 Count (Natural n) = n
146156 Count (Either a b) = (+) (Count a) (Count b)
147157 Count (a, b) = (*) (Count a) (Count b)
148158 Count (a -> b) = (^) (Count b) (Count a)
149−
150−-- | Type family that computes of a given type dimension from a fiven natural
159+ -- Generics
160+ Count (M1 _ _ f p) = Count (f p)
161+ Count (K1 _ _ _) = 1
162+ Count (V1 _) = 0
163+ Count (U1 _) = 1
164+ Count ((:*:) a b p) = Count (a p) * Count (b p)
165+ Count ((:+:) a b p) = Count (a p) + Count (b p)
166+ Count d = Count (Rep d R)
167+
168+-- | Type family that computes of a given type dimension from a given natural
151169type family FromNat (n :: Nat) where
152170 FromNat 0 = Void
153171 FromNat 1 = ()
@@ -199,47 +217,65 @@ instance Num e => Num (Matrix e cols rows) where
199217
200218-- Primitives
201219
220+-- | Empty matrix constructor
202221empty :: Matrix e Void Void
203222empty = Empty
204223
224+-- | Unit matrix constructor
205225one :: e -> Matrix e () ()
206226one = One
207227
228+-- | Matrix 'Junc' constructor
208229junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
209230junc = Junc
210231
211232infixl 3 |||
233+
234+-- | Matrix 'Junc' constructor
212235(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
213236(|||) = Junc
214237
238+-- | Matrix 'Split' constructor
215239split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
216240split = Split
217241
218242infixl 2 ===
243+
244+-- | Matrix 'Split' constructor
219245(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
220246(===) = Split
221247
222248-- Construction
223249
250+-- | Type class for defining the 'fromList' conversion function.
251+-- Given that it is not possible to branch on types at the term level type
252+-- classes are needed bery much like an inductive definition but on types.
224253class FromLists e cols rows where
254+ -- | Build a matrix out of a list of list of elements. Throws a runtime
255+ -- error if the dimensions do not match.
225256 fromLists :: [[e]] -> Matrix e cols rows
226257
258+-- | Void base case
227259instance FromLists e Void Void where
228260 fromLists [] = Empty
229261 fromLists _ = error "Wrong dimensions"
230262
263+-- | Unit base case
231264instance {-# OVERLAPPING #-} FromLists e () () where
232265 fromLists [[e]] = One e
233266 fromLists _ = error "Wrong dimensions"
234267
268+-- | Row vector matrix definition
235269instance (FromLists e cols ()) => FromLists e (Either () cols) () where
236270 fromLists [h : t] = Junc (One h) (fromLists [t])
237271 fromLists _ = error "Wrong dimensions"
238272
273+-- | Column vector matrix definition
239274instance (FromLists e () rows) => FromLists e () (Either () rows) where
240275 fromLists ([h] : t) = Split (One h) (fromLists t)
241276 fromLists _ = error "Wrong dimensions"
242277
278+-- | Arbitrary matrix definition
243279instance {-# OVERLAPPABLE #-} (FromLists e cols c, FromLists e cols d) => FromLists e cols (Either c d) where
244280 fromLists (h : t) =
245281 let lh = length h
@@ -248,6 +284,8 @@ instance {-# OVERLAPPABLE #-} (FromLists e cols c, FromLists e cols d) => FromLi
248284 then Split (fromLists [h]) (fromLists t)
249285 else error "Not all rows have the same length"
250286
287+-- | Matrix builder function. Constructs a matrix provided with
288+-- a construction function.
251289matrixBuilder ::
252290 forall e cols rows.
253291 ( FromLists e cols rows,
@@ -262,12 +300,17 @@ matrixBuilder f =
262300 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
263301 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
264302
303+-- | Constructs a column vector matrix
265304col :: (FromLists e () rows) => [e] -> Matrix e () rows
266305col = fromLists . map (: [])
267306
307+-- | Constructs a row vector matrix
268308row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
269309row = fromLists . (: [])
270310
311+-- | Lifts functions to matrices with arbitrary dimensions.
312+-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
313+-- types @a@ or @b@ allows.
271314fromF ::
272315 forall a b cols rows e.
273316 ( Bounded a,
@@ -302,6 +345,8 @@ fromF f =
302345 buildList [] _ = []
303346 buildList l r = take r l : buildList (drop r l) r
304347
348+-- | Lifts functions to matrices with dimensions matching @a@ and @b@
349+-- cardinality's.
305350fromF' ::
306351 forall a b e.
307352 ( Bounded a,
@@ -338,32 +383,40 @@ fromF' f =
338383
339384-- Conversion
340385
386+-- | Converts a matrix to a list of lists of elements.
341387toLists :: Matrix e cols rows -> [[e]]
342388toLists Empty = []
343389toLists (One e) = [[e]]
344390toLists (Split l r) = toLists l ++ toLists r
345391toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
346392
393+-- | Converts a matrix to a list of elements.
347394toList :: Matrix e cols rows -> [e]
348395toList = concat . toLists
349396
350397-- Zeros Matrix
351398
399+-- | The zero matrix. A matrix wholly filled with zeros.
352400zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
353401zeros = matrixBuilder (const 0)
354402
355403-- Ones Matrix
356404
405+-- | The ones matrix. A matrix wholly filled with ones.
406+-- Also known as T (Top) matrix.
357407ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
358408ones = matrixBuilder (const 1)
359409
360410-- Const Matrix
361411
412+-- | The constant matrix constructor. A matrix wholly filled with a given
413+-- value.
362414constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows
363415constant e = matrixBuilder (const e)
364416
365417-- Bang Matrix
366418
419+-- | The T (Top) row vector matrix.
367420bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()
368421bang =
369422 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
@@ -371,11 +424,15 @@ bang =
371424
372425-- Identity Matrix
373426
427+-- | Identity matrix.
374428identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols
375429identity = matrixBuilder (bool 0 1 . uncurry (==))
376430
377431-- Matrix composition (MMM)
378432
433+-- | Matrix composition. Equivalent to matrix-matrix multiplication.
434+-- This definition takes advantage of divide-and-conquer and fusion laws
435+-- from LAoP.
379436comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
380437comp Empty Empty = Empty
381438comp (One a) (One b) = One (a * b)
@@ -385,12 +442,14 @@ comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc fusion law
385442
386443-- Projections
387444
445+-- | Biproduct first component projection
388446p1 :: 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
389447p1 =
390448 let iden = identity :: Matrix e m m
391449 zero = zeros :: Matrix e n m
392450 in junc iden zero
393451
452+-- | Biproduct second component projection
394453p2 :: 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
395454p2 =
396455 let iden = identity :: Matrix e n n
@@ -399,17 +458,29 @@ p2 =
399458
400459-- Injections
401460
461+-- | Biproduct first component injection
402462i1 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
403463i1 = tr p1
404464
465+-- | Biproduct second component injection
405466i2 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
406467i2 = tr p2
407468
408469-- Dimensions
409470
471+-- | Obtain the number of rows.
472+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
473+-- dimensions in constant time.
474+-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
475+-- exchange for performance.
410476rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int
411477rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
412478
479+-- | Obtain the number of columns.
480+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
481+-- dimensions in constant time.
482+-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
483+-- exchange for performance.
413484columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int
414485columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
415486
@@ -417,6 +488,7 @@ columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
417488
418489infixl 5 -|-
419490
491+-- | Matrix coproduct functor also known as matrix direct sum.
420492(-|-) ::
421493 forall e n k m j.
422494 ( Num e,
@@ -434,51 +506,57 @@ infixl 5 -|-
434506
435507-- Khatri Rao Product and projections
436508
437−class KhatriP1 e m k where
438− kp1 :: Matrix e (Normalize (m, k)) m
439−
440−instance KhatriP1 e Void k where
441− kp1 = Empty
442−
443−instance
509+-- | Khatri Rao product first component projection matrix.
510+kp1 ::
511+ forall e m k .
444512 ( Num e,
445513 KnownNat (Count k),
446514 FromLists e (FromNat (Count m * Count k)) m,
447515 KnownNat (Count m),
448516 KnownNat (Count (Normalize (m, k)))
449− ) =>
450− KhatriP1 e m k
517+ ) => Matrix e (Normalize (m, k)) m
518+kp1 = matrixBuilder f
451519 where
452− kp1 = matrixBuilder f
453− where
454− offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
455− f (x, y)
456− | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
457− | otherwise = 0
458−
459−class KhatriP2 e m k where
460− kp2 :: Matrix e (Normalize (m, k)) k
461−
462−instance KhatriP2 e m Void where
463− kp2 = Empty
464−
465−instance
466− ( Num e,
467− KnownNat (Count k),
468− FromLists e (FromNat (Count m * Count k)) k,
469− KnownNat (Count m),
470− KnownNat (Count (Normalize (m, k)))
471− ) =>
472− KhatriP2 e m k
520+ offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
521+ f (x, y)
522+ | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
523+ | otherwise = 0
524+
525+-- | Khatri Rao product second component projection matrix.
526+kp2 ::
527+ forall e m k .
528+ ( Num e,
529+ KnownNat (Count k),
530+ FromLists e (FromNat (Count m * Count k)) k,
531+ KnownNat (Count m),
532+ KnownNat (Count (Normalize (m, k)))
533+ ) => Matrix e (Normalize (m, k)) k
534+kp2 = matrixBuilder f
473535 where
474− kp2 = matrixBuilder f
475− where
476− offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
477− f (x, y)
478− | x == y || mod (y - x) offset == 0 = 1
479− | otherwise = 0
480−
481−khatri :: forall e cols a b. (Num e, KhatriP1 e a b, KhatriP2 e a b) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
536+ offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
537+ f (x, y)
538+ | x == y || mod (y - x) offset == 0 = 1
539+ | otherwise = 0
540+
541+-- | Khatri Rao Matrix product also known as matrix pairing.
542+-- NOTE: That this is not a true categorical product, see for instance:
543+--
544+-- @
545+-- | kp1 `comp` khatri a b == a
546+-- khatri a b ==> |
547+-- | kp2 `comp` khatri a b == b
548+-- @
549+--
550+-- __Emphasis__ on the implication symbol.
551+khatri ::
552+ forall e cols a b.
553+ ( Num e,
554+ KnownNat (Count a),
555+ KnownNat (Count b),
556+ KnownNat (Count (Normalize (a, b))),
557+ FromLists e (Normalize (a, b)) a,
558+ FromLists e (Normalize (a, b)) b
559+ ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
482560khatri a b =
483561 let kp1' = kp1 @e @a @b
484562 kp2' = kp2 @e @a @b
@@ -488,7 +566,22 @@ khatri a b =
488566
489567infixl 4 ><
490568
491−(><) :: forall e m p n q. (Num e, KhatriP1 e m n, KhatriP2 e m n, KhatriP1 e p q, KhatriP2 e p q) => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
569+-- | Matrix product functor also known as kronecker product
570+(><) ::
571+ forall e m p n q.
572+ ( Num e,
573+ KnownNat (Count m),
574+ KnownNat (Count n),
575+ KnownNat (Count p),
576+ KnownNat (Count q),
577+ KnownNat (Count (Normalize (m, n))),
578+ FromLists e (Normalize (m, n)) m,
579+ FromLists e (Normalize (m, n)) n,
580+ KnownNat (Count (Normalize (p, q))),
581+ FromLists e (Normalize (p, q)) p,
582+ FromLists e (Normalize (p, q)) q
583+ )
584+ => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
492585(><) a b =
493586 let kp1' = kp1 @e @m @n
494587 kp2' = kp2 @e @m @n
@@ -496,6 +589,11 @@ infixl 4 ><
496589
497590-- Matrix abide Junc Split
498591
592+-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
593+--
594+-- @
595+-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
596+-- @
499597abideJS :: Matrix e cols rows -> Matrix e cols rows
500598abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law
501599abideJS Empty = Empty
@@ -505,6 +603,11 @@ abideJS (Split a b) = Split (abideJS a) (abideJS b)
505603
506604-- Matrix abide Split Junc
507605
606+-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
607+--
608+-- @
609+-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
610+-- @
508611abideSJ :: Matrix e cols rows -> Matrix e cols rows
509612abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law
510613abideSJ Empty = Empty
@@ -514,6 +617,7 @@ abideSJ (Split a b) = Split (abideSJ a) (abideSJ b)
514617
515618-- Matrix transposition
516619
620+-- | Matrix transposition.
517621tr :: Matrix e cols rows -> Matrix e rows cols
518622tr Empty = Empty
519623tr (One e) = One e
@@ -522,6 +626,8 @@ tr (Split a b) = Junc (tr a) (tr b)
522626
523627-- Selective 'select' operator
524628
629+-- | Selective functors 'select' operator equivalent inspired by the
630+-- ArrowMonad solution presented in the paper.
525631select :: (Bounded a1, Bounded b, Enum a1, Enum b, Num e, Ord e,
526632 KnownNat (Count a2), KnownNat (Count rows), FromLists e rows a2,
527633 FromLists e rows rows, Eq b) =>
@@ -532,13 +638,13 @@ select m y =
532638
533639-- McCarthy's Conditional
534640
641+-- | McCarthy's Conditional expresses probabilistic choice.
535642cond ::
536643 ( cols ~ FromNat (Count cols),
537644 KnownNat (Count cols),
538645 FromLists e () cols,
539646 FromLists e cols (),
540647 FromLists e cols cols,
541− KhatriP2 e () cols,
542648 Bounded a,
543649 Enum a,
544650 Num e,
@@ -554,7 +660,6 @@ grd ::
554660 FromLists e () q,
555661 FromLists e q (),
556662 FromLists e q q,
557− KhatriP2 e () q,
558663 Bounded a,
559664 Enum a,
560665 Num e,
@@ -571,7 +676,6 @@ corr ::
571676 FromLists e () q,
572677 FromLists e q (),
573678 FromLists e q q,
574− KhatriP2 e () q,
575679 Bounded a,
576680 Enum a,
577681 Num e,
@@ -602,6 +706,7 @@ prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
602706 widest = maximum $ fmap length v
603707 fill str = replicate (widest - length str - 2) ' ' ++ str
604708
709+-- | Matrix pretty printer
605710pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String
606711pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
607712 prettyAux (toLists m) (toLists m) ++
@@ -612,5 +717,6 @@ pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
612717 fill str = replicate (widest - length str) ' ' ++ str
613718 blank = fill ""
614719
720+-- | Matrix pretty printer
615721prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()
616722prettyPrint = putStrLn . pretty