@@ -1,11 +1,10 @@
1−{-# LANGUAGE ConstraintKinds #-}
2−{-# LANGUAGE TypeFamilies #-}
3{-# LANGUAGE AllowAmbiguousTypes #-}
1{-# LANGUAGE AllowAmbiguousTypes #-}
4{-# LANGUAGE DataKinds #-}
2{-# LANGUAGE DataKinds #-}
5{-# LANGUAGE DerivingVia #-}
3{-# LANGUAGE DerivingVia #-}
6{-# LANGUAGE FlexibleContexts #-}
4{-# LANGUAGE FlexibleContexts #-}
7{-# LANGUAGE FlexibleInstances #-}
5{-# LANGUAGE FlexibleInstances #-}
8{-# LANGUAGE GADTs #-}
6{-# LANGUAGE GADTs #-}
7+{-# LANGUAGE KindSignatures #-}
9{-# LANGUAGE MultiParamTypeClasses #-}
8{-# LANGUAGE MultiParamTypeClasses #-}
10{-# LANGUAGE NoStarIsType #-}
9{-# LANGUAGE NoStarIsType #-}
11{-# LANGUAGE RankNTypes #-}
10{-# LANGUAGE RankNTypes #-}
@@ -16,7 +15,7 @@
17-----------------------------------------------------------------------------
16-----------------------------------------------------------------------------
19−-- Module : LAoP.Matrix.Type
18+-- Module : Matrix.Type
20-- Copyright : (c) Armando Santos 2019-2020
19-- Copyright : (c) Armando Santos 2019-2020
21-- Maintainer : armandoifsantos@gmail.com
20-- Maintainer : armandoifsantos@gmail.com
22-- Stability : experimental
21-- Stability : experimental
@@ -37,7 +36,7 @@
38-----------------------------------------------------------------------------
37-----------------------------------------------------------------------------
40−module LAoP.Matrix.Type
39+module Matrix.Type
41 ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
40 ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
43 -- LAoP generalises relations and functions treating them as
42 -- LAoP generalises relations and functions treating them as
@@ -56,24 +55,15 @@ module LAoP.Matrix.Type
56 -- * Type safe matrix representation
55 -- * Type safe matrix representation
57 Matrix (..),
56 Matrix (..),
59− -- * Constraint type aliases
69 -- * Type aliases
58 -- * Type aliases
73 -- * Primitives
62 -- * Primitives
78 -- * Auxiliary type families
68 -- * Auxiliary type families
79 I.FromNat,
69 I.FromNat,
@@ -85,27 +75,24 @@ module LAoP.Matrix.Type
85 fromLists,
75 fromLists,
89 matrixBuilder,
78 matrixBuilder,
98 -- * Functor instance equivalent function
86 -- * Functor instance equivalent function
102 -- * Applicative/Monoidal instance equivalent functions
89 -- * Applicative/Monoidal instance equivalent functions
106 -- * Selective equivalent instance function
93 -- * Selective equivalent instance function
107− selectM,
94+ selectM,
109 -- * Monad equivalent instance function
96 -- * Monad equivalent instance function
@@ -113,34 +100,25 @@ module LAoP.Matrix.Type
113 -- * Misc
100 -- * Misc
114 -- ** Get dimensions
101 -- ** Get dimensions
120 -- ** Matrix Transposition
105 -- ** Matrix Transposition
123− -- ** Scalar multiplication/division of matrices
127 -- ** McCarthy's Conditional
108 -- ** McCarthy's Conditional
130 -- ** Matrix "abiding"
111 -- ** Matrix "abiding"
131− abideJF,
112+ abideJS,
132− abideFJ,
113+ abideSJ,
137 -- * Biproduct approach
115 -- * Biproduct approach
138− -- ** Fork
116+ -- ** Split
140 -- *** Projections
118 -- *** Projections
143− -- ** Join
121+ -- ** Junc
145 -- *** Injections
123 -- *** Injections
@@ -154,11 +132,11 @@ module LAoP.Matrix.Type
154 -- | Note that given the restrictions imposed it is not possible to
132 -- | Note that given the restrictions imposed it is not possible to
155 -- implement the standard type classes present in standard Haskell.
133 -- implement the standard type classes present in standard Haskell.
156 -- *** Matrix pairing projections
134 -- *** Matrix pairing projections
160 -- *** Matrix pairing
138 -- *** Matrix pairing
163 -- * Matrix composition and lifting
141 -- * Matrix composition and lifting
@@ -166,13 +144,10 @@ module LAoP.Matrix.Type
167 -- | Note that given the restrictions imposed it is not possible to
145 -- | Note that given the restrictions imposed it is not possible to
168 -- implement the standard type classes present in standard Haskell.
146 -- implement the standard type classes present in standard Haskell.
177 -- * Matrix printing
152 -- * Matrix printing
@@ -183,44 +158,22 @@ where
183import Data.Void
158import Data.Void
184import Data.Proxy
159import Data.Proxy
185import Data.Kind
160import Data.Kind
186−import GHC.TypeLits
161+import GHC.TypeLits
187import Control.DeepSeq
162import Control.DeepSeq
188−import LAoP.Utils
163+import qualified Control.Category as C
189−import qualified LAoP.Matrix.Internal as I
164+import qualified Matrix.Internal as I
190−import Prelude hiding (id, (.))
192newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
166newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
193 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
167 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
195−-- | Constraint type synonyms to keep the type signatures less convoluted
196−type Countable a = KnownNat (I.Count a)
197−type CountableDims a b = (Countable a, Countable b)
198−type CountableN a = KnownNat (I.Count (I.Normalize a))
199−type CountableDimsN a b = (CountableN a, CountableN b)
200−type FLN a b = I.FromLists (I.Normalize a) (I.Normalize b)
201−type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
202−type Trivial a = I.Normalize (I.Normalize a) ~ I.Normalize (I.Normalize (I.Normalize a))
203−type Trivial2 a = I.Normalize a ~ I.Normalize (I.Normalize a)
204−type Trivial3 a = I.FromNat (I.Count (I.Normalize (I.Normalize a))) ~ I.Normalize (I.Normalize a)
205−type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
207−-- | It is possible to implement a constrained version of the category type
169+-- | It isn't possible to implement the 'id' function so it's
208−-- class.
170+-- implementation is 'undefined'. However 'comp' can be and this partial
171+-- class implementation exists just to make the code more readable.
173+-- Please use 'identity' instead.
209−instance (Num e) => Category (Matrix e) where
174+instance (Num e) => C.Category (Matrix e) where
210− type Object (Matrix e) a = (FLN a a, CountableN a)
175+ id = undefined
212− (.) = comp
176+ (.) = comp
214−-- | Bifunctor equivalent function
222− ) => (a -> b) -> (c -> d) -> Matrix e a c -> Matrix e b d
223−bimapM f g m = fromF g . m . tr (fromF f)
225-- | Zero type alias
178-- | Zero type alias
226type Zero = Void
179type Zero = Void
@@ -230,75 +183,92 @@ type One = ()
231-- Primitives
184-- Primitives
186+-- | Empty matrix constructor
187+empty :: Matrix e Zero Zero
233-- | Unit matrix constructor
190-- | Unit matrix constructor
234one :: e -> Matrix e One One
191one :: e -> Matrix e One One
235one = M . I.One
192one = M . I.One
237−-- | Matrix 'Join' constructor
194+-- | Matrix 'Junc' constructor
196+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
239 Matrix e a rows ->
197 Matrix e a rows ->
240 Matrix e b rows ->
198 Matrix e b rows ->
241 Matrix e (Either a b) rows
199 Matrix e (Either a b) rows
242−join (M a) (M b) = M (I.Join a b)
200+junc (M a) (M b) = M (I.Junc a b)
244infixl 3 |||
202infixl 3 |||
245−-- | Matrix 'Join' constructor
203+-- | Matrix 'Junc' constructor
205+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
247 Matrix e a rows ->
206 Matrix e a rows ->
248 Matrix e b rows ->
207 Matrix e b rows ->
249 Matrix e (Either a b) rows
208 Matrix e (Either a b) rows
250−(|||) = join
209+(|||) = junc
252−-- | Matrix 'Fork' constructor
211+-- | Matrix 'Split' constructor
213+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
254 Matrix e cols a ->
214 Matrix e cols a ->
255 Matrix e cols b ->
215 Matrix e cols b ->
256 Matrix e cols (Either a b)
216 Matrix e cols (Either a b)
257−fork (M a) (M b) = M (I.Fork a b)
217+split (M a) (M b) = M (I.Split a b)
259infixl 2 ===
219infixl 2 ===
260−-- | Matrix 'Fork' constructor
220+-- | Matrix 'Split' constructor
222+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
262 Matrix e cols a ->
223 Matrix e cols a ->
263 Matrix e cols b ->
224 Matrix e cols b ->
264 Matrix e cols (Either a b)
225 Matrix e cols (Either a b)
265−(===) = fork
226+(===) = split
267-- Functor hierarchy
228-- Functor hierarchy
269-- | Functor instance equivalent function
230-- | Functor instance equivalent function
271− ( Liftable e a b,
232+ ( Bounded a,
272− CountableDimsN a b,
233+ Bounded b,
239+ KnownNat (I.Count (I.Normalize a)),
240+ KnownNat (I.Count (I.Normalize b)),
241+ I.FromLists e (I.Normalize b) (I.Normalize a)
276 (a -> b) -> Matrix e c a -> Matrix e c b
244 (a -> b) -> Matrix e c a -> Matrix e c b
277−fmapM f m = fromF f . m
245+fmapM f m = fromF' f `comp` m
279-- | Applicative instance equivalent 'unit' function,
247-- | Applicative instance equivalent 'unit' function,
280unitM :: (Num e) => Matrix e () ()
248unitM :: (Num e) => Matrix e () ()
281unitM = one 1
249unitM = one 1
283-- | Applicative instance equivalent 'unit' function,
251-- | Applicative instance equivalent 'unit' function,
285− ( CountableDimsN a b,
253+ ( KnownNat (I.Count (I.Normalize a)),
286− CountableN (a, b),
254+ KnownNat (I.Count (I.Normalize b)),
255+ KnownNat (I.Count (I.Normalize (a, b))),
288− FLN (a, b) a,
257+ I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
289− FLN (a, b) b,
258+ I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
290− TrivialP a b
259+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
291 ) => Matrix e c a -> Matrix e c b -> Matrix e c (a, b)
260 ) => Matrix e c a -> Matrix e c b -> Matrix e c (a, b)
292−multM = kr
261+multM a b = khatri a b
294-- | Monad instance equivalent 'return' function,
264-- | Monad instance equivalent 'return' function,
295−returnM ::
265+returnM ::
296− forall e a .
266+ forall e a .
297− ( Num e,
267+ ( Num e,
300− FLN () a,
270+ I.FromLists e () (I.Normalize a),
301− Countable a
271+ KnownNat (I.Count a)
302 ) => a -> Matrix e One a
272 ) => a -> Matrix e One a
303returnM a = col l
273returnM a = col l
@@ -314,66 +284,62 @@ bindM = flip comp
315-- | Build a matrix out of a list of list of elements. Throws a runtime
285-- | Build a matrix out of a list of list of elements. Throws a runtime
316-- error if the dimensions do not match.
286-- error if the dimensions do not match.
317−fromLists :: (FLN cols rows) => [[e]] -> Matrix e cols rows
287+fromLists :: (I.FromLists e (I.Normalize cols) (I.Normalize rows)) => [[e]] -> Matrix e cols rows
318fromLists = M . I.fromLists
288fromLists = M . I.fromLists
320-- | Matrix builder function. Constructs a matrix provided with
290-- | Matrix builder function. Constructs a matrix provided with
321−-- a construction function that operates with indices.
291+-- a construction function.
323− (FLN cols rows, CountableDimsN cols rows )
324− => ((Int, Int) -> e) -> Matrix e cols rows
325−matrixBuilder' = M . I.matrixBuilder'
327−-- | Matrix builder function. Constructs a matrix provided with
328−-- a construction function that operates with arbitrary types.
329matrixBuilder ::
292matrixBuilder ::
330− ( FLN a b,
293+ (I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
331− Enum a,
294+ ((Int, Int) -> e) ->
337− ) => ((a, b) -> e) -> Matrix e a b
295+ Matrix e cols rows
338−matrixBuilder f = M (I.matrixBuilder f)
296+matrixBuilder = M . I.matrixBuilder
340-- | Constructs a column vector matrix
298-- | Constructs a column vector matrix
341−col :: (FLN () rows) => [e] -> Matrix e One rows
299+col :: (I.FromLists e () (I.Normalize rows)) => [e] -> Matrix e One rows
342col = M . I.col
300col = M . I.col
344-- | Constructs a row vector matrix
302-- | Constructs a row vector matrix
345−row :: (FLN cols ()) => [e] -> Matrix e cols One
303+row :: (I.FromLists e (I.Normalize cols) ()) => [e] -> Matrix e cols One
346row = M . I.row
304row = M . I.row
348-- | Lifts functions to matrices with arbitrary dimensions.
306-- | Lifts functions to matrices with arbitrary dimensions.
350-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
308-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
351-- types @a@ or @b@ allows.
309-- types @a@ or @b@ allows.
352−fromF' ::
310+fromF ::
353− ( Liftable e a b,
311+ ( Bounded a,
354− CountableDimsN cols rows,
312+ Bounded b,
355− FLN rows cols
313+ Enum a,
318+ KnownNat (I.Count (I.Normalize cols)),
319+ KnownNat (I.Count (I.Normalize rows)),
320+ I.FromLists e (I.Normalize rows) (I.Normalize cols)
357− (a -> b) -> Matrix e cols rows
323+ Matrix e cols rows
358−fromF' = M . I.fromF'
324+fromF = M . I.fromF
360-- | Lifts functions to matrices with dimensions matching @a@ and @b@
326-- | Lifts functions to matrices with dimensions matching @a@ and @b@
361-- cardinality's.
327-- cardinality's.
362−fromF ::
328+fromF' ::
363− ( Liftable e a b,
329+ ( Bounded a,
364− CountableDimsN a b,
330+ Bounded b,
336+ KnownNat (I.Count (I.Normalize a)),
337+ KnownNat (I.Count (I.Normalize b)),
338+ I.FromLists e (I.Normalize b) (I.Normalize a)
367− (a -> b) -> Matrix e a b
341+ Matrix e a b
368−fromF = M . I.fromF
342+fromF' = M . I.fromF'
370−-- | Lifts relation functions to Boolean Matrix
372− ( Liftable (Natural 0 1) a b,
375− ) => (a -> b -> Bool) -> Matrix (Natural 0 1) a b
378-- Conversion
344-- Conversion
@@ -389,8 +355,8 @@ toList (M m) = I.toList m
390-- | The zero matrix. A matrix wholly filled with zeros.
356-- | The zero matrix. A matrix wholly filled with zeros.
392− (Num e, FLN cols rows, CountableDimsN cols rows)
358+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
393− => Matrix e cols rows
359+ Matrix e cols rows
394zeros = M I.zeros
360zeros = M I.zeros
396-- Ones Matrix
362-- Ones Matrix
@@ -399,8 +365,8 @@ zeros = M I.zeros
400-- Also known as T (Top) matrix.
366-- Also known as T (Top) matrix.
402− (Num e, FLN cols rows, CountableDimsN cols rows)
368+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
403− => Matrix e cols rows
369+ Matrix e cols rows
404ones = M I.ones
370ones = M I.ones
406-- Const Matrix
372-- Const Matrix
@@ -408,8 +374,9 @@ ones = M I.ones
408-- | The constant matrix constructor. A matrix wholly filled with a given
374-- | The constant matrix constructor. A matrix wholly filled with a given
410constant ::
376constant ::
411− (Num e, FLN cols rows, CountableDimsN cols rows)
377+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
412− => e -> Matrix e cols rows
379+ Matrix e cols rows
413constant = M . I.constant
380constant = M . I.constant
415-- Bang Matrix
382-- Bang Matrix
@@ -417,30 +384,17 @@ constant = M . I.constant
417-- | The T (Top) row vector matrix.
384-- | The T (Top) row vector matrix.
419 forall e cols.
386 forall e cols.
420− (Num e, Enum e, FLN cols (), CountableN cols) =>
387+ (Num e, Enum e, I.FromLists e (I.Normalize cols) (), KnownNat (I.Count (I.Normalize cols))) =>
421 Matrix e cols One
388 Matrix e cols One
422bang = M I.bang
389bang = M I.bang
424−-- | Point constant relation
433− ) => a -> Matrix e One a
434−point = fromF . const
436−-- iden Matrix
391+-- Identity Matrix
438−-- | iden matrix
393+-- | Identity matrix
439−iden ::
394+identity ::
440− (Num e, FLN a a, CountableN a) =>
395+ (Num e, I.FromLists e (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
441 Matrix e a a
396 Matrix e a a
442−iden = M I.iden
397+identity = M I.identity
443−{-# NOINLINE iden #-}
445-- Matrix composition (MMM)
399-- Matrix composition (MMM)
@@ -450,32 +404,15 @@ iden = M I.iden
450-- from LAoP.
404-- from LAoP.
451comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
405comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
452comp (M a) (M b) = M (I.comp a b)
406comp (M a) (M b) = M (I.comp a b)
453−{-# NOINLINE comp #-}
455− "comp/iden1" forall m. comp m iden = m ;
456− "comp/iden2" forall m. comp iden m = m
459−-- Scalar multiplication of matrices
462−-- | Scalar multiplication of matrices.
463−(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
464−(.|) e (M m) = M (e I..| m)
466−-- Scalar division of matrices
469−-- | Scalar multiplication of matrices.
470−(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
471−(./) (M m) e = M (m I../ e)
473-- | Biproduct first component projection
408-- | Biproduct first component projection
476− CountableDimsN n m,
411+ KnownNat (I.Count (I.Normalize n)),
477− FLN n m,
412+ KnownNat (I.Count (I.Normalize m)),
478− FLN m m
413+ I.FromLists e (I.Normalize n) (I.Normalize m),
414+ I.FromLists e (I.Normalize m) (I.Normalize m),
415+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
480 Matrix e (Either m n) m
417 Matrix e (Either m n) m
481p1 = M I.p1
418p1 = M I.p1
@@ -483,9 +420,11 @@ p1 = M I.p1
483-- | Biproduct second component projection
420-- | Biproduct second component projection
486− CountableDimsN n m,
423+ KnownNat (I.Count (I.Normalize n)),
487− FLN m n,
424+ KnownNat (I.Count (I.Normalize m)),
488− FLN n n
425+ I.FromLists e (I.Normalize m) (I.Normalize n),
426+ I.FromLists e (I.Normalize n) (I.Normalize n),
427+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
490 Matrix e (Either m n) n
429 Matrix e (Either m n) n
491p2 = M I.p2
430p2 = M I.p2
@@ -495,9 +434,11 @@ p2 = M I.p2
495-- | Biproduct first component injection
434-- | Biproduct first component injection
498− CountableDimsN n m,
437+ KnownNat (I.Count (I.Normalize n)),
499− FLN n m,
438+ KnownNat (I.Count (I.Normalize m)),
500− FLN m m
439+ I.FromLists e (I.Normalize n) (I.Normalize m),
440+ I.FromLists e (I.Normalize m) (I.Normalize m),
441+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
502 Matrix e m (Either m n)
443 Matrix e m (Either m n)
503i1 = tr p1
444i1 = tr p1
@@ -505,9 +446,11 @@ i1 = tr p1
505-- | Biproduct second component injection
446-- | Biproduct second component injection
508− CountableDimsN n m,
449+ KnownNat (I.Count (I.Normalize n)),
509− FLN m n,
450+ KnownNat (I.Count (I.Normalize m)),
510− FLN n n
451+ I.FromLists e (I.Normalize m) (I.Normalize n),
452+ I.FromLists e (I.Normalize n) (I.Normalize n),
453+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
512 Matrix e n (Either m n)
455 Matrix e n (Either m n)
513i2 = tr p2
456i2 = tr p2
@@ -516,34 +459,24 @@ i2 = tr p2
517-- | Obtain the number of rows.
460-- | Obtain the number of rows.
519−-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
462+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
520−-- dimensions in constant time. For a version that doesn't require the
463+-- dimensions in constant time.
521−-- constraint see 'rows''.
522−rows :: (CountableN rows) => Matrix e cols rows -> Int
523−rows (M m) = I.rows m
525−-- | Obtain the number of rows in an inefficient manner, but without any
528−-- For a more efficient version see 'rows'.
465+-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
466+-- exchange for performance.
529−rows' :: Matrix e cols rows -> Int
467+rows :: (KnownNat (I.Count (I.Normalize rows))) => Matrix e cols rows -> Int
530−rows' (M m) = I.rows' m
468+rows (M m) = I.rows m
532-- | Obtain the number of columns.
470-- | Obtain the number of columns.
472+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
473+-- dimensions in constant time.
534−-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
475+-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
535−-- dimensions in constant time. For a version that doesn't require the
476+-- exchange for performance.
536−-- constraint see 'columns''.
537−columns :: (CountableN cols) => Matrix e cols rows -> Int
477+columns :: (KnownNat (I.Count (I.Normalize cols))) => Matrix e cols rows -> Int
538columns (M m) = I.columns m
478columns (M m) = I.columns m
540−-- | Obtain the number of columns in an inefficient manner, but without any
543−-- For a more efficient version see 'columns'.
544−columns' :: Matrix e cols rows -> Int
545−columns' (M m) = I.columns' m
547-- Coproduct Bifunctor
480-- Coproduct Bifunctor
549infixl 5 -|-
482infixl 5 -|-
@@ -551,11 +484,14 @@ infixl 5 -|-
551-- | Matrix coproduct functor also known as matrix direct sum.
484-- | Matrix coproduct functor also known as matrix direct sum.
554− CountableDimsN j k,
487+ KnownNat (I.Count (I.Normalize j)),
555− FLN k k,
488+ KnownNat (I.Count (I.Normalize k)),
556− FLN j k,
489+ I.FromLists e (I.Normalize k) (I.Normalize k),
557− FLN k j,
490+ I.FromLists e (I.Normalize j) (I.Normalize k),
558− FLN j j
491+ I.FromLists e (I.Normalize k) (I.Normalize j),
492+ I.FromLists e (I.Normalize j) (I.Normalize j),
493+ I.Normalize (Either n m) ~ Either (I.Normalize n) (I.Normalize m),
494+ I.Normalize (Either k j) ~ Either (I.Normalize k) (I.Normalize j)
560 Matrix e n k ->
496 Matrix e n k ->
561 Matrix e m j ->
497 Matrix e m j ->
@@ -565,98 +501,104 @@ infixl 5 -|-
565-- Khatri Rao Product and projections
501-- Khatri Rao Product and projections
567-- | Khatri Rao product first component projection matrix.
503-- | Khatri Rao product first component projection matrix.
569 forall e m k .
505 forall e m k .
571− CountableDimsN m k,
507+ KnownNat (I.Count (I.Normalize m)),
572− CountableN (m, k),
508+ KnownNat (I.Count (I.Normalize k)),
573− FLN (m, k) m,
509+ KnownNat (I.Count (I.Normalize (m, k))),
574− TrivialP m k
510+ I.FromLists e (I.Normalize (m, k)) (I.Normalize m),
511+ I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
575 ) => Matrix e (m, k) m
512 ) => Matrix e (m, k) m
576−fstM = M (I.fstM @e @(I.Normalize m) @(I.Normalize k))
513+kp1 = M (I.kp1 @e @(I.Normalize m) @(I.Normalize k))
578-- | Khatri Rao product second component projection matrix.
515-- | Khatri Rao product second component projection matrix.
580 forall e m k.
517 forall e m k.
582− CountableDimsN k m,
519+ KnownNat (I.Count (I.Normalize k)),
583− CountableN (m, k),
520+ KnownNat (I.Count (I.Normalize m)),
584− FLN (m, k) k,
521+ KnownNat (I.Count (I.Normalize (m, k))),
585− TrivialP m k
522+ I.FromLists e (I.Normalize (m, k)) (I.Normalize k),
523+ I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
586 ) => Matrix e (m, k) k
524 ) => Matrix e (m, k) k
587−sndM = M (I.sndM @e @(I.Normalize m) @(I.Normalize k))
525+kp2 = M (I.kp2 @e @(I.Normalize m) @(I.Normalize k))
589-- | Khatri Rao Matrix product also known as matrix pairing.
527-- | Khatri Rao Matrix product also known as matrix pairing.
591-- NOTE: That this is not a true categorical product, see for instance:
529-- NOTE: That this is not a true categorical product, see for instance:
594−-- | fstM . kr a b == a
532+-- | kp1 `comp` khatri a b == a
595−-- kr a b ==> |
533+-- khatri a b ==> |
596−-- | sndM . kr a b == b
534+-- | kp2 `comp` khatri a b == b
599-- __Emphasis__ on the implication symbol.
537-- __Emphasis__ on the implication symbol.
601 forall e cols a b.
539 forall e cols a b.
603− CountableDimsN a b,
541+ KnownNat (I.Count (I.Normalize a)),
604− CountableN (a, b),
542+ KnownNat (I.Count (I.Normalize b)),
605− FLN (a, b) a,
543+ KnownNat (I.Count (I.Normalize (a, b))),
606− FLN (a, b) b,
544+ I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
607− TrivialP a b
545+ I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
546+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
608 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, b)
547 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, b)
609−kr a b =
548+khatri a b =
610− let fstM' = fstM @e @a @b
549+ let kp1' = kp1 @e @a @b
611− sndM' = sndM @e @a @b
550+ kp2' = kp2 @e @a @b
612− in comp (tr fstM') a * comp (tr sndM') b
551+ in comp (tr kp1') a * comp (tr kp2') b
614-- Product Bifunctor (Kronecker)
553-- Product Bifunctor (Kronecker)
616infixl 4 ><
555infixl 4 ><
618−-- | Matrix product functor also known as Kronecker product
557+-- | Matrix product functor also known as kronecker product
620 forall e m p n q.
559 forall e m p n q.
622− CountableDimsN m n,
561+ KnownNat (I.Count (I.Normalize m)),
623− CountableDimsN p q,
562+ KnownNat (I.Count (I.Normalize n)),
624− CountableDimsN (m, n) (p, q),
563+ KnownNat (I.Count (I.Normalize p)),
625− FLN (m, n) m,
564+ KnownNat (I.Count (I.Normalize q)),
626− FLN (m, n) n,
565+ KnownNat (I.Count (I.Normalize (m, n))),
627− FLN (p, q) p,
566+ KnownNat (I.Count (I.Normalize (p, q))),
628− FLN (p, q) q,
567+ I.FromLists e (I.Normalize (m, n)) (I.Normalize m),
629− TrivialP m n,
568+ I.FromLists e (I.Normalize (m, n)) (I.Normalize n),
630− TrivialP p q
569+ I.FromLists e (I.Normalize (p, q)) (I.Normalize p),
570+ I.FromLists e (I.Normalize (p, q)) (I.Normalize q),
571+ I.Normalize (m, n) ~ I.Normalize (I.Normalize m, I.Normalize n),
572+ I.Normalize (p, q) ~ I.Normalize (I.Normalize p, I.Normalize q)
631 ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)
573 ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)
632(><) a b =
574(><) a b =
633− let fstM' = fstM @e @m @n
575+ let kp1' = kp1 @e @m @n
634− sndM' = sndM @e @m @n
576+ kp2' = kp2 @e @m @n
635− in kr (comp a fstM') (comp b sndM')
577+ in khatri (comp a kp1') (comp b kp2')
637−-- Matrix abide Join Fork
579+-- Matrix abide Junc Split
639−-- | Matrix "abiding" followin the 'Join'-'Fork' abide law.
581+-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
644−-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
586+-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
646−abideJF :: Matrix e cols rows -> Matrix e cols rows
588+abideJS :: Matrix e cols rows -> Matrix e cols rows
647−abideJF (M m) = M (I.abideJF m)
589+abideJS (M m) = M (I.abideJS m)
649−-- Matrix abide Fork Join
591+-- Matrix abide Split Junc
651−-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
593+-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
656−-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
598+-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
658−abideFJ :: Matrix e cols rows -> Matrix e cols rows
600+abideSJ :: Matrix e cols rows -> Matrix e cols rows
659−abideFJ (M m) = M (I.abideFJ m)
601+abideSJ (M m) = M (I.abideSJ m)
661-- Matrix transposition
603-- Matrix transposition
@@ -668,10 +610,11 @@ tr (M m) = M (I.tr m)
669-- | Selective functors 'select' operator equivalent inspired by the
611-- | Selective functors 'select' operator equivalent inspired by the
670-- ArrowMonad solution presented in the paper.
612-- ArrowMonad solution presented in the paper.
671−selectM ::
613+selectM ::
673− FLN b b,
615+ I.FromLists e (I.Normalize b) (I.Normalize b),
674− CountableN b
616+ KnownNat (I.Count (I.Normalize b)),
617+ I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
675 ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
618 ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
676selectM (M m) (M y) = M (I.select m y)
619selectM (M m) (M y) = M (I.select m y)
@@ -679,14 +622,15 @@ selectM (M m) (M y) = M (I.select m y)
680-- | McCarthy's Conditional expresses probabilistic choice.
623-- | McCarthy's Conditional expresses probabilistic choice.
682− ( Trivial a,
625+ ( I.Normalize (I.Normalize a) ~ I.Normalize a,
683− Trivial2 a,
626+ KnownNat (I.Count (I.Normalize a)),
684− Trivial3 a,
627+ I.FromLists e () (I.Normalize a),
685− CountableN a,
628+ I.FromLists e (I.Normalize a) (),
686− FLN () a,
629+ I.FromLists e (I.Normalize a) (I.Normalize a),
687− FLN a (),
630+ Bounded a,
688− FLN a a,
631+ Enum a,
689− Liftable e a Bool
632+ Num e,
692 (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b
636 (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b
@@ -695,13 +639,9 @@ cond p (M a) (M b) = M (I.cond p a b)
695-- Pretty print
639-- Pretty print
697-- | Matrix pretty printer
641-- | Matrix pretty printer
698−pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String
642+pretty :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> String
699pretty (M m) = I.pretty m
643pretty (M m) = I.pretty m
701-- | Matrix pretty printer
645-- | Matrix pretty printer
702−prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()
646+prettyPrint :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> IO ()
703prettyPrint (M m) = I.prettyPrint m
647prettyPrint (M m) = I.prettyPrint m
705−-- | Zip two matrices with a given binary function
706−zipWithM :: (e -> f -> g) -> Matrix e a b -> Matrix f a b -> Matrix g a b
707−zipWithM f (M a) (M b) = M (I.zipWithM f a b)