git.iko.soy/laop
on master help sign in
Changed modules structure. Added Matrix.Type
c5fb386Armando Santos
app/Main.hs+32−25
compare with master
unifiedsplit
@@ -1,3 +1,4 @@
1+{-# LANGUAGE DeriveGeneric #-}
1{-# LANGUAGE FlexibleContexts #-}
2{-# LANGUAGE FlexibleContexts #-}
2{-# LANGUAGE TypeOperators #-}
3{-# LANGUAGE TypeOperators #-}
3{-# LANGUAGE TypeApplications #-}
4{-# LANGUAGE TypeApplications #-}
@@ -5,25 +6,28 @@
5
6
6module Main where
7module Main where
7
8
8−import Matrix.Nat
9+import Matrix.Type
9import Utils
10import Utils
10import Dist
11import Dist
11import GHC.TypeLits
12import GHC.TypeLits
12import Data.Coerce
13import Data.Coerce
14+import GHC.Generics
15+import Control.Category hiding (id)
16+import Prelude hiding ((.))
13
17
14-- Monty Hall Problem
18-- Monty Hall Problem
15data Outcome = Win | Lose
19data Outcome = Win | Lose
16− deriving (Bounded, Enum, Eq, Show)
20+ deriving (Bounded, Enum, Eq, Show, Generic)
17
21
18switch :: Outcome -> Outcome
22switch :: Outcome -> Outcome
19switch Win = Lose
23switch Win = Lose
20switch Lose = Win
24switch Lose = Win
21
25
22−firstChoice :: Dist Outcome m
26+firstChoice :: Dist Outcome
23firstChoice = col [1/3, 2/3]
27firstChoice = col [1/3, 2/3]
24
28
25−secondChoice :: Matrix Double 2 2
29+secondChoice :: Matrix Double Outcome Outcome
26−secondChoice = fromF switch
30+secondChoice = fromF' switch
27
31
28-- Dice sum
32-- Dice sum
29
33
@@ -42,40 +46,43 @@ condition (fst, snd) thrd = if fst == snd
42conditionSS :: (SS, SS) -> SS -> Natural 3 18
46conditionSS :: (SS, SS) -> SS -> Natural 3 18
43conditionSS = coerceNat2 condition
47conditionSS = coerceNat2 condition
44
48
45−conditionalThrows = fromF' (uncurry conditionSS) `comp` khatri die (khatri die die)
49+conditionalThrows = fromF' (uncurry conditionSS) . khatri (khatri die die) die
46
50
47−die :: Dist (Natural 1 6) 6
51+die :: Dist SS
48die = uniform [nat @1 @6 1 .. nat 6]
52die = uniform [nat @1 @6 1 .. nat 6]
49
53
50-- Sprinkler
54-- Sprinkler
51
55
52−rain :: Dist Bool 2
56+rain :: Dist Bool
53rain = choose 0.8
57rain = choose 0.8
54
58
55−sprinkler :: Matrix Double 2 2
59+sprinkler :: Matrix Double Bool Bool
56sprinkler = fromLists [[0.6, 0.99], [0.4, 0.01]]
60sprinkler = fromLists [[0.6, 0.99], [0.4, 0.01]]
57
61
58−grass :: Matrix Double 4 2
62+grass :: Matrix Double (Bool, Bool) Bool
59grass = fromLists [[1, 0.2, 0.1, 0.01], [0, 0.8, 0.9, 0.99]]
63grass = fromLists [[1, 0.2, 0.1, 0.01], [0, 0.8, 0.9, 0.99]]
60
64
65+state :: Dist (Bool, (Bool, Bool))
61−state = khatri grass identity `comp` khatri sprinkler identity `comp` rain
66+state = khatri grass identity . khatri sprinkler identity . rain
62
67
63−grass_wet = row [0,1] `comp` kp1 @Double @2 @4
68+grass_wet :: Matrix Double (Bool, (Bool, Bool)) One
69+grass_wet = row [0,1] . kp1
64
70
65−rainning = row [0,1] `comp` kp2 @Double @2 @2 `comp` kp2 @Double @2 @4
71+rainning :: Matrix Double (Bool, (Bool, Bool)) One
72+rainning = row [0,1] . kp2 . kp2
66
73
67main :: IO ()
74main :: IO ()
68main = do
75main = do
69− putStrLn "Monty Hall Problem solution:"
76+ -- putStrLn "Monty Hall Problem solution:"
70− prettyPrint (p1 @Double @1 `comp` secondChoice `comp` firstChoice)
77+ -- prettyPrint (secondChoice . firstChoice)
71− putStrLn "\n Sum of dices probability:"
78+ -- putStrLn "\n Sum of dices probability:"
72− prettyPrint (sumSSM `comp` khatri die die)
79+ -- prettyPrint (sumSSM `comp` khatri die die)
73− prettyPrintDist @(Natural 2 12) (sumSSM `comp` khatri die die)
80+ -- prettyPrintDist @(Natural 2 12) (sumSSM . khatri die die)
74− putStrLn "\n Conditional dice throw:"
81+ -- putStrLn "\n Conditional dice throw:"
75− prettyPrintDist @(Natural 3 18) conditionalThrows
82+ -- prettyPrintDist @(Natural 3 18) conditionalThrows
76− putStrLn "\n Checking that the last result is indeed a distribution: "
83+ -- putStrLn "\n Checking that the last result is indeed a distribution: "
77− prettyPrint (bang `comp` sumSSM `comp` khatri die die)
84+ -- prettyPrint (bang . sumSSM . khatri die die)
78 putStrLn "\n Probability of grass being wet:"
85 putStrLn "\n Probability of grass being wet:"
79− prettyPrint (grass_wet `comp` state)
86+ prettyPrint (grass_wet . state)
80− putStrLn "\n Probability of rain:"
87+ -- putStrLn "\n Probability of rain:"
81− prettyPrint (rainning `comp` state)
88+ -- prettyPrint (rainning . state)
src/Dist/Internal.hs+13−13
@@ -22,7 +22,7 @@ module Dist.Internal
22 )
22 )
23 where
23 where
24
24
25−import Matrix.Nat
25+import Matrix.Type
26import Utils
26import Utils
27import GHC.TypeLits
27import GHC.TypeLits
28import Data.Proxy
28import Data.Proxy
@@ -33,14 +33,14 @@ type Prob = Double
33
33
34-- | Type synonym for column vector matrices. This represents a probability
34-- | Type synonym for column vector matrices. This represents a probability
35-- distribution.
35-- distribution.
36−type Dist a (m :: Nat) = (FromLists Prob () (FromNat m)) => Matrix Prob 1 m
36+type Dist a = (FromLists Prob () (Normalize a)) => Matrix Prob () a
37
37
38-- | Constructs a Bernoulli distribution
38-- | Constructs a Bernoulli distribution
39−choose :: Prob -> Dist a 2
39+choose :: Prob -> Dist a
40choose prob = col [prob, 1 - prob]
40choose prob = col [prob, 1 - prob]
41
41
42-- | Creates a distribution given a shape function
42-- | Creates a distribution given a shape function
43−shape :: (Prob -> Prob) -> [a] -> Dist a m
43+shape :: (Prob -> Prob) -> [a] -> Dist a
44shape _ [] = error "Probability.shape: empty list"
44shape _ [] = error "Probability.shape: empty list"
45shape f xs =
45shape f xs =
46 let incr = 1 / fromIntegral (length xs - 1)
46 let incr = 1 / fromIntegral (length xs - 1)
@@ -48,31 +48,31 @@ shape f xs =
48 in fromFreqs (zip xs ps)
48 in fromFreqs (zip xs ps)
49
49
50-- | Constructs a Linear distribution
50-- | Constructs a Linear distribution
51−linear :: [a] -> Dist a m
51+linear :: [a] -> Dist a
52linear = shape id
52linear = shape id
53
53
54-- | Constructs an Uniform distribution
54-- | Constructs an Uniform distribution
55−uniform :: [a] -> Dist a m
55+uniform :: [a] -> Dist a
56uniform = shape (const 1)
56uniform = shape (const 1)
57
57
58-- | Constructs an Negative Exponential distribution
58-- | Constructs an Negative Exponential distribution
59−negExp :: [a] -> Dist a m
59+negExp :: [a] -> Dist a
60negExp = shape (\x -> exp (-x))
60negExp = shape (\x -> exp (-x))
61
61
62-- | Constructs an Normal distribution
62-- | Constructs an Normal distribution
63−normal :: [a] -> Dist a m
63+normal :: [a] -> Dist a
64normal = shape (normalCurve 0.5 0.5)
64normal = shape (normalCurve 0.5 0.5)
65
65
66-- | Transforms a 'Dist' into a list of pairs.
66-- | Transforms a 'Dist' into a list of pairs.
67−toValues :: forall a m . (Enum a, KnownNat m, FromLists Prob () (FromNat m)) => Dist a m -> [(a, Prob)]
67+toValues :: forall a . (Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> [(a, Prob)]
68toValues d =
68toValues d =
69− let rows = fromInteger (natVal (Proxy :: Proxy m))
69+ let rows = fromInteger (natVal (Proxy :: Proxy (Count a)))
70 probs = toList d
70 probs = toList d
71 res = zip (map toEnum [0..rows]) probs
71 res = zip (map toEnum [0..rows]) probs
72 in res
72 in res
73
73
74-- | Pretty a distribution
74-- | Pretty a distribution
75−prettyDist :: forall a m . (Show a, Enum a, KnownNat m, FromLists Prob () (FromNat m)) => Dist a m -> String
75+prettyDist :: forall a. (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> String
76prettyDist d =
76prettyDist d =
77 let values = sortBy (\(a, p1) (b, p2) -> compare p2 p1) (toValues @a d)
77 let values = sortBy (\(a, p1) (b, p2) -> compare p2 p1) (toValues @a d)
78 w = maximum (map (length . show . fst) values)
78 w = maximum (map (length . show . fst) values)
@@ -84,12 +84,12 @@ prettyDist d =
84 showR n x = show x ++ " "
84 showR n x = show x ++ " "
85
85
86-- | Pretty Print a distribution
86-- | Pretty Print a distribution
87−prettyPrintDist :: forall a m . (Show a, Enum a, KnownNat m, FromLists Prob () (FromNat m)) => Dist a m -> IO ()
87+prettyPrintDist :: forall a . (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> IO ()
88prettyPrintDist = putStrLn . prettyDist @a
88prettyPrintDist = putStrLn . prettyDist @a
89
89
90-- Auxiliary functions
90-- Auxiliary functions
91
91
92−fromFreqs :: [(a,Prob)] -> Dist a m
92+fromFreqs :: [(a,Prob)] -> Dist a
93fromFreqs xs = col (map (\(x,p) -> p/q) xs)
93fromFreqs xs = col (map (\(x,p) -> p/q) xs)
94 where q = sum $ map snd xs
94 where q = sum $ map snd xs
95
95
src/Matrix/Internal.hsnew file+781
@@ -0,0 +1,781 @@
1+{-# LANGUAGE AllowAmbiguousTypes #-}
2+{-# LANGUAGE DataKinds #-}
3+{-# LANGUAGE FlexibleContexts #-}
4+{-# LANGUAGE FlexibleInstances #-}
5+{-# LANGUAGE GADTs #-}
6+{-# LANGUAGE InstanceSigs #-}
7+{-# LANGUAGE MultiParamTypeClasses #-}
8+{-# LANGUAGE NoStarIsType #-}
9+{-# LANGUAGE ScopedTypeVariables #-}
10+{-# LANGUAGE StandaloneDeriving #-}
11+{-# LANGUAGE TypeApplications #-}
12+{-# LANGUAGE TypeFamilies #-}
13+{-# LANGUAGE TypeOperators #-}
14+{-# LANGUAGE UndecidableInstances #-}
15+
16+-----------------------------------------------------------------------------
17+-- |
18+-- Module : Matrix.Internal
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+-- This is an Internal module and it is no supposed to be imported.
34+--
35+-----------------------------------------------------------------------------
36+
37+module Matrix.Internal
38+ ( -- | This definition makes use of the fact that 'Void' is
39+ -- isomorphic to 0 and '()' to 1 and captures matrix
40+ -- dimensions as stacks of 'Either's.
41+ --
42+ -- There exists two type families that make it easier to write
43+ -- matrix dimensions: 'FromNat' and 'Count'. This approach
44+ -- leads to a very straightforward implementation
45+ -- of LAoP combinators.
46+
47+ -- * Type safe matrix representation
48+ Matrix (..),
49+
50+ -- * Primitives
51+ empty,
52+ one,
53+ junc,
54+ split,
55+
56+ -- * Auxiliary type families
57+ FromNat,
58+ Count,
59+ Normalize,
60+
61+ -- * Matrix construction and conversion
62+ FromLists,
63+ fromLists,
64+ toLists,
65+ toList,
66+ matrixBuilder,
67+ row,
68+ col,
69+ zeros,
70+ ones,
71+ bang,
72+ constant,
73+
74+ -- * Misc
75+ -- ** Get dimensions
76+ columns,
77+ rows,
78+
79+ -- ** Matrix Transposition
80+ tr,
81+
82+ -- ** Selective operator
83+ select,
84+
85+ -- ** McCarthy's Conditional
86+ cond,
87+
88+ -- ** Matrix "abiding"
89+ abideJS,
90+ abideSJ,
91+
92+ -- * Biproduct approach
93+ -- ** Split
94+ (===),
95+ -- *** Projections
96+ p1,
97+ p2,
98+ -- ** Junc
99+ (|||),
100+ -- *** Injections
101+ i1,
102+ i2,
103+ -- ** Bifunctors
104+ (-|-),
105+ (><),
106+
107+ -- ** Applicative matrix combinators
108+
109+ -- | Note that given the restrictions imposed it is not possible to
110+ -- implement the standard type classes present in standard Haskell.
111+ -- *** Matrix pairing projections
112+ kp1,
113+ kp2,
114+
115+ -- *** Matrix pairing
116+ khatri,
117+
118+ -- * Matrix composition and lifting
119+
120+ -- ** Arrow matrix combinators
121+
122+ -- | Note that given the restrictions imposed it is not possible to
123+ -- implement the standard type classes present in standard Haskell.
124+ identity,
125+ comp,
126+ fromF,
127+ fromF',
128+
129+ -- * Matrix printing
130+ pretty,
131+ prettyPrint
132+ )
133+ where
134+
135+import Utils
136+import Data.Bool
137+import Data.Kind
138+import Data.List
139+import Data.Proxy
140+import Data.Void
141+import GHC.TypeLits
142+import Data.Type.Equality
143+import GHC.Generics
144+import Control.DeepSeq
145+import Control.Category
146+import Prelude hiding ((.))
147+
148+-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
149+data Matrix e cols rows where
150+ Empty :: Matrix e Void Void
151+ One :: e -> Matrix e () ()
152+ Junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
153+ Split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
154+
155+deriving instance (Show e) => Show (Matrix e cols rows)
156+
157+-- | Type family that computes the cardinality of a given type dimension.
158+--
159+-- It can also count the cardinality of custom types that implement the
160+-- 'Generic' instance.
161+type family Count (d :: Type) :: Nat where
162+ Count (Natural n m) = (m - n) + 1
163+ Count (Either a b) = (+) (Count a) (Count b)
164+ Count (a, b) = (*) (Count a) (Count b)
165+ Count (a -> b) = (^) (Count b) (Count a)
166+ -- Generics
167+ Count (M1 _ _ f p) = Count (f p)
168+ Count (K1 _ _ _) = 1
169+ Count (V1 _) = 0
170+ Count (U1 _) = 1
171+ Count ((:*:) a b p) = Count (a p) * Count (b p)
172+ Count ((:+:) a b p) = Count (a p) + Count (b p)
173+ Count d = Count (Rep d R)
174+
175+-- | Type family that computes of a given type dimension from a given natural
176+--
177+-- Thanks to Li-Yao Xia this type family is super fast.
178+type family FromNat (n :: Nat) :: Type where
179+ FromNat 0 = Void
180+ FromNat 1 = ()
181+ FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
182+
183+type family FromNat' (b :: Bool) (m :: Type) :: Type where
184+ FromNat' 'True m = Either m m
185+ FromNat' 'False m = Either () (Either m m)
186+
187+-- | Type family that normalizes the representation of a given data
188+-- structure
189+type family Normalize (d :: Type) :: Type where
190+ Normalize d = FromNat (Count d)
191+
192+-- | It isn't possible to implement the 'id' function so it's
193+-- implementation is 'undefined'. However 'comp' can be and this partial
194+-- class implementation exists just to make the code more readable.
195+--
196+-- Please use 'identity' instead.
197+instance (Num e) => Category (Matrix e) where
198+ id = undefined
199+ (.) = comp
200+
201+instance NFData e => NFData (Matrix e cols rows) where
202+ rnf Empty = ()
203+ rnf (One e) = rnf e
204+ rnf (Junc a b) = rnf a `seq` rnf b
205+ rnf (Split a b) = rnf a `seq` rnf b
206+
207+instance Eq e => Eq (Matrix e cols rows) where
208+ Empty == Empty = True
209+ (One a) == (One b) = a == b
210+ (Junc a b) == (Junc c d) = a == c && b == d
211+ (Split a b) == (Split c d) = a == c && b == d
212+ x@(Split a b) == y@(Junc c d) = x == abideJS y
213+ x@(Junc a b) == y@(Split c d) = abideJS x == y
214+
215+instance Num e => Num (Matrix e cols rows) where
216+
217+ Empty + Empty = Empty
218+ (One a) + (One b) = One (a + b)
219+ (Junc a b) + (Junc c d) = Junc (a + c) (b + d)
220+ (Split a b) + (Split c d) = Split (a + c) (b + d)
221+ x@(Split a b) + y@(Junc c d) = x + abideJS y
222+ x@(Junc a b) + y@(Split c d) = abideJS x + y
223+
224+ Empty - Empty = Empty
225+ (One a) - (One b) = One (a - b)
226+ (Junc a b) - (Junc c d) = Junc (a - c) (b - d)
227+ (Split a b) - (Split c d) = Split (a - c) (b - d)
228+ x@(Split a b) - y@(Junc c d) = x - abideJS y
229+ x@(Junc a b) - y@(Split c d) = abideJS x - y
230+
231+ Empty * Empty = Empty
232+ (One a) * (One b) = One (a * b)
233+ (Junc a b) * (Junc c d) = Junc (a * c) (b * d)
234+ (Split a b) * (Split c d) = Split (a * c) (b * d)
235+ x@(Split a b) * y@(Junc c d) = x * abideJS y
236+ x@(Junc a b) * y@(Split c d) = abideJS x * y
237+
238+ abs Empty = Empty
239+ abs (One a) = One (abs a)
240+ abs (Junc a b) = Junc (abs a) (abs b)
241+ abs (Split a b) = Split (abs a) (abs b)
242+
243+ signum Empty = Empty
244+ signum (One a) = One (signum a)
245+ signum (Junc a b) = Junc (signum a) (signum b)
246+ signum (Split a b) = Split (signum a) (signum b)
247+
248+-- Primitives
249+
250+-- | Empty matrix constructor
251+empty :: Matrix e Void Void
252+empty = Empty
253+
254+-- | Unit matrix constructor
255+one :: e -> Matrix e () ()
256+one = One
257+
258+-- | Matrix 'Junc' constructor
259+junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
260+junc = Junc
261+
262+infixl 3 |||
263+
264+-- | Matrix 'Junc' constructor
265+(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
266+(|||) = Junc
267+
268+-- | Matrix 'Split' constructor
269+split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
270+split = Split
271+
272+infixl 2 ===
273+
274+-- | Matrix 'Split' constructor
275+(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
276+(===) = Split
277+
278+-- Construction
279+
280+-- | Type class for defining the 'fromList' conversion function.
281+--
282+-- Given that it is not possible to branch on types at the term level type
283+-- classes are needed bery much like an inductive definition but on types.
284+class FromLists e cols rows where
285+ -- | Build a matrix out of a list of list of elements. Throws a runtime
286+ -- error if the dimensions do not match.
287+ fromLists :: [[e]] -> Matrix e cols rows
288+
289+instance FromLists e Void Void where
290+ fromLists [] = Empty
291+ fromLists _ = error "Wrong dimensions"
292+
293+instance {-# OVERLAPPING #-} FromLists e () () where
294+ fromLists [[e]] = One e
295+ fromLists _ = error "Wrong dimensions"
296+
297+instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
298+ fromLists [h : t] = Junc (One h) (fromLists [t])
299+ fromLists _ = error "Wrong dimensions"
300+
301+instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), KnownNat (Count a)) => FromLists e (Either a b) () where
302+ fromLists [l] =
303+ let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
304+ in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])
305+ fromLists _ = error "Wrong dimensions"
306+
307+instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
308+ fromLists ([h] : t) = Split (One h) (fromLists t)
309+ fromLists _ = error "Wrong dimensions"
310+
311+instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, KnownNat (Count a)) => FromLists e () (Either a b) where
312+ fromLists l@([h] : t) =
313+ let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
314+ in Split (fromLists (take rowsA l)) (fromLists (drop rowsA l))
315+ fromLists _ = error "Wrong dimensions"
316+
317+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
318+ fromLists l@(h : t) =
319+ let lh = length h
320+ rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
321+ condition = all (== lh) (map length t)
322+ in if lh > 0 && condition
323+ then Split (fromLists (take rowsC l)) (fromLists (drop rowsC l))
324+ else error "Not all rows have the same length"
325+
326+-- | Matrix builder function. Constructs a matrix provided with
327+-- a construction function.
328+matrixBuilder ::
329+ forall e cols rows.
330+ ( FromLists e cols rows,
331+ KnownNat (Count cols),
332+ KnownNat (Count rows)
333+ ) =>
334+ ((Int, Int) -> e) ->
335+ Matrix e cols rows
336+matrixBuilder f =
337+ let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
338+ r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
339+ positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
340+ in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
341+
342+-- | Constructs a column vector matrix
343+col :: (FromLists e () rows) => [e] -> Matrix e () rows
344+col = fromLists . map (: [])
345+
346+-- | Constructs a row vector matrix
347+row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
348+row = fromLists . (: [])
349+
350+-- | Lifts functions to matrices with arbitrary dimensions.
351+--
352+-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
353+-- types @a@ or @b@ allows.
354+fromF ::
355+ forall a b cols rows e.
356+ ( Bounded a,
357+ Bounded b,
358+ Enum a,
359+ Enum b,
360+ Eq b,
361+ Num e,
362+ Ord e,
363+ KnownNat (Count cols),
364+ KnownNat (Count rows),
365+ FromLists e rows cols
366+ ) =>
367+ (a -> b) ->
368+ Matrix e cols rows
369+fromF f =
370+ let minA = minBound @a
371+ maxA = maxBound @a
372+ minB = minBound @b
373+ maxB = maxBound @b
374+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
375+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
376+ elementsA = take ccols [minA .. maxA]
377+ elementsB = take rrows [minB .. maxB]
378+ combinations = (,) <$> elementsA <*> elementsB
379+ combAp = map snd . sort . map (\(a, b) -> if f a == b
380+ then ((fromEnum a, fromEnum b), 1)
381+ else ((fromEnum a, fromEnum b), 0)) $ combinations
382+ mList = buildList combAp rrows
383+ in tr $ fromLists mList
384+ where
385+ buildList [] _ = []
386+ buildList l r = take r l : buildList (drop r l) r
387+
388+-- | Lifts functions to matrices with dimensions matching @a@ and @b@
389+-- cardinality's.
390+fromF' ::
391+ forall a b e.
392+ ( Bounded a,
393+ Bounded b,
394+ Enum a,
395+ Enum b,
396+ Eq b,
397+ Num e,
398+ Ord e,
399+ KnownNat (Count (Normalize a)),
400+ KnownNat (Count (Normalize b)),
401+ FromLists e (Normalize b) (Normalize a)
402+ ) =>
403+ (a -> b) ->
404+ Matrix e (Normalize a) (Normalize b)
405+fromF' f =
406+ let minA = minBound @a
407+ maxA = maxBound @a
408+ minB = minBound @b
409+ maxB = maxBound @b
410+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
411+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
412+ elementsA = take ccols [minA .. maxA]
413+ elementsB = take rrows [minB .. maxB]
414+ combinations = (,) <$> elementsA <*> elementsB
415+ combAp = map snd . sort . map (\(a, b) -> if f a == b
416+ then ((fromEnum a, fromEnum b), 1)
417+ else ((fromEnum a, fromEnum b), 0)) $ combinations
418+ mList = buildList combAp rrows
419+ in tr $ fromLists mList
420+ where
421+ buildList [] _ = []
422+ buildList l r = take r l : buildList (drop r l) r
423+
424+-- Conversion
425+
426+-- | Converts a matrix to a list of lists of elements.
427+toLists :: Matrix e cols rows -> [[e]]
428+toLists Empty = []
429+toLists (One e) = [[e]]
430+toLists (Split l r) = toLists l ++ toLists r
431+toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
432+
433+-- | Converts a matrix to a list of elements.
434+toList :: Matrix e cols rows -> [e]
435+toList = concat . toLists
436+
437+-- Zeros Matrix
438+
439+-- | The zero matrix. A matrix wholly filled with zeros.
440+zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
441+zeros = matrixBuilder (const 0)
442+
443+-- Ones Matrix
444+
445+-- | The ones matrix. A matrix wholly filled with ones.
446+--
447+-- Also known as T (Top) matrix.
448+ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
449+ones = matrixBuilder (const 1)
450+
451+-- Const Matrix
452+
453+-- | The constant matrix constructor. A matrix wholly filled with a given
454+-- value.
455+constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows
456+constant e = matrixBuilder (const e)
457+
458+-- Bang Matrix
459+
460+-- | The T (Top) row vector matrix.
461+bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()
462+bang =
463+ let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
464+ in fromLists [take c [1, 1 ..]]
465+
466+-- Identity Matrix
467+
468+-- | Identity matrix.
469+identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols
470+identity = matrixBuilder (bool 0 1 . uncurry (==))
471+
472+-- Matrix composition (MMM)
473+
474+-- | Matrix composition. Equivalent to matrix-matrix multiplication.
475+--
476+-- This definition takes advantage of divide-and-conquer and fusion laws
477+-- from LAoP.
478+comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
479+comp Empty Empty = Empty
480+comp (One a) (One b) = One (a * b)
481+comp (Junc a b) (Split c d) = comp a c + comp b d -- Divide-and-conquer law
482+comp (Split a b) c = Split (comp a c) (comp b c) -- Split fusion law
483+comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc fusion law
484+
485+-- Projections
486+
487+-- | Biproduct first component projection
488+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
489+p1 =
490+ let iden = identity :: Matrix e m m
491+ zero = zeros :: Matrix e n m
492+ in junc iden zero
493+
494+-- | Biproduct second component projection
495+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
496+p2 =
497+ let iden = identity :: Matrix e n n
498+ zero = zeros :: Matrix e m n
499+ in junc zero iden
500+
501+-- Injections
502+
503+-- | Biproduct first component injection
504+i1 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
505+i1 = tr p1
506+
507+-- | Biproduct second component injection
508+i2 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
509+i2 = tr p2
510+
511+-- Dimensions
512+
513+-- | Obtain the number of rows.
514+--
515+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
516+-- dimensions in constant time.
517+--
518+-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
519+-- exchange for performance.
520+rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int
521+rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
522+
523+-- | Obtain the number of columns.
524+--
525+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
526+-- dimensions in constant time.
527+--
528+-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
529+-- exchange for performance.
530+columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int
531+columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
532+
533+-- Coproduct Bifunctor
534+
535+infixl 5 -|-
536+
537+-- | Matrix coproduct functor also known as matrix direct sum.
538+(-|-) ::
539+ forall e n k m j.
540+ ( Num e,
541+ KnownNat (Count j),
542+ KnownNat (Count k),
543+ FromLists e k k,
544+ FromLists e j k,
545+ FromLists e k j,
546+ FromLists e j j
547+ ) =>
548+ Matrix e n k ->
549+ Matrix e m j ->
550+ Matrix e (Either n m) (Either k j)
551+(-|-) a b = Junc (i1 . a) (i2 . b)
552+
553+-- Khatri Rao Product and projections
554+
555+-- | Khatri Rao product first component projection matrix.
556+kp1 ::
557+ forall e m k .
558+ ( Num e,
559+ KnownNat (Count k),
560+ FromLists e (FromNat (Count m * Count k)) m,
561+ KnownNat (Count m),
562+ KnownNat (Count (Normalize (m, k)))
563+ ) => Matrix e (Normalize (m, k)) m
564+kp1 = matrixBuilder f
565+ where
566+ offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
567+ f (x, y)
568+ | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
569+ | otherwise = 0
570+
571+-- | Khatri Rao product second component projection matrix.
572+kp2 ::
573+ forall e m k .
574+ ( Num e,
575+ KnownNat (Count k),
576+ FromLists e (FromNat (Count m * Count k)) k,
577+ KnownNat (Count m),
578+ KnownNat (Count (Normalize (m, k)))
579+ ) => Matrix e (Normalize (m, k)) k
580+kp2 = matrixBuilder f
581+ where
582+ offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
583+ f (x, y)
584+ | x == y || mod (y - x) offset == 0 = 1
585+ | otherwise = 0
586+
587+-- | Khatri Rao Matrix product also known as matrix pairing.
588+--
589+-- NOTE: That this is not a true categorical product, see for instance:
590+--
591+-- @
592+-- | kp1 . khatri a b == a
593+-- khatri a b ==> |
594+-- | kp2 . khatri a b == b
595+-- @
596+--
597+-- __Emphasis__ on the implication symbol.
598+khatri ::
599+ forall e cols a b.
600+ ( Num e,
601+ KnownNat (Count a),
602+ KnownNat (Count b),
603+ KnownNat (Count (Normalize (a, b))),
604+ FromLists e (Normalize (a, b)) a,
605+ FromLists e (Normalize (a, b)) b
606+ ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
607+khatri a b =
608+ let kp1' = kp1 @e @a @b
609+ kp2' = kp2 @e @a @b
610+ in (tr kp1') . a * (tr kp2') . b
611+
612+-- Product Bifunctor (Kronecker)
613+
614+infixl 4 ><
615+
616+-- | Matrix product functor also known as kronecker product
617+(><) ::
618+ forall e m p n q.
619+ ( Num e,
620+ KnownNat (Count m),
621+ KnownNat (Count n),
622+ KnownNat (Count p),
623+ KnownNat (Count q),
624+ KnownNat (Count (Normalize (m, n))),
625+ FromLists e (Normalize (m, n)) m,
626+ FromLists e (Normalize (m, n)) n,
627+ KnownNat (Count (Normalize (p, q))),
628+ FromLists e (Normalize (p, q)) p,
629+ FromLists e (Normalize (p, q)) q
630+ )
631+ => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
632+(><) a b =
633+ let kp1' = kp1 @e @m @n
634+ kp2' = kp2 @e @m @n
635+ in khatri (a . kp1') (b . kp2')
636+
637+-- Matrix abide Junc Split
638+
639+-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
640+--
641+-- Law:
642+--
643+-- @
644+-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
645+-- @
646+abideJS :: Matrix e cols rows -> Matrix e cols rows
647+abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law
648+abideJS Empty = Empty
649+abideJS (One e) = One e
650+abideJS (Junc a b) = Junc (abideJS a) (abideJS b)
651+abideJS (Split a b) = Split (abideJS a) (abideJS b)
652+
653+-- Matrix abide Split Junc
654+
655+-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
656+--
657+-- @
658+-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
659+-- @
660+abideSJ :: Matrix e cols rows -> Matrix e cols rows
661+abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law
662+abideSJ Empty = Empty
663+abideSJ (One e) = One e
664+abideSJ (Junc a b) = Junc (abideSJ a) (abideSJ b)
665+abideSJ (Split a b) = Split (abideSJ a) (abideSJ b)
666+
667+-- Matrix transposition
668+
669+-- | Matrix transposition.
670+tr :: Matrix e cols rows -> Matrix e rows cols
671+tr Empty = Empty
672+tr (One e) = One e
673+tr (Junc a b) = Split (tr a) (tr b)
674+tr (Split a b) = Junc (tr a) (tr b)
675+
676+-- Selective 'select' operator
677+
678+-- | Selective functors 'select' operator equivalent inspired by the
679+-- ArrowMonad solution presented in the paper.
680+select ::
681+ ( Bounded a,
682+ Bounded b,
683+ Enum a,
684+ Enum b,
685+ Num e,
686+ Ord e,
687+ Eq b,
688+ KnownNat (Count (Normalize a)),
689+ KnownNat (Count (Normalize b)),
690+ KnownNat (Count cols),
691+ FromLists e (Normalize b) (Normalize a),
692+ FromLists e (Normalize b) (Normalize b)
693+ ) => Matrix e cols (Either (Normalize a) (Normalize b)) -> (a -> b) -> Matrix e cols (Normalize b)
694+select m y =
695+ let f = fromF y
696+ in junc f identity . m
697+
698+-- McCarthy's Conditional
699+
700+-- | McCarthy's Conditional expresses probabilistic choice.
701+cond ::
702+ ( cols ~ FromNat (Count cols),
703+ KnownNat (Count cols),
704+ FromLists e () cols,
705+ FromLists e cols (),
706+ FromLists e cols cols,
707+ Bounded a,
708+ Enum a,
709+ Num e,
710+ Ord e
711+ )
712+ =>
713+ (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
714+cond p f g = junc f g . grd p
715+
716+grd ::
717+ ( q ~ FromNat (Count q),
718+ KnownNat (Count q),
719+ FromLists e () q,
720+ FromLists e q (),
721+ FromLists e q q,
722+ Bounded a,
723+ Enum a,
724+ Num e,
725+ Ord e
726+ )
727+ =>
728+ (a -> Bool) -> Matrix e q (Either q q)
729+grd f = split (corr f) (corr (not . f))
730+
731+corr ::
732+ forall e a q .
733+ ( q ~ FromNat (Count q),
734+ KnownNat (Count q),
735+ FromLists e () q,
736+ FromLists e q (),
737+ FromLists e q q,
738+ Bounded a,
739+ Enum a,
740+ Num e,
741+ Ord e
742+ )
743+ => (a -> Bool) -> Matrix e q q
744+corr p = let f = fromF p :: Matrix e q ()
745+ in khatri f (identity :: Matrix e q q)
746+
747+-- Pretty print
748+
749+prettyAux :: Show e => [[e]] -> [[e]] -> String
750+prettyAux [] _ = ""
751+prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
752+ where
753+ v = fmap show m
754+ widest = maximum $ fmap length v
755+ fill str = replicate (widest - length str - 2) ' ' ++ str
756+prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
757+ where
758+ v = fmap show m
759+ widest = maximum $ fmap length v
760+ fill str = replicate (widest - length str - 2) ' ' ++ str
761+prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
762+ prettyAux t l
763+ where
764+ v = fmap show l
765+ widest = maximum $ fmap length v
766+ fill str = replicate (widest - length str - 2) ' ' ++ str
767+
768+-- | Matrix pretty printer
769+pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String
770+pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
771+ prettyAux (toLists m) (toLists m) ++
772+ "└ " ++ unwords (replicate (columns m) blank) ++ " ┘"
773+ where
774+ v = fmap show (toList m)
775+ widest = maximum $ fmap length v
776+ fill str = replicate (widest - length str) ' ' ++ str
777+ blank = fill ""
778+
779+-- | Matrix pretty printer
780+prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()
781+prettyPrint = putStrLn . pretty
src/Matrix/Nat.hs+24−9
@@ -141,11 +141,21 @@ where
141import Data.Proxy
141import Data.Proxy
142import GHC.TypeLits
142import GHC.TypeLits
143import Control.DeepSeq
143import Control.DeepSeq
144−import qualified Matrix.Type as I
144+import qualified Control.Category as C
145+import qualified Matrix.Internal as I
145
146
146newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
147newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
147 deriving (Show, Num, Eq, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
148 deriving (Show, Num, Eq, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
148
149
150+-- | It isn't possible to implement the 'id' function so it's
151+-- implementation is 'undefined'. However 'comp' can be and this partial
152+-- class implementation exists just to make the code more readable.
153+--
154+-- Please use 'identity' instead.
155+instance (Num e) => C.Category (Matrix e) where
156+ id = undefined
157+ (.) = comp
158+
149-- Primitives
159-- Primitives
150
160
151empty :: Matrix e 0 0
161empty :: Matrix e 0 0
@@ -437,14 +447,19 @@ tr :: Matrix e cols rows -> Matrix e rows cols
437tr (M m) = M (I.tr m)
447tr (M m) = M (I.tr m)
438
448
439-- Selective 'select' operator
449-- Selective 'select' operator
440−
450+--
441−select :: ( Bounded a1, Bounded b, Enum a1, Enum b, Num e, Ord e,
451+select :: (Bounded a, Bounded b, Enum a, Enum b, Num e, Ord e,
452+ KnownNat (I.Count (I.FromNat (I.Count a))),
453+ KnownNat (I.Count (I.FromNat (I.Count b))),
442− KnownNat (I.Count a2), KnownNat (I.Count (I.FromNat rows1)),
454+ KnownNat (I.Count (I.FromNat cols1)),
443− I.FromLists e (I.FromNat rows1) a2,
455+ I.FromLists e (I.FromNat (I.Count b)) (I.FromNat (I.Count a)),
444− I.FromLists e (I.FromNat rows1) (I.FromNat rows1), Eq b,
456+ I.FromLists e (I.FromNat (I.Count b)) (I.FromNat (I.Count b)),
457+ Eq b,
445− I.FromNat cols1 ~ I.FromNat cols2,
458+ I.FromNat rows1
446− I.FromNat rows2 ~ Either a2 (I.FromNat rows1)) =>
459+ ~ Either (I.FromNat (I.Count a)) (I.FromNat (I.Count b)),
460+ I.FromNat cols2 ~ I.FromNat cols1,
461+ I.FromNat (I.Count b) ~ I.FromNat rows2) =>
447− Matrix e cols1 rows2 -> (a1 -> b) -> Matrix e cols2 rows1
462+ Matrix e cols1 rows1 -> (a -> b) -> Matrix e cols2 rows2
448select (M m) y = M (I.select m y)
463select (M m) y = M (I.select m y)
449
464
450-- McCarthy's Conditional
465-- McCarthy's Conditional
src/Matrix/Type.hs+267−421
@@ -1,15 +1,15 @@
1{-# LANGUAGE AllowAmbiguousTypes #-}
1{-# LANGUAGE AllowAmbiguousTypes #-}
2{-# LANGUAGE DataKinds #-}
2{-# LANGUAGE DataKinds #-}
3+{-# LANGUAGE DerivingVia #-}
3{-# LANGUAGE FlexibleContexts #-}
4{-# LANGUAGE FlexibleContexts #-}
4{-# LANGUAGE FlexibleInstances #-}
5{-# LANGUAGE FlexibleInstances #-}
5{-# LANGUAGE GADTs #-}
6{-# LANGUAGE GADTs #-}
6−{-# LANGUAGE InstanceSigs #-}
7+{-# LANGUAGE KindSignatures #-}
7{-# LANGUAGE MultiParamTypeClasses #-}
8{-# LANGUAGE MultiParamTypeClasses #-}
8{-# LANGUAGE NoStarIsType #-}
9{-# LANGUAGE NoStarIsType #-}
10+{-# LANGUAGE RankNTypes #-}
9{-# LANGUAGE ScopedTypeVariables #-}
11{-# LANGUAGE ScopedTypeVariables #-}
10−{-# LANGUAGE StandaloneDeriving #-}
11{-# LANGUAGE TypeApplications #-}
12{-# LANGUAGE TypeApplications #-}
12−{-# LANGUAGE TypeFamilies #-}
13{-# LANGUAGE TypeOperators #-}
13{-# LANGUAGE TypeOperators #-}
14{-# LANGUAGE UndecidableInstances #-}
14{-# LANGUAGE UndecidableInstances #-}
15
15
@@ -27,24 +27,38 @@
27-- in Haskell. See <https://github.com/bolt12/master-thesis my Msc Thesis> for the
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.
28-- motivation behind the library, the underlying theory, and implementation details.
29--
29--
30−-- This module offers many of the combinators mentioned in the work of
30+-- This module offers a newtype wrapper around 'Matrix.Type.Matrix' that
31−-- Macedo (2012) and Oliveira (2012).
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.
32--
36--
33-----------------------------------------------------------------------------
37-----------------------------------------------------------------------------
34
38
35module Matrix.Type
39module Matrix.Type
36− ( -- | This definition makes use of the fact that 'Void' is
40+ ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
37− -- isomorphic to 0 and '()' to 1 and captures matrix
41+ --
38− -- dimensions as stacks of 'Either's.
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.
39 --
53 --
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.
44
54
45 -- * Type safe matrix representation
55 -- * Type safe matrix representation
46 Matrix (..),
56 Matrix (..),
47
57
58+ -- * Type aliases
59+ Zero,
60+ One,
61+
48 -- * Primitives
62 -- * Primitives
49 empty,
63 empty,
50 one,
64 one,
@@ -52,12 +66,12 @@ module Matrix.Type
52 split,
66 split,
53
67
54 -- * Auxiliary type families
68 -- * Auxiliary type families
55− FromNat,
69+ I.FromNat,
56− Count,
70+ I.Count,
57− Normalize,
71+ I.Normalize,
58
72
59 -- * Matrix construction and conversion
73 -- * Matrix construction and conversion
60− FromLists,
74+ I.FromLists,
61 fromLists,
75 fromLists,
62 toLists,
76 toLists,
63 toList,
77 toList,
@@ -128,214 +142,106 @@ module Matrix.Type
128 pretty,
142 pretty,
129 prettyPrint
143 prettyPrint
130 )
144 )
131− where
145+where
132
146
133−import Utils
134−import Data.Bool
135−import Data.Kind
136−import Data.List
137−import Data.Proxy
138import Data.Void
147import Data.Void
148+import Data.Proxy
149+import Data.Kind
139−import GHC.TypeLits
150+import GHC.TypeLits
140−import Data.Type.Equality
141−import GHC.Generics
142import Control.DeepSeq
151import Control.DeepSeq
152+import qualified Control.Category as C
153+import qualified Matrix.Internal as I
143
154
144−-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
155+newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
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)
156+ deriving (Show, Num, Eq, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
152−
157+
153−-- | Type family that computes the cardinality of a given type dimension.
158+-- | It isn't possible to implement the 'id' function so it's
154−-- It can also count the cardinality of custom types that implement the
159+-- implementation is 'undefined'. However 'comp' can be and this partial
155−-- 'Generic' instance.
160+-- class implementation exists just to make the code more readable.
156−type family Count (d :: Type) where
161+--
157− Count (Natural n m) = (m - n) + 1
162+-- Please use 'identity' instead.
158− Count (Either a b) = (+) (Count a) (Count b)
163+instance (Num e) => C.Category (Matrix e) where
159− Count (a, b) = (*) (Count a) (Count b)
164+ id = undefined
160− Count (a -> b) = (^) (Count b) (Count a)
165+ (.) = comp
161− -- Generics
166+
162− Count (M1 _ _ f p) = Count (f p)
167+-- | Zero type alias
163− Count (K1 _ _ _) = 1
168+type Zero = Void
164− Count (V1 _) = 0
169+
165− Count (U1 _) = 1
170+-- | One type alias
166− Count ((:*:) a b p) = Count (a p) * Count (b p)
171+type One = ()
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)
232
172
233-- Primitives
173-- Primitives
234
174
235-- | Empty matrix constructor
175-- | Empty matrix constructor
236−empty :: Matrix e Void Void
176+empty :: Matrix e Zero Zero
237−empty = Empty
177+empty = M I.Empty
238
178
239-- | Unit matrix constructor
179-- | Unit matrix constructor
240−one :: e -> Matrix e () ()
180+one :: e -> Matrix e One One
241−one = One
181+one = M . I.One
242
182
243-- | Matrix 'Junc' constructor
183-- | Matrix 'Junc' constructor
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 ->
244−junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
188+ Matrix e (Either a b) rows
245−junc = Junc
189+junc (M a) (M b) = M (I.Junc a b)
246
190
247infixl 3 |||
191infixl 3 |||
248−
249-- | Matrix 'Junc' constructor
192-- | Matrix 'Junc' constructor
193+(|||) ::
194+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
195+ Matrix e a rows ->
196+ Matrix e b rows ->
250−(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
197+ Matrix e (Either a b) rows
251−(|||) = Junc
198+(|||) = junc
252
199
253-- | Matrix 'Split' constructor
200-- | Matrix 'Split' constructor
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 ->
254−split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
205+ Matrix e cols (Either a b)
255−split = Split
206+split (M a) (M b) = M (I.Split a b)
256
207
257infixl 2 ===
208infixl 2 ===
258−
259-- | Matrix 'Split' constructor
209-- | Matrix 'Split' constructor
210+(===) ::
211+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
212+ Matrix e cols a ->
213+ Matrix e cols b ->
260−(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
214+ Matrix e cols (Either a b)
261−(===) = Split
215+(===) = split
262
216
263-- Construction
217-- Construction
264
218
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
219+-- | Build a matrix out of a list of list of elements. Throws a runtime
270− -- error if the dimensions do not match.
220+-- error if the dimensions do not match.
271− fromLists :: [[e]] -> Matrix e cols rows
221+fromLists :: (I.FromLists e (I.Normalize cols) (I.Normalize rows)) => [[e]] -> Matrix e cols rows
272−
273−instance FromLists e Void Void where
274− fromLists [] = Empty
222+fromLists = M . I.fromLists
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"
309
223
310-- | Matrix builder function. Constructs a matrix provided with
224-- | Matrix builder function. Constructs a matrix provided with
311-- a construction function.
225-- a construction function.
312matrixBuilder ::
226matrixBuilder ::
313− forall e cols rows.
227+ (I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
314− ( FromLists e cols rows,
315− KnownNat (Count cols),
316− KnownNat (Count rows)
317− ) =>
318 ((Int, Int) -> e) ->
228 ((Int, Int) -> e) ->
319 Matrix e cols rows
229 Matrix e cols rows
320−matrixBuilder f =
230+matrixBuilder = M . I.matrixBuilder
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
325
231
326-- | Constructs a column vector matrix
232-- | Constructs a column vector matrix
327−col :: (FromLists e () rows) => [e] -> Matrix e () rows
233+col :: (I.FromLists e () (I.Normalize rows)) => [e] -> Matrix e One rows
328−col = fromLists . map (: [])
234+col = M . I.col
329
235
330-- | Constructs a row vector matrix
236-- | Constructs a row vector matrix
331−row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
237+row :: (I.FromLists e (I.Normalize cols) ()) => [e] -> Matrix e cols One
332−row = fromLists . (: [])
238+row = M . I.row
333
239
334-- | Lifts functions to matrices with arbitrary dimensions.
240-- | Lifts functions to matrices with arbitrary dimensions.
241+--
335−-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
242+-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
336-- types @a@ or @b@ allows.
243-- types @a@ or @b@ allows.
337fromF ::
244fromF ::
338− forall a b cols rows e.
339 ( Bounded a,
245 ( Bounded a,
340 Bounded b,
246 Bounded b,
341 Enum a,
247 Enum a,
@@ -343,35 +249,17 @@ fromF ::
343 Eq b,
249 Eq b,
344 Num e,
250 Num e,
345 Ord e,
251 Ord e,
346− KnownNat (Count cols),
252+ KnownNat (I.Count (I.Normalize cols)),
347− KnownNat (Count rows),
253+ KnownNat (I.Count (I.Normalize rows)),
348− FromLists e rows cols
254+ I.FromLists e (I.Normalize rows) (I.Normalize cols)
349 ) =>
255 ) =>
350 (a -> b) ->
256 (a -> b) ->
351 Matrix e cols rows
257 Matrix e cols rows
352−fromF f =
258+fromF = M . I.fromF
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
370
259
371-- | Lifts functions to matrices with dimensions matching @a@ and @b@
260-- | Lifts functions to matrices with dimensions matching @a@ and @b@
372-- cardinality's.
261-- cardinality's.
373fromF' ::
262fromF' ::
374− forall a b e.
375 ( Bounded a,
263 ( Bounded a,
376 Bounded b,
264 Bounded b,
377 Enum a,
265 Enum a,
@@ -379,133 +267,149 @@ fromF' ::
379 Eq b,
267 Eq b,
380 Num e,
268 Num e,
381 Ord e,
269 Ord e,
382− KnownNat (Count (Normalize a)),
270+ KnownNat (I.Count (I.Normalize a)),
383− KnownNat (Count (Normalize b)),
271+ KnownNat (I.Count (I.Normalize b)),
384− FromLists e (Normalize b) (Normalize a)
272+ I.FromLists e (I.Normalize b) (I.Normalize a)
385 ) =>
273 ) =>
386 (a -> b) ->
274 (a -> b) ->
387− Matrix e (Normalize a) (Normalize b)
275+ Matrix e a b
388−fromF' f =
276+fromF' = M . I.fromF'
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
406
277
407-- Conversion
278-- Conversion
408
279
409-- | Converts a matrix to a list of lists of elements.
280-- | Converts a matrix to a list of lists of elements.
410toLists :: Matrix e cols rows -> [[e]]
281toLists :: Matrix e cols rows -> [[e]]
411−toLists Empty = []
282+toLists (M m) = I.toLists m
412−toLists (One e) = [[e]]
413−toLists (Split l r) = toLists l ++ toLists r
414−toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
415
283
416-- | Converts a matrix to a list of elements.
284-- | Converts a matrix to a list of elements.
417toList :: Matrix e cols rows -> [e]
285toList :: Matrix e cols rows -> [e]
418−toList = concat . toLists
286+toList (M m) = I.toList m
419
287
420-- Zeros Matrix
288-- Zeros Matrix
421
289
422-- | The zero matrix. A matrix wholly filled with zeros.
290-- | The zero matrix. A matrix wholly filled with zeros.
291+zeros ::
423−zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
292+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
424−zeros = matrixBuilder (const 0)
293+ Matrix e cols rows
294+zeros = M I.zeros
425
295
426-- Ones Matrix
296-- Ones Matrix
427
297
428-- | The ones matrix. A matrix wholly filled with ones.
298-- | The ones matrix. A matrix wholly filled with ones.
299+--
429−-- Also known as T (Top) matrix.
300+-- Also known as T (Top) matrix.
301+ones ::
430−ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
302+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
431−ones = matrixBuilder (const 1)
303+ Matrix e cols rows
304+ones = M I.ones
432
305
433-- Const Matrix
306-- Const Matrix
434
307
435-- | The constant matrix constructor. A matrix wholly filled with a given
308-- | The constant matrix constructor. A matrix wholly filled with a given
436-- value.
309-- value.
310+constant ::
437−constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows
311+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
438−constant e = matrixBuilder (const e)
312+ e ->
313+ Matrix e cols rows
314+constant = M . I.constant
439
315
440-- Bang Matrix
316-- Bang Matrix
441
317
442-- | The T (Top) row vector matrix.
318-- | The T (Top) row vector matrix.
319+bang ::
320+ forall e cols.
443−bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()
321+ (Num e, Enum e, I.FromLists e (I.Normalize cols) (), KnownNat (I.Count (I.Normalize cols))) =>
322+ Matrix e cols One
444−bang =
323+bang = M I.bang
445− let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
446− in fromLists [take c [1, 1 ..]]
447
324
448-- Identity Matrix
325-- Identity Matrix
449
326
450−-- | Identity matrix.
327+-- | Identity matrix
328+identity ::
451−identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols
329+ (Num e, I.FromLists e (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
452−identity = matrixBuilder (bool 0 1 . uncurry (==))
330+ Matrix e a a
331+identity = M I.identity
453
332
454-- Matrix composition (MMM)
333-- Matrix composition (MMM)
455
334
456-- | Matrix composition. Equivalent to matrix-matrix multiplication.
335-- | Matrix composition. Equivalent to matrix-matrix multiplication.
336+--
457−-- This definition takes advantage of divide-and-conquer and fusion laws
337+-- This definition takes advantage of divide-and-conquer and fusion laws
458-- from LAoP.
338-- from LAoP.
459comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
339comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
460−comp Empty Empty = Empty
340+comp (M a) (M b) = M (I.comp a b)
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
467
341
468-- | Biproduct first component projection
342-- | 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
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
470−p1 =
352+p1 = M I.p1
471− let iden = identity :: Matrix e m m
472− zero = zeros :: Matrix e n m
473− in junc iden zero
474
353
475-- | Biproduct second component projection
354-- | 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
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
477−p2 =
364+p2 = M I.p2
478− let iden = identity :: Matrix e n n
479− zero = zeros :: Matrix e m n
480− in junc zero iden
481
365
482-- Injections
366-- Injections
483
367
484-- | Biproduct first component injection
368-- | 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)
486i1 = tr p1
378i1 = tr p1
487
379
488-- | Biproduct second component injection
380-- | 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)
490i2 = tr p2
390i2 = tr p2
491
391
492-- Dimensions
392-- Dimensions
493
393
494-- | Obtain the number of rows.
394-- | Obtain the number of rows.
395+--
495−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
396+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
496-- dimensions in constant time.
397-- dimensions in constant time.
398+--
497-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
399-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
498-- exchange for performance.
400-- exchange for performance.
499−rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int
401+rows :: (KnownNat (I.Count (I.Normalize rows))) => Matrix e cols rows -> Int
500−rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
402+rows (M m) = I.rows m
501
403
502-- | Obtain the number of columns.
404-- | Obtain the number of columns.
405+--
503−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
406+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
504-- dimensions in constant time.
407-- dimensions in constant time.
408+--
505-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
409-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
506-- exchange for performance.
410-- exchange for performance.
507−columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int
411+columns :: (KnownNat (I.Count (I.Normalize cols))) => Matrix e cols rows -> Int
508−columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
412+columns (M m) = I.columns m
509
413
510-- Coproduct Bifunctor
414-- Coproduct Bifunctor
511
415
@@ -513,19 +417,20 @@ infixl 5 -|-
513
417
514-- | Matrix coproduct functor also known as matrix direct sum.
418-- | Matrix coproduct functor also known as matrix direct sum.
515(-|-) ::
419(-|-) ::
516− forall e n k m j.
517 ( Num e,
420 ( Num e,
518− KnownNat (Count j),
421+ KnownNat (I.Count (I.Normalize j)),
519− KnownNat (Count k),
422+ KnownNat (I.Count (I.Normalize k)),
520− FromLists e k k,
423+ I.FromLists e (I.Normalize k) (I.Normalize k),
521− FromLists e j k,
424+ I.FromLists e (I.Normalize j) (I.Normalize k),
522− FromLists e k j,
425+ I.FromLists e (I.Normalize k) (I.Normalize j),
523− FromLists e j 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)
524 ) =>
429 ) =>
525 Matrix e n k ->
430 Matrix e n k ->
526 Matrix e m j ->
431 Matrix e m j ->
527 Matrix e (Either n m) (Either k j)
432 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)
529
434
530-- Khatri Rao Product and projections
435-- Khatri Rao Product and projections
531
436
@@ -533,36 +438,29 @@ infixl 5 -|-
533kp1 ::
438kp1 ::
534 forall e m k .
439 forall e m k .
535 ( Num e,
440 ( Num e,
536− KnownNat (Count k),
441+ KnownNat (I.Count (I.Normalize m)),
442+ KnownNat (I.Count (I.Normalize k)),
443+ KnownNat (I.Count (I.Normalize (m, k))),
537− FromLists e (FromNat (Count m * Count k)) m,
444+ I.FromLists e (I.Normalize (m, k)) (I.Normalize m),
538− KnownNat (Count m),
445+ I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
539− KnownNat (Count (Normalize (m, k)))
540− ) => Matrix e (Normalize (m, k)) m
446+ ) => Matrix e (m, k) m
541−kp1 = matrixBuilder f
447+kp1 = M (I.kp1 @e @(I.Normalize m) @(I.Normalize k))
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
547
448
548-- | Khatri Rao product second component projection matrix.
449-- | Khatri Rao product second component projection matrix.
549kp2 ::
450kp2 ::
550− forall e m k .
451+ forall e m k.
551 ( Num e,
452 ( Num e,
552− KnownNat (Count k),
453+ KnownNat (I.Count (I.Normalize k)),
454+ KnownNat (I.Count (I.Normalize m)),
455+ KnownNat (I.Count (I.Normalize (m, k))),
553− FromLists e (FromNat (Count m * Count k)) k,
456+ I.FromLists e (I.Normalize (m, k)) (I.Normalize k),
554− KnownNat (Count m),
457+ I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
555− KnownNat (Count (Normalize (m, k)))
556− ) => Matrix e (Normalize (m, k)) k
458+ ) => Matrix e (m, k) k
557−kp2 = matrixBuilder f
459+kp2 = M (I.kp2 @e @(I.Normalize m) @(I.Normalize k))
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
563
460
564-- | Khatri Rao Matrix product also known as matrix pairing.
461-- | Khatri Rao Matrix product also known as matrix pairing.
462+--
565−-- NOTE: That this is not a true categorical product, see for instance:
463+-- NOTE: That this is not a true categorical product, see for instance:
566--
464--
567-- @
465-- @
568-- | kp1 `comp` khatri a b == a
466-- | kp1 `comp` khatri a b == a
@@ -571,15 +469,16 @@ kp2 = matrixBuilder f
571-- @
469-- @
572--
470--
573-- __Emphasis__ on the implication symbol.
471-- __Emphasis__ on the implication symbol.
574−khatri ::
472+khatri ::
575− forall e cols a b.
473+ forall e cols a b.
576− ( Num e,
474+ ( Num e,
577− KnownNat (Count a),
475+ KnownNat (I.Count (I.Normalize a)),
578− KnownNat (Count b),
476+ KnownNat (I.Count (I.Normalize b)),
579− KnownNat (Count (Normalize (a, b))),
477+ KnownNat (I.Count (I.Normalize (a, b))),
580− FromLists e (Normalize (a, b)) a,
478+ I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
581− FromLists e (Normalize (a, b)) b
479+ I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
480+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
582− ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
481+ ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, b)
583khatri a b =
482khatri a b =
584 let kp1' = kp1 @e @a @b
483 let kp1' = kp1 @e @a @b
585 kp2' = kp2 @e @a @b
484 kp2' = kp2 @e @a @b
@@ -590,21 +489,22 @@ khatri a b =
590infixl 4 ><
489infixl 4 ><
591
490
592-- | Matrix product functor also known as kronecker product
491-- | Matrix product functor also known as kronecker product
593−(><) ::
492+(><) ::
594− forall e m p n q.
493+ forall e m p n q.
595− ( Num e,
494+ ( Num e,
596− KnownNat (Count m),
495+ KnownNat (I.Count (I.Normalize m)),
597− KnownNat (Count n),
496+ KnownNat (I.Count (I.Normalize n)),
598− KnownNat (Count p),
497+ KnownNat (I.Count (I.Normalize p)),
599− KnownNat (Count q),
498+ KnownNat (I.Count (I.Normalize q)),
600− KnownNat (Count (Normalize (m, n))),
499+ KnownNat (I.Count (I.Normalize (m, n))),
500+ KnownNat (I.Count (I.Normalize (p, q))),
601− FromLists e (Normalize (m, n)) m,
501+ I.FromLists e (I.Normalize (m, n)) (I.Normalize m),
602− FromLists e (Normalize (m, n)) n,
502+ I.FromLists e (I.Normalize (m, n)) (I.Normalize n),
603− KnownNat (Count (Normalize (p, q))),
503+ I.FromLists e (I.Normalize (p, q)) (I.Normalize p),
604− FromLists e (Normalize (p, q)) p,
504+ I.FromLists e (I.Normalize (p, q)) (I.Normalize q),
605− FromLists e (Normalize (p, q)) q
505+ I.Normalize (m, n) ~ I.Normalize (I.Normalize m, I.Normalize n),
606− )
506+ I.Normalize (p, q) ~ I.Normalize (I.Normalize p, I.Normalize q)
607− => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
507+ ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)
608(><) a b =
508(><) a b =
609 let kp1' = kp1 @e @m @n
509 let kp1' = kp1 @e @m @n
610 kp2' = kp2 @e @m @n
510 kp2' = kp2 @e @m @n
@@ -614,132 +514,78 @@ infixl 4 ><
614
514
615-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
515-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
616--
516--
517+-- Law:
518+--
617-- @
519-- @
618-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
520-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
619-- @
521-- @
620abideJS :: Matrix e cols rows -> Matrix e cols rows
522abideJS :: 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
523+abideJS (M m) = M (I.abideJS m)
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)
626
524
627-- Matrix abide Split Junc
525-- Matrix abide Split Junc
628
526
629-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
527-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
630--
528--
529+-- Law:
530+--
631-- @
531-- @
632-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
532-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
633-- @
533-- @
634abideSJ :: Matrix e cols rows -> Matrix e cols rows
534abideSJ :: 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
535+abideSJ (M m) = M (I.abideSJ m)
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)
640
536
641-- Matrix transposition
537-- Matrix transposition
642
538
643-- | Matrix transposition.
539-- | Matrix transposition.
644tr :: Matrix e cols rows -> Matrix e rows cols
540tr :: Matrix e cols rows -> Matrix e rows cols
645−tr Empty = Empty
541+tr (M m) = M (I.tr m)
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)
649
542
650-- Selective 'select' operator
543-- Selective 'select' operator
651
544
652-- | Selective functors 'select' operator equivalent inspired by the
545-- | Selective functors 'select' operator equivalent inspired by the
653-- ArrowMonad solution presented in the paper.
546-- ArrowMonad solution presented in the paper.
654−select :: (Bounded a1, Bounded b, Enum a1, Enum b, Num e, Ord e,
547+select ::
655− KnownNat (Count a2), KnownNat (Count rows), FromLists e rows a2,
548+ ( Bounded a,
656− FromLists e rows rows, Eq b) =>
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+ )
657− Matrix e cols (Either a2 rows) -> (a1 -> b) -> Matrix e cols rows
562+ => Matrix e cols (Either a b) -> (a -> b) -> Matrix e cols b
658−select m y =
563+select (M m) y = M (I.select m y)
659− let f = fromF y
660− in junc f identity `comp` m
661
564
662-- McCarthy's Conditional
565-- McCarthy's Conditional
663
566
664-- | McCarthy's Conditional expresses probabilistic choice.
567-- | McCarthy's Conditional expresses probabilistic choice.
665cond ::
568cond ::
666− ( cols ~ FromNat (Count cols),
569+ ( I.Normalize (I.Normalize a) ~ I.Normalize a,
667− KnownNat (Count cols),
570+ KnownNat (I.Count (I.Normalize a)),
668− FromLists e () cols,
571+ I.FromLists e () (I.Normalize a),
669− FromLists e cols (),
572+ I.FromLists e (I.Normalize a) (),
670− FromLists e cols cols,
573+ I.FromLists e (I.Normalize a) (I.Normalize a),
671 Bounded a,
574 Bounded a,
672 Enum a,
575 Enum a,
673 Num e,
576 Num e,
674 Ord e
577 Ord e
675 )
578 )
676 =>
579 =>
677− (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
580+ (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b
678−cond p f g = junc f g `comp` grd p
581+cond p (M a) (M b) = M (I.cond p a b)
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)
710
582
711-- Pretty print
583-- Pretty print
712
584
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−
732-- | Matrix pretty printer
585-- | Matrix pretty printer
733−pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String
586+pretty :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> String
734−pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
587+pretty (M m) = I.pretty m
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 ""
742
588
743-- | Matrix pretty printer
589-- | Matrix pretty printer
744−prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()
590+prettyPrint :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> IO ()
745−prettyPrint = putStrLn . pretty
591+prettyPrint (M m) = I.prettyPrint m