git.iko.soy/laop
on master help sign in
Added documentation
b3fbc73Armando Santos
app/Main.hs+1−1
compare with master
unifiedsplit
@@ -34,7 +34,7 @@ mulSS = coerceNat (*)
34
34
35sumSSM = fromF' (uncurry sumSS)
35sumSSM = fromF' (uncurry sumSS)
36
36
37−mulSSM3 = fromF' (mulSS (Nat 3))
37+mulSSM3 = fromF' (mulSS (nat 3))
38
38
39die :: Dist (Natural 6) 6
39die :: Dist (Natural 6) 6
40die = uniform [nat @6 1 .. nat 6]
40die = uniform [nat @6 1 .. nat 6]
src/Dist.hs+45−10
@@ -1,13 +1,48 @@
1+-----------------------------------------------------------------------------
2+-- |
3+-- Module : Dist
4+-- Copyright : (c) Armando Santos 2019-2020
5+-- Maintainer : armandoifsantos@gmail.com
6+-- Stability : experimental
7+--
8+-- __LAoP__ is a library for algebraic (inductive) construction and manipulation of matrices
9+-- in Haskell. See <https://github.com/bolt12/master-thesis my Msc Thesis> for the
10+-- motivation behind the library, the underlying theory, and implementation details.
11+--
12+-- This module exports a type synonym 'Dist'
13+-- that represents a stochastic distribution
14+-- matrix and several distribution construction
15+-- functions.
16+--
17+-----------------------------------------------------------------------------
18+
1module Dist
19module Dist
2− (
20+ ( -- | If the sum of the rows of a column matrix
21+ -- is equal to 1 then this stochastic matrix
22+ -- can be seen as a probability distribution.
23+ --
24+ --
25+ -- This module is still experimental but it's
26+ -- already possible to model probabilistic programming
27+ -- problems with it. Import 'Matrix.Nat' or 'Matrix.Type'
28+ -- to access LAoP matrix combinators and then all you have
29+ -- to do is to define your sample space, either by creating a new data
30+ -- type or by abstracting it out via 'Natural'.
31+ --
32+ -- Write manipulation functions and promote them to matrices via
33+ -- 'fromF' or 'fromF'' and you're good to go!
34+
35+ -- * 'Dist' and 'Prob' type synonyms
3− Dist(..),
36+ Dist (..),
37+ Prob,
38+ -- * Distribution construction functions
4− choose,
39+ choose,
5− shape,
40+ shape,
6− linear,
41+ linear,
7− uniform,
42+ uniform,
8− negExp,
43+ negExp,
9− normal
44+ normal,
10− )
45+ )
11− where
46+where
12
47
13import Dist.Internal
48import Dist.Internal
src/Dist/Internal.hs+12−1
@@ -5,6 +5,7 @@
5module Dist.Internal
5module Dist.Internal
6 (
6 (
7 Dist(..),
7 Dist(..),
8+ Prob,
8 choose,
9 choose,
9 shape,
10 shape,
10 linear,
11 linear,
@@ -17,12 +18,18 @@ module Dist.Internal
17import Matrix.Nat
18import Matrix.Nat
18import Utils
19import Utils
19
20
21+-- | Type synonym for probability value
20type Prob = Double
22type Prob = Double
23+
24+-- | Type synonym for column vector matrices. This represents a probability
25+-- distribution.
21type Dist a m = (FromLists Prob () (FromNat m)) => Matrix Prob 1 m
26type Dist a m = (FromLists Prob () (FromNat m)) => Matrix Prob 1 m
22
27
28+-- | Constructs a Bernoulli distribution
23choose :: Prob -> Dist a 2
29choose :: Prob -> Dist a 2
24choose prob = col [prob, 1 - prob]
30choose prob = col [prob, 1 - prob]
25
31
32+-- | Creates a distribution given a shape function
26shape :: (Prob -> Prob) -> [a] -> Dist a m
33shape :: (Prob -> Prob) -> [a] -> Dist a m
27shape _ [] = error "Probability.shape: empty list"
34shape _ [] = error "Probability.shape: empty list"
28shape f xs =
35shape f xs =
@@ -30,19 +37,23 @@ shape f xs =
30 ps = map f (iterate (+incr) 0)
37 ps = map f (iterate (+incr) 0)
31 in fromFreqs (zip xs ps)
38 in fromFreqs (zip xs ps)
32
39
40+-- | Constructs a Linear distribution
33linear :: [a] -> Dist a m
41linear :: [a] -> Dist a m
34linear = shape id
42linear = shape id
35
43
44+-- | Constructs an Uniform distribution
36uniform :: [a] -> Dist a m
45uniform :: [a] -> Dist a m
37uniform = shape (const 1)
46uniform = shape (const 1)
38
47
48+-- | Constructs an Negative Exponential distribution
39negExp :: [a] -> Dist a m
49negExp :: [a] -> Dist a m
40negExp = shape (\x -> exp (-x))
50negExp = shape (\x -> exp (-x))
41
51
52+-- | Constructs an Normal distribution
42normal :: [a] -> Dist a m
53normal :: [a] -> Dist a m
43normal = shape (normalCurve 0.5 0.5)
54normal = shape (normalCurve 0.5 0.5)
44
55
45−---
56+-- Auxiliary functions
46
57
47fromFreqs :: [(a,Prob)] -> Dist a m
58fromFreqs :: [(a,Prob)] -> Dist a m
48fromFreqs xs = col (map (\(x,p) -> p/q) xs)
59fromFreqs xs = col (map (\(x,p) -> p/q) xs)
src/Matrix/Nat.hs+67−61
@@ -13,6 +13,26 @@
13{-# LANGUAGE TypeOperators #-}
13{-# LANGUAGE TypeOperators #-}
14{-# LANGUAGE UndecidableInstances #-}
14{-# LANGUAGE UndecidableInstances #-}
15
15
16+-----------------------------------------------------------------------------
17+-- |
18+-- Module : Matrix.Nat
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 a newtype wrapper around 'Matrix.Type.Matrix' that
31+-- uses type level naturals instead of standard data types for the matrices
32+-- dimensions.
33+--
34+-----------------------------------------------------------------------------
35+
16module Matrix.Nat
36module Matrix.Nat
17 ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
37 ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
18 --
38 --
@@ -95,9 +115,7 @@ module Matrix.Nat
95 -- | Note that given the restrictions imposed it is not possible to
115 -- | Note that given the restrictions imposed it is not possible to
96 -- implement the standard type classes present in standard Haskell.
116 -- implement the standard type classes present in standard Haskell.
97 -- *** Matrix pairing projections
117 -- *** Matrix pairing projections
98− KhatriP1,
99 kp1,
118 kp1,
100− KhatriP2,
101 kp2,
119 kp2,
102
120
103 -- *** Matrix pairing
121 -- *** Matrix pairing
@@ -340,59 +358,38 @@ infixl 5 -|-
340
358
341-- Khatri Rao Product and projections
359-- Khatri Rao Product and projections
342
360
343−class KhatriP1 e (m :: Nat) (k :: Nat) where
361+kp1 ::
344− kp1 :: Matrix e (m * k) m
345−
346−instance KhatriP1 e 0 k where
347− kp1 = empty
348−
349−instance
350− forall e m k.
362+ forall e m k .
351 ( Num e,
363 ( Num e,
352− KnownNat k,
353− I.FromLists e (I.FromNat (m * k)) (I.FromNat m),
354 KnownNat (I.Count (I.FromNat m)),
364 KnownNat (I.Count (I.FromNat m)),
355− KnownNat (I.Count (I.FromNat (m * k)))
356− ) =>
357− KhatriP1 e m k
358− where
359− kp1 = matrixBuilder f
360− where
361− offset = fromInteger (natVal (Proxy :: Proxy k))
362− f (x, y)
363− | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
364− | otherwise = 0
365−
366−class KhatriP2 e (m :: Nat) (k :: Nat) where
367− kp2 :: Matrix e (m * k) k
368−
369−instance KhatriP2 e m 0 where
370− kp2 = empty
371−
372−instance
373− forall e m k.
374− ( Num e,
375− KnownNat k,
376 KnownNat (I.Count (I.FromNat k)),
365 KnownNat (I.Count (I.FromNat k)),
366+ KnownNat (I.Count (I.FromNat (m * k))),
377− I.FromLists e (I.FromNat (m * k)) (I.FromNat k),
367+ I.FromLists e (I.FromNat (m * k)) (I.FromNat m),
378− KnownNat (I.Count (I.FromNat m)),
368+ I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
379− KnownNat (I.Count (I.FromNat (m * k)))
369+ ) => Matrix e (m * k) m
380− ) =>
370+kp1 = M (I.kp1 @e @(I.FromNat m) @(I.FromNat k))
381− KhatriP2 e m k
371+
382− where
372+kp2 ::
383− kp2 = matrixBuilder f
373+ forall e m k.
384− where
374+ ( Num e,
385− offset = fromInteger (natVal (Proxy :: Proxy k))
375+ KnownNat (I.Count (I.FromNat k)),
386− f (x, y)
376+ I.FromLists e (I.FromNat (m * k)) (I.FromNat k),
387− | x == y || mod (y - x) offset == 0 = 1
377+ KnownNat (I.Count (I.FromNat m)),
388− | otherwise = 0
378+ KnownNat (I.Count (I.FromNat (m * k))),
379+ I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
380+ ) => Matrix e (m * k) k
381+kp2 = M (I.kp2 @e @(I.FromNat m) @(I.FromNat k))
389
382
390khatri ::
383khatri ::
391 forall e cols a b.
384 forall e cols a b.
392− (Num e, KhatriP1 e a b, KhatriP2 e a b) =>
385+ ( Num e,
393− Matrix e cols a ->
386+ KnownNat (I.Count (I.FromNat a)),
394− Matrix e cols b ->
387+ KnownNat (I.Count (I.FromNat b)),
388+ KnownNat (I.Count (I.FromNat (a * b))),
389+ I.FromLists e (I.FromNat (a * b)) (I.FromNat a),
390+ I.FromLists e (I.FromNat (a * b)) (I.FromNat b),
391+ I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))
395− Matrix e cols (a * b)
392+ ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
396khatri a b =
393khatri a b =
397 let kp1' = kp1 @e @a @b
394 let kp1' = kp1 @e @a @b
398 kp2' = kp2 @e @a @b
395 kp2' = kp2 @e @a @b
@@ -404,10 +401,20 @@ infixl 4 ><
404
401
405(><) ::
402(><) ::
406 forall e m p n q.
403 forall e m p n q.
407− (Num e, KhatriP1 e m n, KhatriP2 e m n, KhatriP1 e p q, KhatriP2 e p q) =>
404+ ( Num e,
408− Matrix e m p ->
405+ KnownNat (I.Count (I.FromNat m)),
409− Matrix e n q ->
406+ KnownNat (I.Count (I.FromNat n)),
407+ KnownNat (I.Count (I.FromNat p)),
408+ KnownNat (I.Count (I.FromNat q)),
409+ KnownNat (I.Count (I.FromNat (m * n))),
410+ KnownNat (I.Count (I.FromNat (p * q))),
411+ I.FromLists e (I.FromNat (m * n)) (I.FromNat m),
412+ I.FromLists e (I.FromNat (m * n)) (I.FromNat n),
413+ I.FromLists e (I.FromNat (p * q)) (I.FromNat p),
414+ I.FromLists e (I.FromNat (p * q)) (I.FromNat q),
415+ I.FromNat (m * n) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat n)),
416+ I.FromNat (p * q) ~ I.FromNat (I.Count (I.FromNat p) * I.Count (I.FromNat q))
410− Matrix e (m * n) (p * q)
417+ ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
411(><) a b =
418(><) a b =
412 let kp1' = kp1 @e @m @n
419 let kp1' = kp1 @e @m @n
413 kp2' = kp2 @e @m @n
420 kp2' = kp2 @e @m @n
@@ -430,13 +437,13 @@ tr (M m) = M (I.tr m)
430
437
431-- Selective 'select' operator
438-- Selective 'select' operator
432
439
433−select :: (Bounded a1, Bounded b, Enum a1, Enum b, Num e, Ord e,
440+select :: ( Bounded a1, Bounded b, Enum a1, Enum b, Num e, Ord e,
434− KnownNat (I.Count a2), KnownNat (I.Count (I.FromNat rows1)),
441+ KnownNat (I.Count a2), KnownNat (I.Count (I.FromNat rows1)),
435− I.FromLists e (I.FromNat rows1) a2,
442+ I.FromLists e (I.FromNat rows1) a2,
436− I.FromLists e (I.FromNat rows1) (I.FromNat rows1), Eq b,
443+ I.FromLists e (I.FromNat rows1) (I.FromNat rows1), Eq b,
437− I.FromNat cols1 ~ I.FromNat cols2,
444+ I.FromNat cols1 ~ I.FromNat cols2,
438− I.FromNat rows2 ~ Either a2 (I.FromNat rows1)) =>
445+ I.FromNat rows2 ~ Either a2 (I.FromNat rows1)) =>
439− Matrix e cols1 rows2 -> (a1 -> b) -> Matrix e cols2 rows1
446+ Matrix e cols1 rows2 -> (a1 -> b) -> Matrix e cols2 rows1
440select (M m) y = M (I.select m y)
447select (M m) y = M (I.select m y)
441
448
442-- McCarthy's Conditional
449-- McCarthy's Conditional
@@ -447,7 +454,6 @@ cond ::
447 I.FromLists e () (I.FromNat cols),
454 I.FromLists e () (I.FromNat cols),
448 I.FromLists e (I.FromNat cols) (),
455 I.FromLists e (I.FromNat cols) (),
449 I.FromLists e (I.FromNat cols) (I.FromNat cols),
456 I.FromLists e (I.FromNat cols) (I.FromNat cols),
450− I.KhatriP2 e () (I.FromNat cols),
451 Bounded a,
457 Bounded a,
452 Enum a,
458 Enum a,
453 Num e,
459 Num e,
src/Matrix/Type.hs+171−65
@@ -13,22 +13,34 @@
13{-# LANGUAGE TypeOperators #-}
13{-# LANGUAGE TypeOperators #-}
14{-# LANGUAGE UndecidableInstances #-}
14{-# LANGUAGE UndecidableInstances #-}
15
15
16+-----------------------------------------------------------------------------
17+-- |
18+-- Module : Matrix.Type
19+-- Copyright : (c) Armando Santos 2019-2020
20+-- Maintainer : armandoifsantos@gmail.com
21+-- Stability : experimental
22+--
23+-- The LAoP discipline generalises relations and functions treating them as
24+-- Boolean matrices and in turn consider these as arrows.
25+--
26+-- __LAoP__ is a library for algebraic (inductive) construction and manipulation of matrices
27+-- in Haskell. See <https://github.com/bolt12/master-thesis my Msc Thesis> for the
28+-- motivation behind the library, the underlying theory, and implementation details.
29+--
30+-- This module offers many of the combinators mentioned in the work of
31+-- Macedo (2012) and Oliveira (2012).
32+--
33+-----------------------------------------------------------------------------
34+
16module Matrix.Type
35module Matrix.Type
17− ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
18− --
19− -- LAoP generalises relations and functions treating them as
20− -- Boolean matrices and in turn consider these as arrows.
21− -- This library offers many of the combinators mentioned in the work of
22− -- Macedo (2012) and Oliveira (2012).
23− --
24− -- This definition makes use of the fact that 'Void' is
36+ ( -- | This definition makes use of the fact that 'Void' is
25− -- isomorphic to 0 and '()' to 1 and captures matrix
37+ -- isomorphic to 0 and '()' to 1 and captures matrix
26− -- dimensions as stacks of 'Either's.
38+ -- dimensions as stacks of 'Either's.
27 --
39 --
28− -- There exists two type families that make it easier to write
40+ -- There exists two type families that make it easier to write
29− -- matrix dimensions: 'FromNat' and 'Count'. This approach
41+ -- matrix dimensions: 'FromNat' and 'Count'. This approach
30− -- leads to a very straightforward implementation
42+ -- leads to a very straightforward implementation
31− -- of LAoP combinators.
43+ -- of LAoP combinators.
32
44
33 -- * Type safe matrix representation
45 -- * Type safe matrix representation
34 Matrix (..),
46 Matrix (..),
@@ -95,9 +107,7 @@ module Matrix.Type
95 -- | Note that given the restrictions imposed it is not possible to
107 -- | Note that given the restrictions imposed it is not possible to
96 -- implement the standard type classes present in standard Haskell.
108 -- implement the standard type classes present in standard Haskell.
97 -- *** Matrix pairing projections
109 -- *** Matrix pairing projections
98− KhatriP1,
99 kp1,
110 kp1,
100− KhatriP2,
101 kp2,
111 kp2,
102
112
103 -- *** Matrix pairing
113 -- *** Matrix pairing
@@ -127,8 +137,9 @@ import Data.List
127import Data.Proxy
137import Data.Proxy
128import Data.Void
138import Data.Void
129import GHC.TypeLits
139import GHC.TypeLits
140+import GHC.Generics
130
141
131−-- | Matrix data type
142+-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
132data Matrix e cols rows where
143data Matrix e cols rows where
133 Empty :: Matrix e Void Void
144 Empty :: Matrix e Void Void
134 One :: e -> Matrix e () ()
145 One :: e -> Matrix e () ()
@@ -137,17 +148,24 @@ data Matrix e cols rows where
137
148
138deriving instance (Show e) => Show (Matrix e cols rows)
149deriving instance (Show e) => Show (Matrix e cols rows)
139
150
140−-- | Type family that computes the cardinality of a given type dimension
151+-- | Type family that computes the cardinality of a given type dimension.
152+-- It can also count the cardinality of custom types that implement the
153+-- 'Generic' instance.
141type family Count (d :: Type) where
154type family Count (d :: Type) where
142− Count Void = 0
143− Count () = 1
144− Count Bool = 2
145 Count (Natural n) = n
155 Count (Natural n) = n
146 Count (Either a b) = (+) (Count a) (Count b)
156 Count (Either a b) = (+) (Count a) (Count b)
147 Count (a, b) = (*) (Count a) (Count b)
157 Count (a, b) = (*) (Count a) (Count b)
148 Count (a -> b) = (^) (Count b) (Count a)
158 Count (a -> b) = (^) (Count b) (Count a)
149−
159+ -- Generics
160+ Count (M1 _ _ f p) = Count (f p)
161+ Count (K1 _ _ _) = 1
162+ Count (V1 _) = 0
163+ Count (U1 _) = 1
164+ Count ((:*:) a b p) = Count (a p) * Count (b p)
165+ Count ((:+:) a b p) = Count (a p) + Count (b p)
166+ Count d = Count (Rep d R)
167+
150−-- | Type family that computes of a given type dimension from a fiven natural
168+-- | Type family that computes of a given type dimension from a given natural
151type family FromNat (n :: Nat) where
169type family FromNat (n :: Nat) where
152 FromNat 0 = Void
170 FromNat 0 = Void
153 FromNat 1 = ()
171 FromNat 1 = ()
@@ -199,47 +217,65 @@ instance Num e => Num (Matrix e cols rows) where
199
217
200-- Primitives
218-- Primitives
201
219
220+-- | Empty matrix constructor
202empty :: Matrix e Void Void
221empty :: Matrix e Void Void
203empty = Empty
222empty = Empty
204
223
224+-- | Unit matrix constructor
205one :: e -> Matrix e () ()
225one :: e -> Matrix e () ()
206one = One
226one = One
207
227
228+-- | Matrix 'Junc' constructor
208junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
229junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
209junc = Junc
230junc = Junc
210
231
211infixl 3 |||
232infixl 3 |||
233+
234+-- | Matrix 'Junc' constructor
212(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
235(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
213(|||) = Junc
236(|||) = Junc
214
237
238+-- | Matrix 'Split' constructor
215split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
239split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
216split = Split
240split = Split
217
241
218infixl 2 ===
242infixl 2 ===
243+
244+-- | Matrix 'Split' constructor
219(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
245(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
220(===) = Split
246(===) = Split
221
247
222-- Construction
248-- Construction
223
249
250+-- | Type class for defining the 'fromList' conversion function.
251+-- Given that it is not possible to branch on types at the term level type
252+-- classes are needed bery much like an inductive definition but on types.
224class FromLists e cols rows where
253class FromLists e cols rows where
254+ -- | Build a matrix out of a list of list of elements. Throws a runtime
255+ -- error if the dimensions do not match.
225 fromLists :: [[e]] -> Matrix e cols rows
256 fromLists :: [[e]] -> Matrix e cols rows
226
257
258+-- | Void base case
227instance FromLists e Void Void where
259instance FromLists e Void Void where
228 fromLists [] = Empty
260 fromLists [] = Empty
229 fromLists _ = error "Wrong dimensions"
261 fromLists _ = error "Wrong dimensions"
230
262
263+-- | Unit base case
231instance {-# OVERLAPPING #-} FromLists e () () where
264instance {-# OVERLAPPING #-} FromLists e () () where
232 fromLists [[e]] = One e
265 fromLists [[e]] = One e
233 fromLists _ = error "Wrong dimensions"
266 fromLists _ = error "Wrong dimensions"
234
267
268+-- | Row vector matrix definition
235instance (FromLists e cols ()) => FromLists e (Either () cols) () where
269instance (FromLists e cols ()) => FromLists e (Either () cols) () where
236 fromLists [h : t] = Junc (One h) (fromLists [t])
270 fromLists [h : t] = Junc (One h) (fromLists [t])
237 fromLists _ = error "Wrong dimensions"
271 fromLists _ = error "Wrong dimensions"
238
272
273+-- | Column vector matrix definition
239instance (FromLists e () rows) => FromLists e () (Either () rows) where
274instance (FromLists e () rows) => FromLists e () (Either () rows) where
240 fromLists ([h] : t) = Split (One h) (fromLists t)
275 fromLists ([h] : t) = Split (One h) (fromLists t)
241 fromLists _ = error "Wrong dimensions"
276 fromLists _ = error "Wrong dimensions"
242
277
278+-- | Arbitrary matrix definition
243instance {-# OVERLAPPABLE #-} (FromLists e cols c, FromLists e cols d) => FromLists e cols (Either c d) where
279instance {-# OVERLAPPABLE #-} (FromLists e cols c, FromLists e cols d) => FromLists e cols (Either c d) where
244 fromLists (h : t) =
280 fromLists (h : t) =
245 let lh = length h
281 let lh = length h
@@ -248,6 +284,8 @@ instance {-# OVERLAPPABLE #-} (FromLists e cols c, FromLists e cols d) => FromLi
248 then Split (fromLists [h]) (fromLists t)
284 then Split (fromLists [h]) (fromLists t)
249 else error "Not all rows have the same length"
285 else error "Not all rows have the same length"
250
286
287+-- | Matrix builder function. Constructs a matrix provided with
288+-- a construction function.
251matrixBuilder ::
289matrixBuilder ::
252 forall e cols rows.
290 forall e cols rows.
253 ( FromLists e cols rows,
291 ( FromLists e cols rows,
@@ -262,12 +300,17 @@ matrixBuilder f =
262 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
300 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
263 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
301 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
264
302
303+-- | Constructs a column vector matrix
265col :: (FromLists e () rows) => [e] -> Matrix e () rows
304col :: (FromLists e () rows) => [e] -> Matrix e () rows
266col = fromLists . map (: [])
305col = fromLists . map (: [])
267
306
307+-- | Constructs a row vector matrix
268row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
308row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
269row = fromLists . (: [])
309row = fromLists . (: [])
270
310
311+-- | Lifts functions to matrices with arbitrary dimensions.
312+-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
313+-- types @a@ or @b@ allows.
271fromF ::
314fromF ::
272 forall a b cols rows e.
315 forall a b cols rows e.
273 ( Bounded a,
316 ( Bounded a,
@@ -302,6 +345,8 @@ fromF f =
302 buildList [] _ = []
345 buildList [] _ = []
303 buildList l r = take r l : buildList (drop r l) r
346 buildList l r = take r l : buildList (drop r l) r
304
347
348+-- | Lifts functions to matrices with dimensions matching @a@ and @b@
349+-- cardinality's.
305fromF' ::
350fromF' ::
306 forall a b e.
351 forall a b e.
307 ( Bounded a,
352 ( Bounded a,
@@ -338,32 +383,40 @@ fromF' f =
338
383
339-- Conversion
384-- Conversion
340
385
386+-- | Converts a matrix to a list of lists of elements.
341toLists :: Matrix e cols rows -> [[e]]
387toLists :: Matrix e cols rows -> [[e]]
342toLists Empty = []
388toLists Empty = []
343toLists (One e) = [[e]]
389toLists (One e) = [[e]]
344toLists (Split l r) = toLists l ++ toLists r
390toLists (Split l r) = toLists l ++ toLists r
345toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
391toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
346
392
393+-- | Converts a matrix to a list of elements.
347toList :: Matrix e cols rows -> [e]
394toList :: Matrix e cols rows -> [e]
348toList = concat . toLists
395toList = concat . toLists
349
396
350-- Zeros Matrix
397-- Zeros Matrix
351
398
399+-- | The zero matrix. A matrix wholly filled with zeros.
352zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
400zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
353zeros = matrixBuilder (const 0)
401zeros = matrixBuilder (const 0)
354
402
355-- Ones Matrix
403-- Ones Matrix
356
404
405+-- | The ones matrix. A matrix wholly filled with ones.
406+-- Also known as T (Top) matrix.
357ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
407ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
358ones = matrixBuilder (const 1)
408ones = matrixBuilder (const 1)
359
409
360-- Const Matrix
410-- Const Matrix
361
411
412+-- | The constant matrix constructor. A matrix wholly filled with a given
413+-- value.
362constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows
414constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows
363constant e = matrixBuilder (const e)
415constant e = matrixBuilder (const e)
364
416
365-- Bang Matrix
417-- Bang Matrix
366
418
419+-- | The T (Top) row vector matrix.
367bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()
420bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()
368bang =
421bang =
369 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
422 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
@@ -371,11 +424,15 @@ bang =
371
424
372-- Identity Matrix
425-- Identity Matrix
373
426
427+-- | Identity matrix.
374identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols
428identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols
375identity = matrixBuilder (bool 0 1 . uncurry (==))
429identity = matrixBuilder (bool 0 1 . uncurry (==))
376
430
377-- Matrix composition (MMM)
431-- Matrix composition (MMM)
378
432
433+-- | Matrix composition. Equivalent to matrix-matrix multiplication.
434+-- This definition takes advantage of divide-and-conquer and fusion laws
435+-- from LAoP.
379comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
436comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
380comp Empty Empty = Empty
437comp Empty Empty = Empty
381comp (One a) (One b) = One (a * b)
438comp (One a) (One b) = One (a * b)
@@ -385,12 +442,14 @@ comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc fusion law
385
442
386-- Projections
443-- Projections
387
444
445+-- | Biproduct first component projection
388p1 :: 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
446p1 :: 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
389p1 =
447p1 =
390 let iden = identity :: Matrix e m m
448 let iden = identity :: Matrix e m m
391 zero = zeros :: Matrix e n m
449 zero = zeros :: Matrix e n m
392 in junc iden zero
450 in junc iden zero
393
451
452+-- | Biproduct second component projection
394p2 :: 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
453p2 :: 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
395p2 =
454p2 =
396 let iden = identity :: Matrix e n n
455 let iden = identity :: Matrix e n n
@@ -399,17 +458,29 @@ p2 =
399
458
400-- Injections
459-- Injections
401
460
461+-- | Biproduct first component injection
402i1 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
462i1 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
403i1 = tr p1
463i1 = tr p1
404
464
465+-- | Biproduct second component injection
405i2 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
466i2 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
406i2 = tr p2
467i2 = tr p2
407
468
408-- Dimensions
469-- Dimensions
409
470
471+-- | Obtain the number of rows.
472+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
473+-- dimensions in constant time.
474+-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
475+-- exchange for performance.
410rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int
476rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int
411rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
477rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
412
478
479+-- | Obtain the number of columns.
480+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
481+-- dimensions in constant time.
482+-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
483+-- exchange for performance.
413columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int
484columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int
414columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
485columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
415
486
@@ -417,6 +488,7 @@ columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
417
488
418infixl 5 -|-
489infixl 5 -|-
419
490
491+-- | Matrix coproduct functor also known as matrix direct sum.
420(-|-) ::
492(-|-) ::
421 forall e n k m j.
493 forall e n k m j.
422 ( Num e,
494 ( Num e,
@@ -434,51 +506,57 @@ infixl 5 -|-
434
506
435-- Khatri Rao Product and projections
507-- Khatri Rao Product and projections
436
508
437−class KhatriP1 e m k where
509+-- | Khatri Rao product first component projection matrix.
438− kp1 :: Matrix e (Normalize (m, k)) m
510+kp1 ::
439−
511+ forall e m k .
440−instance KhatriP1 e Void k where
441− kp1 = Empty
442−
443−instance
444 ( Num e,
512 ( Num e,
445 KnownNat (Count k),
513 KnownNat (Count k),
446 FromLists e (FromNat (Count m * Count k)) m,
514 FromLists e (FromNat (Count m * Count k)) m,
447 KnownNat (Count m),
515 KnownNat (Count m),
448 KnownNat (Count (Normalize (m, k)))
516 KnownNat (Count (Normalize (m, k)))
449− ) =>
517+ ) => Matrix e (Normalize (m, k)) m
450− KhatriP1 e m k
518+kp1 = matrixBuilder f
451 where
519 where
452− kp1 = matrixBuilder f
453− where
454− offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
520+ offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
455− f (x, y)
521+ f (x, y)
456− | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
522+ | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
457− | otherwise = 0
523+ | otherwise = 0
458−
524+
459−class KhatriP2 e m k where
525+-- | Khatri Rao product second component projection matrix.
460− kp2 :: Matrix e (Normalize (m, k)) k
526+kp2 ::
461−
527+ forall e m k .
462−instance KhatriP2 e m Void where
463− kp2 = Empty
464−
465−instance
466− ( Num e,
528+ ( Num e,
467− KnownNat (Count k),
529+ KnownNat (Count k),
468− FromLists e (FromNat (Count m * Count k)) k,
530+ FromLists e (FromNat (Count m * Count k)) k,
469− KnownNat (Count m),
531+ KnownNat (Count m),
470− KnownNat (Count (Normalize (m, k)))
532+ KnownNat (Count (Normalize (m, k)))
471− ) =>
533+ ) => Matrix e (Normalize (m, k)) k
472− KhatriP2 e m k
534+kp2 = matrixBuilder f
473 where
535 where
474− kp2 = matrixBuilder f
475− where
476− offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
536+ offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
477− f (x, y)
537+ f (x, y)
478− | x == y || mod (y - x) offset == 0 = 1
538+ | x == y || mod (y - x) offset == 0 = 1
479− | otherwise = 0
539+ | otherwise = 0
480−
540+
541+-- | Khatri Rao Matrix product also known as matrix pairing.
542+-- NOTE: That this is not a true categorical product, see for instance:
543+--
544+-- @
545+-- | kp1 `comp` khatri a b == a
546+-- khatri a b ==> |
547+-- | kp2 `comp` khatri a b == b
548+-- @
549+--
550+-- __Emphasis__ on the implication symbol.
551+khatri ::
552+ forall e cols a b.
553+ ( Num e,
554+ KnownNat (Count a),
555+ KnownNat (Count b),
556+ KnownNat (Count (Normalize (a, b))),
557+ FromLists e (Normalize (a, b)) a,
558+ FromLists e (Normalize (a, b)) b
481−khatri :: forall e cols a b. (Num e, KhatriP1 e a b, KhatriP2 e a b) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
559+ ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
482khatri a b =
560khatri a b =
483 let kp1' = kp1 @e @a @b
561 let kp1' = kp1 @e @a @b
484 kp2' = kp2 @e @a @b
562 kp2' = kp2 @e @a @b
@@ -488,7 +566,22 @@ khatri a b =
488
566
489infixl 4 ><
567infixl 4 ><
490
568
569+-- | Matrix product functor also known as kronecker product
570+(><) ::
571+ forall e m p n q.
572+ ( Num e,
573+ KnownNat (Count m),
574+ KnownNat (Count n),
575+ KnownNat (Count p),
576+ KnownNat (Count q),
577+ KnownNat (Count (Normalize (m, n))),
578+ FromLists e (Normalize (m, n)) m,
579+ FromLists e (Normalize (m, n)) n,
580+ KnownNat (Count (Normalize (p, q))),
581+ FromLists e (Normalize (p, q)) p,
582+ FromLists e (Normalize (p, q)) q
583+ )
491−(><) :: forall e m p n q. (Num e, KhatriP1 e m n, KhatriP2 e m n, KhatriP1 e p q, KhatriP2 e p q) => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
584+ => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
492(><) a b =
585(><) a b =
493 let kp1' = kp1 @e @m @n
586 let kp1' = kp1 @e @m @n
494 kp2' = kp2 @e @m @n
587 kp2' = kp2 @e @m @n
@@ -496,6 +589,11 @@ infixl 4 ><
496
589
497-- Matrix abide Junc Split
590-- Matrix abide Junc Split
498
591
592+-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
593+--
594+-- @
595+-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
596+-- @
499abideJS :: Matrix e cols rows -> Matrix e cols rows
597abideJS :: Matrix e cols rows -> Matrix e cols rows
500abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law
598abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law
501abideJS Empty = Empty
599abideJS Empty = Empty
@@ -505,6 +603,11 @@ abideJS (Split a b) = Split (abideJS a) (abideJS b)
505
603
506-- Matrix abide Split Junc
604-- Matrix abide Split Junc
507
605
606+-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
607+--
608+-- @
609+-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
610+-- @
508abideSJ :: Matrix e cols rows -> Matrix e cols rows
611abideSJ :: Matrix e cols rows -> Matrix e cols rows
509abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law
612abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law
510abideSJ Empty = Empty
613abideSJ Empty = Empty
@@ -514,6 +617,7 @@ abideSJ (Split a b) = Split (abideSJ a) (abideSJ b)
514
617
515-- Matrix transposition
618-- Matrix transposition
516
619
620+-- | Matrix transposition.
517tr :: Matrix e cols rows -> Matrix e rows cols
621tr :: Matrix e cols rows -> Matrix e rows cols
518tr Empty = Empty
622tr Empty = Empty
519tr (One e) = One e
623tr (One e) = One e
@@ -522,6 +626,8 @@ tr (Split a b) = Junc (tr a) (tr b)
522
626
523-- Selective 'select' operator
627-- Selective 'select' operator
524
628
629+-- | Selective functors 'select' operator equivalent inspired by the
630+-- ArrowMonad solution presented in the paper.
525select :: (Bounded a1, Bounded b, Enum a1, Enum b, Num e, Ord e,
631select :: (Bounded a1, Bounded b, Enum a1, Enum b, Num e, Ord e,
526 KnownNat (Count a2), KnownNat (Count rows), FromLists e rows a2,
632 KnownNat (Count a2), KnownNat (Count rows), FromLists e rows a2,
527 FromLists e rows rows, Eq b) =>
633 FromLists e rows rows, Eq b) =>
@@ -532,13 +638,13 @@ select m y =
532
638
533-- McCarthy's Conditional
639-- McCarthy's Conditional
534
640
641+-- | McCarthy's Conditional expresses probabilistic choice.
535cond ::
642cond ::
536 ( cols ~ FromNat (Count cols),
643 ( cols ~ FromNat (Count cols),
537 KnownNat (Count cols),
644 KnownNat (Count cols),
538 FromLists e () cols,
645 FromLists e () cols,
539 FromLists e cols (),
646 FromLists e cols (),
540 FromLists e cols cols,
647 FromLists e cols cols,
541− KhatriP2 e () cols,
542 Bounded a,
648 Bounded a,
543 Enum a,
649 Enum a,
544 Num e,
650 Num e,
@@ -554,7 +660,6 @@ grd ::
554 FromLists e () q,
660 FromLists e () q,
555 FromLists e q (),
661 FromLists e q (),
556 FromLists e q q,
662 FromLists e q q,
557− KhatriP2 e () q,
558 Bounded a,
663 Bounded a,
559 Enum a,
664 Enum a,
560 Num e,
665 Num e,
@@ -571,7 +676,6 @@ corr ::
571 FromLists e () q,
676 FromLists e () q,
572 FromLists e q (),
677 FromLists e q (),
573 FromLists e q q,
678 FromLists e q q,
574− KhatriP2 e () q,
575 Bounded a,
679 Bounded a,
576 Enum a,
680 Enum a,
577 Num e,
681 Num e,
@@ -602,6 +706,7 @@ prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
602 widest = maximum $ fmap length v
706 widest = maximum $ fmap length v
603 fill str = replicate (widest - length str - 2) ' ' ++ str
707 fill str = replicate (widest - length str - 2) ' ' ++ str
604
708
709+-- | Matrix pretty printer
605pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String
710pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String
606pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
711pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
607 prettyAux (toLists m) (toLists m) ++
712 prettyAux (toLists m) (toLists m) ++
@@ -612,5 +717,6 @@ pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
612 fill str = replicate (widest - length str) ' ' ++ str
717 fill str = replicate (widest - length str) ' ' ++ str
613 blank = fill ""
718 blank = fill ""
614
719
720+-- | Matrix pretty printer
615prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()
721prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()
616prettyPrint = putStrLn . pretty
722prettyPrint = putStrLn . pretty
src/Utils.hs+97−7
@@ -1,9 +1,99 @@
1+-----------------------------------------------------------------------------
2+-- |
3+-- Module : Utils
4+-- Copyright : (c) Armando Santos 2019-2020
5+-- Maintainer : armandoifsantos@gmail.com
6+-- Stability : experimental
7+--
8+-- __LAoP__ is a library for algebraic (inductive) construction and manipulation of matrices
9+-- in Haskell. See <https://github.com/bolt12/master-thesis my Msc Thesis> for the
10+-- motivation behind the library, the underlying theory, and implementation details.
11+--
12+-- This module provides the 'Natural' data type.
13+-- The semantic associated with this data type is that
14+-- it's meant to be a restricted 'Int' value.
15+--
16+-----------------------------------------------------------------------------
17+
1−module Utils
18+module Utils
2− ( Natural(..),
19+ ( -- | Utility module that provides the 'Natural' data type.
20+ -- The semantic associated with this data type is that
21+ -- it's meant to be a restricted 'Int' value. For example
22+ -- the type @Natural 6@ can only be instanciated with @Nat n@
23+ -- where @0 <= n <= 6@. Why, You might ask, because with normal
24+ -- 'Int's it is not possible to have a decent @Enum (Int, Int)@
25+ -- instance. See the following probabilistic programming model as and
26+ -- example:
27+ --
28+ -- We want to calculate the probability of the sum of two dice throws.
29+ -- To do this we start by defining the sample space:
30+ --
31+ -- @
32+ -- type SampleSpace = Int -- We think 'Int' are enough
33+ --
34+ -- die :: Dist Int 6
35+ -- die = unifrom [1..6]
36+ --
37+ -- -- Promote 'Int' addition to a matrix
38+ -- addM = fromF (uncurry (+)) -- Impossible
39+ -- @
40+ --
41+ -- The last line is impossible because @(Int, Int)@ does not have
42+ -- a good 'Enum' instance: @[(0, 1), (0, 2), .. (0, maxBound), (1, 0),
43+ -- ..]@. And we'd like the addition matrix to be of 36 columns by 12
44+ -- rows but limited to integers up to @6@!
45+ --
46+ -- One way to solve this issue is by defining and auxilary data type to
47+ -- represent the sample space:
48+ --
49+ -- @
50+ -- data SampleSpace = S1 | S2 | S3 | S4 | S5 | S6
51+ -- deriving (Show, Eq, Enum, Bounded) -- Enum and Bounded are
52+ -- important
53+ -- @
54+ --
55+ -- And write the sample space addition function:
56+ --
57+ -- @
58+ -- ssAdd :: SampleSpace -> SampleSpace -> Int
59+ -- ssAdd a b = (fromEnum a + 1) + (fromEnum b + 1)
60+ -- @
61+ --
62+ -- And then promote that function to matrix and everything is alright:
63+ --
64+ -- @
65+ -- ssAddM = fromF' (uncurry ssAdd)
66+ --
67+ -- dieSumProb = ssAddM `comp` (khatri die die)
68+ -- @
69+ --
70+ -- This is a nice solution for small sample spaces. But for larger ones
71+ -- it is not feasible to write a data type with hundreds of constructors
72+ -- and then write manipulation functions that need to deal with them.
73+ -- To mitigate this limitation the 'Natural' type comes a long way and
74+ -- allows one to model the sample in an easier way. See for instance:
75+ --
76+ -- @
77+ -- ssAdd :: Natural 6 -> Natural 6 -> Natural 12
78+ -- ssAdd = coerceNat (+)
79+ --
80+ -- ssAddM = fromF' (uncurry sumSS)
81+ --
82+ -- die :: Dist (Natural 6) 6
83+ -- die = uniform [nat @6 1 .. nat 6]
84+ --
85+ -- dieSumProb = ssAddM `comp` (khatri die die)
86+ -- @
87+ --
88+ -- * 'Natural' data type
89+ Natural,
3− nat,
90+ nat,
91+
92+ -- * Coerce auxiliar functions to help promote 'Int' typed functions to
93+ -- 'Natural' typed functions.
4− coerceNat,
94+ coerceNat,
5− coerceNat2
95+ coerceNat2,
6− )
96+ )
7− where
97+where
8
98
9import Utils.Internal
99import Utils.Internal
src/Utils/Internal.hs+113−22
@@ -1,47 +1,136 @@
1−{-# LANGUAGE GeneralizedNewtypeDeriving #-}
2{-# LANGUAGE DataKinds #-}
1{-# LANGUAGE DataKinds #-}
3−{-# LANGUAGE KindSignatures #-}
4{-# LANGUAGE FlexibleInstances #-}
2{-# LANGUAGE FlexibleInstances #-}
3+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
4+{-# LANGUAGE KindSignatures #-}
5{-# LANGUAGE ScopedTypeVariables #-}
5{-# LANGUAGE ScopedTypeVariables #-}
6
6
7module Utils.Internal
7module Utils.Internal
8− ( Natural(..),
8+ ( -- | This is an internal module and it is not meant to be imported.
9+ --
10+ -- Utility module that provides the 'Natural' data type.
11+ -- The semantic associated with this data type is that
12+ -- it's meant to be a restricted 'Int' value. For example
13+ -- the type @Natural 6@ can only be instanciated with @Nat n@
14+ -- where @0 <= n <= 6@. Why, You might ask, because with normal
15+ -- 'Int's it is not possible to have a decent @Enum (Int, Int)@
16+ -- instance. See the following probabilistic programming model as and
17+ -- example:
18+ --
19+ -- We want to calculate the probability of the sum of two dice throws.
20+ -- To do this we start by defining the sample space:
21+ --
22+ -- @
23+ -- type SampleSpace = Int -- We think 'Int' are enough
24+ --
25+ -- die :: Dist Int 6
26+ -- die = unifrom [1..6]
27+ --
28+ -- -- Promote 'Int' addition to a matrix
29+ -- addM = fromF (uncurry (+)) -- Impossible
30+ -- @
31+ --
32+ -- The last line is impossible because @(Int, Int)@ does not have
33+ -- a good 'Enum' instance: @[(0, 1), (0, 2), .. (0, maxBound), (1, 0),
34+ -- ..]@. And we'd like the addition matrix to be of 36 columns by 12
35+ -- rows but limited to integers up to @6@!
36+ --
37+ -- One way to solve this issue is by defining and auxilary data type to
38+ -- represent the sample space:
39+ --
40+ -- @
41+ -- data SampleSpace = S1 | S2 | S3 | S4 | S5 | S6
42+ -- deriving (Show, Eq, Enum, Bounded) -- Enum and Bounded are
43+ -- important
44+ -- @
45+ --
46+ -- And write the sample space addition function:
47+ --
48+ -- @
49+ -- ssAdd :: SampleSpace -> SampleSpace -> Int
50+ -- ssAdd a b = (fromEnum a + 1) + (fromEnum b + 1)
51+ -- @
52+ --
53+ -- And then promote that function to matrix and everything is alright:
54+ --
55+ -- @
56+ -- ssAddM = fromF' (uncurry ssAdd)
57+ --
58+ -- dieSumProb = ssAddM `comp` (khatri die die)
59+ -- @
60+ --
61+ -- This is a nice solution for small sample spaces. But for larger ones
62+ -- it is not feasible to write a data type with hundreds of constructors
63+ -- and then write manipulation functions that need to deal with them.
64+ -- To mitigate this limitation the 'Natural' type comes a long way and
65+ -- allows one to model the sample in an easier way. See for instance:
66+ --
67+ -- @
68+ -- ssAdd :: Natural 6 -> Natural 6 -> Natural 12
69+ -- ssAdd = coerceNat (+)
70+ --
71+ -- ssAddM = fromF' (uncurry sumSS)
72+ --
73+ -- die :: Dist (Natural 6) 6
74+ -- die = uniform [nat @6 1 .. nat 6]
75+ --
76+ -- dieSumProb = ssAddM `comp` (khatri die die)
77+ -- @
78+ --
79+ -- * 'Natural' data type
80+ Natural,
9− nat,
81+ nat,
82+
83+ -- * Coerce auxiliar functions to help promote 'Int' typed functions to
84+ -- 'Natural' typed functions.
10− coerceNat,
85+ coerceNat,
11− coerceNat2
86+ coerceNat2,
12− )
87+ )
13− where
88+where
14
89
15−import GHC.TypeLits
16−import Data.Proxy
17import Data.Coerce
90import Data.Coerce
91+import Data.Proxy
92+import GHC.TypeLits
18
93
94+-- | Wrapper around 'Int's that have a restrictive semantic associated.
95+-- A value of type @'Natural' n@ can only be instanciated with some 'Int'
96+-- @i@ that's @0 <= i <= n@.
19newtype Natural (nat :: Nat) = Nat Int
97newtype Natural (nat :: Nat) = Nat Int
20 deriving (Show, Read, Eq, Num)
98 deriving (Show, Read, Eq, Num)
21
99
100+-- | Natural constructor function. Throws a runtime error if the 'Int'
101+-- value is greater than the corresponding @n@ in the @'Natural' n@ type.
22−nat :: forall n . (KnownNat n) => Int -> Natural n
102+nat :: forall n. (KnownNat n) => Int -> Natural n
103+nat i =
23−nat i = let nat = fromInteger (natVal (Proxy :: Proxy n))
104+ let nat = fromInteger (natVal (Proxy :: Proxy n))
24− in if i <= nat
105+ in if i <= nat
25− then Nat i
106+ then Nat i
26− else error "Off limits"
107+ else error "Off limits"
27
108
109+-- | Auxiliary function that promotes binary 'Int' functions to 'Natural'
110+-- binary functions.
28coerceNat :: (Int -> Int -> Int) -> (Natural a -> Natural b -> Natural c)
111coerceNat :: (Int -> Int -> Int) -> (Natural a -> Natural b -> Natural c)
29coerceNat = coerce
112coerceNat = coerce
30
113
114+-- | Auxiliary function that promotes ternary (binary) 'Int' functions to 'Natural'
115+-- functions.
31coerceNat2 :: ((Int, Int) -> Int -> Int) -> ((Natural a, Natural b) -> Natural c -> Natural d)
116coerceNat2 :: ((Int, Int) -> Int -> Int) -> ((Natural a, Natural b) -> Natural c -> Natural d)
32coerceNat2 = coerce
117coerceNat2 = coerce
33
118
34instance KnownNat n => Bounded (Natural n) where
119instance KnownNat n => Bounded (Natural n) where
35− minBound = Nat 0
120+ minBound = Nat 0
36− maxBound = Nat $ fromInteger (natVal (Proxy :: Proxy n))
121+ maxBound = Nat $ fromInteger (natVal (Proxy :: Proxy n))
37
122
38instance KnownNat n => Enum (Natural n) where
123instance KnownNat n => Enum (Natural n) where
39− toEnum = nat
124+ toEnum = nat
125+ -- | Throws a runtime error if the value is off limits
126+ fromEnum (Nat nat) =
40− fromEnum (Nat nat) = let val = fromInteger (natVal (Proxy :: Proxy n))
127+ let val = fromInteger (natVal (Proxy :: Proxy n))
41− in if nat > val
128+ in if nat > val
42− then error "Off limits"
129+ then error "Off limits"
43− else nat
130+ else nat
44
131
132+-- | Optimized 'Enum' instance for tuples that comply with the given
133+-- constraints.
45instance
134instance
46 ( Enum a,
135 ( Enum a,
47 Enum b,
136 Enum b,
@@ -49,12 +138,14 @@ instance
49 ) =>
138 ) =>
50 Enum (a, b)
139 Enum (a, b)
51 where
140 where
141+
52 toEnum i =
142 toEnum i =
53 let (listB :: [b]) = [minBound .. maxBound]
143 let (listB :: [b]) = [minBound .. maxBound]
54 lengthB = length listB
144 lengthB = length listB
55 fstI = div i lengthB
145 fstI = div i lengthB
56 sndI = mod i lengthB
146 sndI = mod i lengthB
57 in (toEnum fstI, toEnum sndI)
147 in (toEnum fstI, toEnum sndI)
148+
58 fromEnum (a, b) =
149 fromEnum (a, b) =
59 let (listB :: [b]) = [minBound .. maxBound]
150 let (listB :: [b]) = [minBound .. maxBound]
60 lengthB = length listB
151 lengthB = length listB