@@ -1,15 +1,15 @@
11{-# LANGUAGE AllowAmbiguousTypes #-}
22{-# LANGUAGE DataKinds #-}
3+{-# LANGUAGE DerivingVia #-}
34{-# LANGUAGE FlexibleContexts #-}
45{-# LANGUAGE FlexibleInstances #-}
56{-# LANGUAGE GADTs #-}
6−{-# LANGUAGE InstanceSigs #-}
7+{-# LANGUAGE KindSignatures #-}
78{-# LANGUAGE MultiParamTypeClasses #-}
89{-# LANGUAGE NoStarIsType #-}
10+{-# LANGUAGE RankNTypes #-}
911{-# LANGUAGE ScopedTypeVariables #-}
10−{-# LANGUAGE StandaloneDeriving #-}
1112{-# LANGUAGE TypeApplications #-}
12−{-# LANGUAGE TypeFamilies #-}
1313{-# LANGUAGE TypeOperators #-}
1414{-# LANGUAGE UndecidableInstances #-}
1515
@@ -27,24 +27,38 @@
2727-- in Haskell. See <https://github.com/bolt12/master-thesis my Msc Thesis> for the
2828-- motivation behind the library, the underlying theory, and implementation details.
2929--
30−-- This module offers many of the combinators mentioned in the work of
31−-- Macedo (2012) and Oliveira (2012).
30+-- This module offers a newtype wrapper around 'Matrix.Type.Matrix' that
31+-- uses arbitrary types instead of canonical data types for the matrices
32+-- dimensions.
33+--
34+-- __NOTE__: If the types in the dimensions are custom they must need to
35+-- implement a 'Generic' instance.
3236--
3337-----------------------------------------------------------------------------
3438
3539module Matrix.Type
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.
40+ ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
41+ --
42+ -- LAoP generalises relations and functions treating them as
43+ -- Boolean matrices and in turn consider these as arrows.
44+ -- This library offers many of the combinators mentioned in the work of
45+ -- Macedo (2012) and Oliveira (2012).
46+ --
47+ -- This definition is a wrapper around 'Matrix.Type' but
48+ -- dimensions are arbitrary data types. Type inference might not
49+ -- be as desired.
50+
51+ -- __NOTE__: If the types in the dimensions are custom they must need to
52+ -- implement a 'Generic' instance.
3953 --
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.
4454
4555 -- * Type safe matrix representation
4656 Matrix (..),
4757
58+ -- * Type aliases
59+ Zero,
60+ One,
61+
4862 -- * Primitives
4963 empty,
5064 one,
@@ -52,12 +66,12 @@ module Matrix.Type
5266 split,
5367
5468 -- * Auxiliary type families
55− FromNat,
56− Count,
57− Normalize,
69+ I.FromNat,
70+ I.Count,
71+ I.Normalize,
5872
5973 -- * Matrix construction and conversion
60− FromLists,
74+ I.FromLists,
6175 fromLists,
6276 toLists,
6377 toList,
@@ -128,214 +142,106 @@ module Matrix.Type
128142 pretty,
129143 prettyPrint
130144 )
131− where
145+where
132146
133−import Utils
134−import Data.Bool
135−import Data.Kind
136−import Data.List
137−import Data.Proxy
138147import Data.Void
139−import GHC.TypeLits
140−import Data.Type.Equality
141−import GHC.Generics
148+import Data.Proxy
149+import Data.Kind
150+import GHC.TypeLits
142151import Control.DeepSeq
152+import qualified Control.Category as C
153+import qualified Matrix.Internal as I
143154
144−-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
145−data Matrix e cols rows where
146− Empty :: Matrix e Void Void
147− One :: e -> Matrix e () ()
148− Junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
149− Split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
150−
151−deriving instance (Show e) => Show (Matrix e cols rows)
152−
153−-- | Type family that computes the cardinality of a given type dimension.
154−-- It can also count the cardinality of custom types that implement the
155−-- 'Generic' instance.
156−type family Count (d :: Type) where
157− Count (Natural n m) = (m - n) + 1
158− Count (Either a b) = (+) (Count a) (Count b)
159− Count (a, b) = (*) (Count a) (Count b)
160− Count (a -> b) = (^) (Count b) (Count a)
161− -- Generics
162− Count (M1 _ _ f p) = Count (f p)
163− Count (K1 _ _ _) = 1
164− Count (V1 _) = 0
165− Count (U1 _) = 1
166− Count ((:*:) a b p) = Count (a p) * Count (b p)
167− Count ((:+:) a b p) = Count (a p) + Count (b p)
168− Count d = Count (Rep d R)
169−
170−-- | Type family that computes of a given type dimension from a given natural
171−-- Thanks to Li-Yao Xia this type family is super fast.
172−type family FromNat (n :: Nat) where
173− FromNat 0 = Void
174− FromNat 1 = ()
175− FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
176−
177−type family FromNat' (b :: Bool) (m :: Type) :: Type where
178− FromNat' 'True m = Either m m
179− FromNat' 'False m = Either () (Either m m)
180−
181−-- | Type family that normalizes the representation of a given data
182−-- structure
183−type family Normalize (d :: Type) where
184− Normalize d = FromNat (Count d)
185−
186−instance NFData e => NFData (Matrix e cols rows) where
187− rnf Empty = ()
188− rnf (One e) = rnf e
189− rnf (Junc a b) = rnf a `seq` rnf b
190− rnf (Split a b) = rnf a `seq` rnf b
191−
192−instance Eq e => Eq (Matrix e cols rows) where
193− Empty == Empty = True
194− (One a) == (One b) = a == b
195− (Junc a b) == (Junc c d) = a == c && b == d
196− (Split a b) == (Split c d) = a == c && b == d
197− x@(Split a b) == y@(Junc c d) = x == abideJS y
198− x@(Junc a b) == y@(Split c d) = abideJS x == y
199−
200−instance Num e => Num (Matrix e cols rows) where
201−
202− Empty + Empty = Empty
203− (One a) + (One b) = One (a + b)
204− (Junc a b) + (Junc c d) = Junc (a + c) (b + d)
205− (Split a b) + (Split c d) = Split (a + c) (b + d)
206− x@(Split a b) + y@(Junc c d) = x + abideJS y
207− x@(Junc a b) + y@(Split c d) = abideJS x + y
208−
209− Empty - Empty = Empty
210− (One a) - (One b) = One (a - b)
211− (Junc a b) - (Junc c d) = Junc (a - c) (b - d)
212− (Split a b) - (Split c d) = Split (a - c) (b - d)
213− x@(Split a b) - y@(Junc c d) = x - abideJS y
214− x@(Junc a b) - y@(Split c d) = abideJS x - y
215−
216− Empty * Empty = Empty
217− (One a) * (One b) = One (a * b)
218− (Junc a b) * (Junc c d) = Junc (a * c) (b * d)
219− (Split a b) * (Split c d) = Split (a * c) (b * d)
220− x@(Split a b) * y@(Junc c d) = x * abideJS y
221− x@(Junc a b) * y@(Split c d) = abideJS x * y
222−
223− abs Empty = Empty
224− abs (One a) = One (abs a)
225− abs (Junc a b) = Junc (abs a) (abs b)
226− abs (Split a b) = Split (abs a) (abs b)
227−
228− signum Empty = Empty
229− signum (One a) = One (signum a)
230− signum (Junc a b) = Junc (signum a) (signum b)
231− signum (Split a b) = Split (signum a) (signum b)
155+newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
156+ deriving (Show, Num, Eq, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
157+
158+-- | It isn't possible to implement the 'id' function so it's
159+-- implementation is 'undefined'. However 'comp' can be and this partial
160+-- class implementation exists just to make the code more readable.
161+--
162+-- Please use 'identity' instead.
163+instance (Num e) => C.Category (Matrix e) where
164+ id = undefined
165+ (.) = comp
166+
167+-- | Zero type alias
168+type Zero = Void
169+
170+-- | One type alias
171+type One = ()
232172
233173-- Primitives
234174
235175-- | Empty matrix constructor
236−empty :: Matrix e Void Void
237−empty = Empty
176+empty :: Matrix e Zero Zero
177+empty = M I.Empty
238178
239179-- | Unit matrix constructor
240−one :: e -> Matrix e () ()
241−one = One
180+one :: e -> Matrix e One One
181+one = M . I.One
242182
243183-- | Matrix 'Junc' constructor
244−junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
245−junc = Junc
184+junc ::
185+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
186+ Matrix e a rows ->
187+ Matrix e b rows ->
188+ Matrix e (Either a b) rows
189+junc (M a) (M b) = M (I.Junc a b)
246190
247191infixl 3 |||
248−
249192-- | Matrix 'Junc' constructor
250−(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
251−(|||) = Junc
193+(|||) ::
194+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
195+ Matrix e a rows ->
196+ Matrix e b rows ->
197+ Matrix e (Either a b) rows
198+(|||) = junc
252199
253200-- | Matrix 'Split' constructor
254−split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
255−split = Split
201+split ::
202+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
203+ Matrix e cols a ->
204+ Matrix e cols b ->
205+ Matrix e cols (Either a b)
206+split (M a) (M b) = M (I.Split a b)
256207
257208infixl 2 ===
258−
259209-- | Matrix 'Split' constructor
260−(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
261−(===) = Split
210+(===) ::
211+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
212+ Matrix e cols a ->
213+ Matrix e cols b ->
214+ Matrix e cols (Either a b)
215+(===) = split
262216
263217-- Construction
264218
265−-- | Type class for defining the 'fromList' conversion function.
266−-- Given that it is not possible to branch on types at the term level type
267−-- classes are needed bery much like an inductive definition but on types.
268−class FromLists e cols rows where
269− -- | Build a matrix out of a list of list of elements. Throws a runtime
270− -- error if the dimensions do not match.
271− fromLists :: [[e]] -> Matrix e cols rows
272−
273−instance FromLists e Void Void where
274− fromLists [] = Empty
275− fromLists _ = error "Wrong dimensions"
276−
277−instance {-# OVERLAPPING #-} FromLists e () () where
278− fromLists [[e]] = One e
279− fromLists _ = error "Wrong dimensions"
280−
281−instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
282− fromLists [h : t] = Junc (One h) (fromLists [t])
283− fromLists _ = error "Wrong dimensions"
284−
285−instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), KnownNat (Count a)) => FromLists e (Either a b) () where
286− fromLists [l] =
287− let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
288− in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])
289− fromLists _ = error "Wrong dimensions"
290−
291−instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
292− fromLists ([h] : t) = Split (One h) (fromLists t)
293− fromLists _ = error "Wrong dimensions"
294−
295−instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, KnownNat (Count a)) => FromLists e () (Either a b) where
296− fromLists l@([h] : t) =
297− let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
298− in Split (fromLists (take rowsA l)) (fromLists (drop rowsA l))
299− fromLists _ = error "Wrong dimensions"
300−
301−instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a b) d, KnownNat (Count c)) => FromLists e (Either a b) (Either c d) where
302− fromLists l@(h : t) =
303− let lh = length h
304− rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
305− condition = all (== lh) (map length t)
306− in if lh > 0 && condition
307− then Split (fromLists (take rowsC l)) (fromLists (drop rowsC l))
308− else error "Not all rows have the same length"
219+-- | Build a matrix out of a list of list of elements. Throws a runtime
220+-- error if the dimensions do not match.
221+fromLists :: (I.FromLists e (I.Normalize cols) (I.Normalize rows)) => [[e]] -> Matrix e cols rows
222+fromLists = M . I.fromLists
309223
310224-- | Matrix builder function. Constructs a matrix provided with
311225-- a construction function.
312226matrixBuilder ::
313− forall e cols rows.
314− ( FromLists e cols rows,
315− KnownNat (Count cols),
316− KnownNat (Count rows)
317− ) =>
227+ (I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
318228 ((Int, Int) -> e) ->
319229 Matrix e cols rows
320−matrixBuilder f =
321− let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
322− r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
323− positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
324− in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
230+matrixBuilder = M . I.matrixBuilder
325231
326232-- | Constructs a column vector matrix
327−col :: (FromLists e () rows) => [e] -> Matrix e () rows
328−col = fromLists . map (: [])
233+col :: (I.FromLists e () (I.Normalize rows)) => [e] -> Matrix e One rows
234+col = M . I.col
329235
330236-- | Constructs a row vector matrix
331−row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
332−row = fromLists . (: [])
237+row :: (I.FromLists e (I.Normalize cols) ()) => [e] -> Matrix e cols One
238+row = M . I.row
333239
334240-- | Lifts functions to matrices with arbitrary dimensions.
335−-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
241+--
242+-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
336243-- types @a@ or @b@ allows.
337244fromF ::
338− forall a b cols rows e.
339245 ( Bounded a,
340246 Bounded b,
341247 Enum a,
@@ -343,35 +249,17 @@ fromF ::
343249 Eq b,
344250 Num e,
345251 Ord e,
346− KnownNat (Count cols),
347− KnownNat (Count rows),
348− FromLists e rows cols
252+ KnownNat (I.Count (I.Normalize cols)),
253+ KnownNat (I.Count (I.Normalize rows)),
254+ I.FromLists e (I.Normalize rows) (I.Normalize cols)
349255 ) =>
350256 (a -> b) ->
351257 Matrix e cols rows
352−fromF f =
353− let minA = minBound @a
354− maxA = maxBound @a
355− minB = minBound @b
356− maxB = maxBound @b
357− ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
358− rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
359− elementsA = take ccols [minA .. maxA]
360− elementsB = take rrows [minB .. maxB]
361− combinations = (,) <$> elementsA <*> elementsB
362− combAp = map snd . sort . map (\(a, b) -> if f a == b
363− then ((fromEnum a, fromEnum b), 1)
364− else ((fromEnum a, fromEnum b), 0)) $ combinations
365− mList = buildList combAp rrows
366− in tr $ fromLists mList
367− where
368− buildList [] _ = []
369− buildList l r = take r l : buildList (drop r l) r
258+fromF = M . I.fromF
370259
371260-- | Lifts functions to matrices with dimensions matching @a@ and @b@
372261-- cardinality's.
373262fromF' ::
374− forall a b e.
375263 ( Bounded a,
376264 Bounded b,
377265 Enum a,
@@ -379,133 +267,149 @@ fromF' ::
379267 Eq b,
380268 Num e,
381269 Ord e,
382− KnownNat (Count (Normalize a)),
383− KnownNat (Count (Normalize b)),
384− FromLists e (Normalize b) (Normalize a)
270+ KnownNat (I.Count (I.Normalize a)),
271+ KnownNat (I.Count (I.Normalize b)),
272+ I.FromLists e (I.Normalize b) (I.Normalize a)
385273 ) =>
386274 (a -> b) ->
387− Matrix e (Normalize a) (Normalize b)
388−fromF' f =
389− let minA = minBound @a
390− maxA = maxBound @a
391− minB = minBound @b
392− maxB = maxBound @b
393− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
394− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
395− elementsA = take ccols [minA .. maxA]
396− elementsB = take rrows [minB .. maxB]
397− combinations = (,) <$> elementsA <*> elementsB
398− combAp = map snd . sort . map (\(a, b) -> if f a == b
399− then ((fromEnum a, fromEnum b), 1)
400− else ((fromEnum a, fromEnum b), 0)) $ combinations
401− mList = buildList combAp rrows
402− in tr $ fromLists mList
403− where
404− buildList [] _ = []
405− buildList l r = take r l : buildList (drop r l) r
275+ Matrix e a b
276+fromF' = M . I.fromF'
406277
407278-- Conversion
408279
409280-- | Converts a matrix to a list of lists of elements.
410281toLists :: Matrix e cols rows -> [[e]]
411−toLists Empty = []
412−toLists (One e) = [[e]]
413−toLists (Split l r) = toLists l ++ toLists r
414−toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
282+toLists (M m) = I.toLists m
415283
416284-- | Converts a matrix to a list of elements.
417285toList :: Matrix e cols rows -> [e]
418−toList = concat . toLists
286+toList (M m) = I.toList m
419287
420288-- Zeros Matrix
421289
422290-- | The zero matrix. A matrix wholly filled with zeros.
423−zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
424−zeros = matrixBuilder (const 0)
291+zeros ::
292+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
293+ Matrix e cols rows
294+zeros = M I.zeros
425295
426296-- Ones Matrix
427297
428298-- | The ones matrix. A matrix wholly filled with ones.
429−-- Also known as T (Top) matrix.
430−ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
431−ones = matrixBuilder (const 1)
299+--
300+-- Also known as T (Top) matrix.
301+ones ::
302+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
303+ Matrix e cols rows
304+ones = M I.ones
432305
433306-- Const Matrix
434307
435308-- | The constant matrix constructor. A matrix wholly filled with a given
436309-- value.
437−constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows
438−constant e = matrixBuilder (const e)
310+constant ::
311+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
312+ e ->
313+ Matrix e cols rows
314+constant = M . I.constant
439315
440316-- Bang Matrix
441317
442318-- | The T (Top) row vector matrix.
443−bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()
444−bang =
445− let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
446− in fromLists [take c [1, 1 ..]]
319+bang ::
320+ forall e cols.
321+ (Num e, Enum e, I.FromLists e (I.Normalize cols) (), KnownNat (I.Count (I.Normalize cols))) =>
322+ Matrix e cols One
323+bang = M I.bang
447324
448325-- Identity Matrix
449326
450−-- | Identity matrix.
451−identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols
452−identity = matrixBuilder (bool 0 1 . uncurry (==))
327+-- | Identity matrix
328+identity ::
329+ (Num e, I.FromLists e (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
330+ Matrix e a a
331+identity = M I.identity
453332
454333-- Matrix composition (MMM)
455334
456335-- | Matrix composition. Equivalent to matrix-matrix multiplication.
457−-- This definition takes advantage of divide-and-conquer and fusion laws
336+--
337+-- This definition takes advantage of divide-and-conquer and fusion laws
458338-- from LAoP.
459339comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
460−comp Empty Empty = Empty
461−comp (One a) (One b) = One (a * b)
462−comp (Junc a b) (Split c d) = comp a c + comp b d -- Divide-and-conquer law
463−comp (Split a b) c = Split (comp a c) (comp b c) -- Split fusion law
464−comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc fusion law
465−
466−-- Projections
340+comp (M a) (M b) = M (I.comp a b)
467341
468342-- | Biproduct first component projection
469−p1 :: forall e m n. (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e (Either m n) m
470−p1 =
471− let iden = identity :: Matrix e m m
472− zero = zeros :: Matrix e n m
473− in junc iden zero
343+p1 ::
344+ ( Num e,
345+ KnownNat (I.Count (I.Normalize n)),
346+ KnownNat (I.Count (I.Normalize m)),
347+ I.FromLists e (I.Normalize n) (I.Normalize m),
348+ I.FromLists e (I.Normalize m) (I.Normalize m),
349+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
350+ ) =>
351+ Matrix e (Either m n) m
352+p1 = M I.p1
474353
475354-- | Biproduct second component projection
476−p2 :: forall e m n. (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e (Either m n) n
477−p2 =
478− let iden = identity :: Matrix e n n
479− zero = zeros :: Matrix e m n
480− in junc zero iden
355+p2 ::
356+ ( Num e,
357+ KnownNat (I.Count (I.Normalize n)),
358+ KnownNat (I.Count (I.Normalize m)),
359+ I.FromLists e (I.Normalize m) (I.Normalize n),
360+ I.FromLists e (I.Normalize n) (I.Normalize n),
361+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
362+ ) =>
363+ Matrix e (Either m n) n
364+p2 = M I.p2
481365
482366-- Injections
483367
484368-- | Biproduct first component injection
485−i1 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
369+i1 ::
370+ ( Num e,
371+ KnownNat (I.Count (I.Normalize n)),
372+ KnownNat (I.Count (I.Normalize m)),
373+ I.FromLists e (I.Normalize n) (I.Normalize m),
374+ I.FromLists e (I.Normalize m) (I.Normalize m),
375+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
376+ ) =>
377+ Matrix e m (Either m n)
486378i1 = tr p1
487379
488380-- | Biproduct second component injection
489−i2 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
381+i2 ::
382+ ( Num e,
383+ KnownNat (I.Count (I.Normalize n)),
384+ KnownNat (I.Count (I.Normalize m)),
385+ I.FromLists e (I.Normalize m) (I.Normalize n),
386+ I.FromLists e (I.Normalize n) (I.Normalize n),
387+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
388+ ) =>
389+ Matrix e n (Either m n)
490390i2 = tr p2
491391
492392-- Dimensions
493393
494394-- | Obtain the number of rows.
495−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
395+--
396+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
496397-- dimensions in constant time.
398+--
497399-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
498400-- exchange for performance.
499−rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int
500−rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
401+rows :: (KnownNat (I.Count (I.Normalize rows))) => Matrix e cols rows -> Int
402+rows (M m) = I.rows m
501403
502404-- | Obtain the number of columns.
503−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
405+--
406+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
504407-- dimensions in constant time.
408+--
505409-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
506410-- exchange for performance.
507−columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int
508−columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
411+columns :: (KnownNat (I.Count (I.Normalize cols))) => Matrix e cols rows -> Int
412+columns (M m) = I.columns m
509413
510414-- Coproduct Bifunctor
511415
@@ -513,19 +417,20 @@ infixl 5 -|-
513417
514418-- | Matrix coproduct functor also known as matrix direct sum.
515419(-|-) ::
516− forall e n k m j.
517420 ( Num e,
518− KnownNat (Count j),
519− KnownNat (Count k),
520− FromLists e k k,
521− FromLists e j k,
522− FromLists e k j,
523− FromLists e j j
421+ KnownNat (I.Count (I.Normalize j)),
422+ KnownNat (I.Count (I.Normalize k)),
423+ I.FromLists e (I.Normalize k) (I.Normalize k),
424+ I.FromLists e (I.Normalize j) (I.Normalize k),
425+ I.FromLists e (I.Normalize k) (I.Normalize j),
426+ I.FromLists e (I.Normalize j) (I.Normalize j),
427+ I.Normalize (Either n m) ~ Either (I.Normalize n) (I.Normalize m),
428+ I.Normalize (Either k j) ~ Either (I.Normalize k) (I.Normalize j)
524429 ) =>
525430 Matrix e n k ->
526431 Matrix e m j ->
527432 Matrix e (Either n m) (Either k j)
528−(-|-) a b = Junc (comp i1 a) (comp i2 b)
433+(-|-) (M a) (M b) = M ((I.-|-) a b)
529434
530435-- Khatri Rao Product and projections
531436
@@ -533,36 +438,29 @@ infixl 5 -|-
533438kp1 ::
534439 forall e m k .
535440 ( Num e,
536− KnownNat (Count k),
537− FromLists e (FromNat (Count m * Count k)) m,
538− KnownNat (Count m),
539− KnownNat (Count (Normalize (m, k)))
540− ) => Matrix e (Normalize (m, k)) m
541−kp1 = matrixBuilder f
542− where
543− offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
544− f (x, y)
545− | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
546− | otherwise = 0
441+ KnownNat (I.Count (I.Normalize m)),
442+ KnownNat (I.Count (I.Normalize k)),
443+ KnownNat (I.Count (I.Normalize (m, k))),
444+ I.FromLists e (I.Normalize (m, k)) (I.Normalize m),
445+ I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
446+ ) => Matrix e (m, k) m
447+kp1 = M (I.kp1 @e @(I.Normalize m) @(I.Normalize k))
547448
548449-- | Khatri Rao product second component projection matrix.
549450kp2 ::
550− forall e m k .
451+ forall e m k.
551452 ( Num e,
552− KnownNat (Count k),
553− FromLists e (FromNat (Count m * Count k)) k,
554− KnownNat (Count m),
555− KnownNat (Count (Normalize (m, k)))
556− ) => Matrix e (Normalize (m, k)) k
557−kp2 = matrixBuilder f
558− where
559− offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
560− f (x, y)
561− | x == y || mod (y - x) offset == 0 = 1
562− | otherwise = 0
453+ KnownNat (I.Count (I.Normalize k)),
454+ KnownNat (I.Count (I.Normalize m)),
455+ KnownNat (I.Count (I.Normalize (m, k))),
456+ I.FromLists e (I.Normalize (m, k)) (I.Normalize k),
457+ I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
458+ ) => Matrix e (m, k) k
459+kp2 = M (I.kp2 @e @(I.Normalize m) @(I.Normalize k))
563460
564461-- | Khatri Rao Matrix product also known as matrix pairing.
565−-- NOTE: That this is not a true categorical product, see for instance:
462+--
463+-- NOTE: That this is not a true categorical product, see for instance:
566464--
567465-- @
568466-- | kp1 `comp` khatri a b == a
@@ -571,15 +469,16 @@ kp2 = matrixBuilder f
571469-- @
572470--
573471-- __Emphasis__ on the implication symbol.
574−khatri ::
575− forall e cols a b.
576− ( Num e,
577− KnownNat (Count a),
578− KnownNat (Count b),
579− KnownNat (Count (Normalize (a, b))),
580− FromLists e (Normalize (a, b)) a,
581− FromLists e (Normalize (a, b)) b
582− ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
472+khatri ::
473+ forall e cols a b.
474+ ( Num e,
475+ KnownNat (I.Count (I.Normalize a)),
476+ KnownNat (I.Count (I.Normalize b)),
477+ KnownNat (I.Count (I.Normalize (a, b))),
478+ I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
479+ I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
480+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
481+ ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, b)
583482khatri a b =
584483 let kp1' = kp1 @e @a @b
585484 kp2' = kp2 @e @a @b
@@ -590,21 +489,22 @@ khatri a b =
590489infixl 4 ><
591490
592491-- | Matrix product functor also known as kronecker product
593−(><) ::
594− forall e m p n q.
595− ( Num e,
596− KnownNat (Count m),
597− KnownNat (Count n),
598− KnownNat (Count p),
599− KnownNat (Count q),
600− KnownNat (Count (Normalize (m, n))),
601− FromLists e (Normalize (m, n)) m,
602− FromLists e (Normalize (m, n)) n,
603− KnownNat (Count (Normalize (p, q))),
604− FromLists e (Normalize (p, q)) p,
605− FromLists e (Normalize (p, q)) q
606− )
607− => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
492+(><) ::
493+ forall e m p n q.
494+ ( Num e,
495+ KnownNat (I.Count (I.Normalize m)),
496+ KnownNat (I.Count (I.Normalize n)),
497+ KnownNat (I.Count (I.Normalize p)),
498+ KnownNat (I.Count (I.Normalize q)),
499+ KnownNat (I.Count (I.Normalize (m, n))),
500+ KnownNat (I.Count (I.Normalize (p, q))),
501+ I.FromLists e (I.Normalize (m, n)) (I.Normalize m),
502+ I.FromLists e (I.Normalize (m, n)) (I.Normalize n),
503+ I.FromLists e (I.Normalize (p, q)) (I.Normalize p),
504+ I.FromLists e (I.Normalize (p, q)) (I.Normalize q),
505+ I.Normalize (m, n) ~ I.Normalize (I.Normalize m, I.Normalize n),
506+ I.Normalize (p, q) ~ I.Normalize (I.Normalize p, I.Normalize q)
507+ ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)
608508(><) a b =
609509 let kp1' = kp1 @e @m @n
610510 kp2' = kp2 @e @m @n
@@ -614,132 +514,78 @@ infixl 4 ><
614514
615515-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
616516--
517+-- Law:
518+--
617519-- @
618520-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
619521-- @
620522abideJS :: Matrix e cols rows -> Matrix e cols rows
621−abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law
622−abideJS Empty = Empty
623−abideJS (One e) = One e
624−abideJS (Junc a b) = Junc (abideJS a) (abideJS b)
625−abideJS (Split a b) = Split (abideJS a) (abideJS b)
523+abideJS (M m) = M (I.abideJS m)
626524
627525-- Matrix abide Split Junc
628526
629527-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
630528--
529+-- Law:
530+--
631531-- @
632532-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
633533-- @
634534abideSJ :: Matrix e cols rows -> Matrix e cols rows
635−abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law
636−abideSJ Empty = Empty
637−abideSJ (One e) = One e
638−abideSJ (Junc a b) = Junc (abideSJ a) (abideSJ b)
639−abideSJ (Split a b) = Split (abideSJ a) (abideSJ b)
535+abideSJ (M m) = M (I.abideSJ m)
640536
641537-- Matrix transposition
642538
643539-- | Matrix transposition.
644540tr :: Matrix e cols rows -> Matrix e rows cols
645−tr Empty = Empty
646−tr (One e) = One e
647−tr (Junc a b) = Split (tr a) (tr b)
648−tr (Split a b) = Junc (tr a) (tr b)
541+tr (M m) = M (I.tr m)
649542
650543-- Selective 'select' operator
651544
652545-- | Selective functors 'select' operator equivalent inspired by the
653546-- ArrowMonad solution presented in the paper.
654−select :: (Bounded a1, Bounded b, Enum a1, Enum b, Num e, Ord e,
655− KnownNat (Count a2), KnownNat (Count rows), FromLists e rows a2,
656− FromLists e rows rows, Eq b) =>
657− Matrix e cols (Either a2 rows) -> (a1 -> b) -> Matrix e cols rows
658−select m y =
659− let f = fromF y
660− in junc f identity `comp` m
547+select ::
548+ ( Bounded a,
549+ Bounded b,
550+ Enum a,
551+ Eq b,
552+ Enum b,
553+ Num e,
554+ Ord e,
555+ KnownNat (I.Count (I.Normalize a)),
556+ KnownNat (I.Count (I.Normalize b)),
557+ KnownNat (I.Count (I.Normalize cols)),
558+ I.FromLists e (I.Normalize b) (I.Normalize a),
559+ I.FromLists e (I.Normalize b) (I.Normalize b),
560+ I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
561+ )
562+ => Matrix e cols (Either a b) -> (a -> b) -> Matrix e cols b
563+select (M m) y = M (I.select m y)
661564
662565-- McCarthy's Conditional
663566
664567-- | McCarthy's Conditional expresses probabilistic choice.
665568cond ::
666− ( cols ~ FromNat (Count cols),
667− KnownNat (Count cols),
668− FromLists e () cols,
669− FromLists e cols (),
670− FromLists e cols cols,
569+ ( I.Normalize (I.Normalize a) ~ I.Normalize a,
570+ KnownNat (I.Count (I.Normalize a)),
571+ I.FromLists e () (I.Normalize a),
572+ I.FromLists e (I.Normalize a) (),
573+ I.FromLists e (I.Normalize a) (I.Normalize a),
671574 Bounded a,
672575 Enum a,
673576 Num e,
674577 Ord e
675578 )
676579 =>
677− (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
678−cond p f g = junc f g `comp` grd p
679−
680−grd ::
681− ( q ~ FromNat (Count q),
682− KnownNat (Count q),
683− FromLists e () q,
684− FromLists e q (),
685− FromLists e q q,
686− Bounded a,
687− Enum a,
688− Num e,
689− Ord e
690− )
691− =>
692− (a -> Bool) -> Matrix e q (Either q q)
693−grd f = split (corr f) (corr (not . f))
694−
695−corr ::
696− forall e a q .
697− ( q ~ FromNat (Count q),
698− KnownNat (Count q),
699− FromLists e () q,
700− FromLists e q (),
701− FromLists e q q,
702− Bounded a,
703− Enum a,
704− Num e,
705− Ord e
706− )
707− => (a -> Bool) -> Matrix e q q
708−corr p = let f = fromF p :: Matrix e q ()
709− in khatri f (identity :: Matrix e q q)
580+ (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b
581+cond p (M a) (M b) = M (I.cond p a b)
710582
711583-- Pretty print
712584
713−prettyAux :: Show e => [[e]] -> [[e]] -> String
714−prettyAux [] _ = ""
715−prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
716− where
717− v = fmap show m
718− widest = maximum $ fmap length v
719− fill str = replicate (widest - length str - 2) ' ' ++ str
720−prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
721− where
722− v = fmap show m
723− widest = maximum $ fmap length v
724− fill str = replicate (widest - length str - 2) ' ' ++ str
725−prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
726− prettyAux t l
727− where
728− v = fmap show l
729− widest = maximum $ fmap length v
730− fill str = replicate (widest - length str - 2) ' ' ++ str
731−
732585-- | Matrix pretty printer
733−pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String
734−pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
735− prettyAux (toLists m) (toLists m) ++
736− "└ " ++ unwords (replicate (columns m) blank) ++ " ┘"
737− where
738− v = fmap show (toList m)
739− widest = maximum $ fmap length v
740− fill str = replicate (widest - length str) ' ' ++ str
741− blank = fill ""
586+pretty :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> String
587+pretty (M m) = I.pretty m
742588
743589-- | Matrix pretty printer
744−prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()
745−prettyPrint = putStrLn . pretty
590+prettyPrint :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> IO ()
591+prettyPrint (M m) = I.prettyPrint m