@@ -1 +1,190 @@
1−# laop
1+# laop - Linear Algebra of Programming library
2+
3+The LAoP discipline generalises relations and functions treating them as
4+Boolean matrices and in turn consider these as arrows.
5+
6+__LAoP__ is a library for algebraic (inductive) construction and manipulation of matrices
7+in Haskell. See <https://github.com/bolt12/master-thesis my Msc Thesis> for the
8+motivation behind the library, the underlying theory, and implementation details.
9+
10+This module offers many of the combinators mentioned in the work of
11+Macedo (2012) and Oliveira (2012).
12+
13+## Features
14+
15+This library offers:
16+
17+- One that uses normal datatypes (`Void`, `()`, `Either`) for matrix dimensions and two
18+ type families `FromNat` and `Count` to make it easier to work with these type of matrices.
19+- Other that uses type level naturals for the dimensions and is just a newtype wrapper
20+ around the other matrix data type.
21+- A very simple Probabilistic Programming module and several functions and data types to
22+ make it easier to deal with sample space.
23+
24+Given this, this new matrix formulation compared to other libraries one has much more advantages, such as:
25+
26+- Has an inductive definition enabling writing matrix manipulation functions in a much more elegant and calculational way;
27+- Statically typed dimensions;
28+- Polymorphic data type dimensions;
29+- Polymorphic matrix content;
30+- Awesome dimension type inference;
31+- Fast type natural conversion via `FromNat` type family;
32+- Matrix `Junc` and `Split`-ing in O(1);
33+- Matrix composition takes advantage of divide-and-conquer and fusion laws.
34+
35+Unfortunately, this approach does not solve the issue of type dimensions being in some way constrainted making it impossible to write Arrow instances, for example. Type inference isn't perfect, when it comes to infer the types of matrices which dimensions are computed using type level naturals multiplication, the compiler needs type annotations in order to succeed.
36+
37+## Example
38+
39+```Haskell
40+{-# LANGUAGE FlexibleContexts #-}
41+{-# LANGUAGE TypeOperators #-}
42+{-# LANGUAGE TypeApplications #-}
43+{-# LANGUAGE DataKinds #-}
44+
45+module Main where
46+
47+import Matrix.Nat
48+import Utils
49+import Dist
50+import GHC.TypeLits
51+import Data.Coerce
52+
53+-- Monty Hall Problem
54+data Outcome = Win | Lose
55+ deriving (Bounded, Enum, Eq, Show)
56+
57+switch :: Outcome -> Outcome
58+switch Win = Lose
59+switch Lose = Win
60+
61+firstChoice :: Dist Outcome m
62+firstChoice = col [1/3, 2/3]
63+
64+secondChoice :: Matrix Double 2 2
65+secondChoice = fromF switch
66+
67+-- Dice sum
68+
69+type SS = Natural 1 6
70+
71+sumSS :: SS -> SS -> Natural 2 12
72+sumSS = coerceNat (+)
73+
74+sumSSM = fromF' (uncurry sumSS)
75+
76+condition :: (Int, Int) -> Int -> Int
77+condition (fst, snd) thrd = if fst == snd
78+ then fst * 3
79+ else fst + snd + thrd
80+
81+conditionSS :: (SS, SS) -> SS -> Natural 3 18
82+conditionSS = coerceNat2 condition
83+
84+conditionalThrows = fromF' (uncurry conditionSS) `comp` khatri die (khatri die die)
85+
86+die :: Dist (Natural 1 6) 6
87+die = uniform [nat @1 @6 1 .. nat 6]
88+
89+-- Sprinkler
90+
91+rain :: Dist Bool 2
92+rain = choose 0.8
93+
94+sprinkler :: Matrix Double 2 2
95+sprinkler = fromLists [[0.6, 0.99], [0.4, 0.01]]
96+
97+grass :: Matrix Double 4 2
98+grass = fromLists [[1, 0.2, 0.1, 0.01], [0, 0.8, 0.9, 0.99]]
99+
100+state = khatri grass identity `comp` khatri sprinkler identity `comp` rain
101+
102+grass_wet = row [0,1] `comp` kp1 @Double @2 @4
103+
104+rainning = row [0,1] `comp` kp2 @Double @2 @2 `comp` kp2 @Double @2 @4
105+
106+main :: IO ()
107+main = do
108+ putStrLn "Monty Hall Problem solution:"
109+ prettyPrint (p1 @Double @1 `comp` secondChoice `comp` firstChoice)
110+ putStrLn "\n Sum of dices probability:"
111+ prettyPrint (sumSSM `comp` khatri die die)
112+ prettyPrintDist @(Natural 2 12) (sumSSM `comp` khatri die die)
113+ putStrLn "\n Conditional dice throw:"
114+ prettyPrintDist @(Natural 3 18) conditionalThrows
115+ putStrLn "\n Checking that the last result is indeed a distribution: "
116+ prettyPrint (bang `comp` sumSSM `comp` khatri die die)
117+ putStrLn "\n Probability of grass being wet:"
118+ prettyPrint (grass_wet `comp` state)
119+ putStrLn "\n Probability of rain:"
120+ prettyPrint (rainning `comp` state)
121+```
122+
123+```Shell
124+Monty Hall Problem solution:
125+┌ ┐
126+│ 0.6666666666666666 │
127+└ ┘
128+
129+ Sum of dices probability:
130+┌ ┐
131+│ 2.7777777777777776e-2 │
132+│ 5.555555555555555e-2 │
133+│ 8.333333333333333e-2 │
134+│ 0.1111111111111111 │
135+│ 0.1388888888888889 │
136+│ 0.16666666666666666 │
137+│ 0.1388888888888889 │
138+│ 0.1111111111111111 │
139+│ 8.333333333333333e-2 │
140+│ 5.555555555555555e-2 │
141+│ 2.7777777777777776e-2 │
142+└ ┘
143+Nat 7 16.666666666666664%
144+Nat 6 13.88888888888889%
145+Nat 8 13.88888888888889%
146+Nat 5 11.11111111111111%
147+Nat 9 11.11111111111111%
148+Nat 4 8.333333333333332%
149+Nat 10 8.333333333333332%
150+Nat 3 5.555555555555555%
151+Nat 11 5.555555555555555%
152+Nat 2 2.7777777777777777%
153+Nat 12 2.7777777777777777%
154+
155+
156+ Conditional dice throw:
157+Nat 9 12.962962962962962%
158+Nat 12 12.962962962962962%
159+Nat 10 11.11111111111111%
160+Nat 11 11.11111111111111%
161+Nat 8 8.333333333333332%
162+Nat 13 8.333333333333332%
163+Nat 6 6.481481481481481%
164+Nat 15 6.481481481481481%
165+Nat 7 5.555555555555555%
166+Nat 14 5.555555555555555%
167+Nat 3 2.7777777777777777%
168+Nat 18 2.7777777777777777%
169+Nat 5 1.8518518518518516%
170+Nat 16 1.8518518518518516%
171+Nat 4 0.9259259259259258%
172+Nat 17 0.9259259259259258%
173+
174+
175+ Checking that the last result is indeed a distribution:
176+┌ ┐
177+│ 1.0 │
178+└ ┘
179+
180+ Probability of grass being wet:
181+┌ ┐
182+│ 0.44838 │
183+└ ┘
184+
185+ Probability of rain:
186+┌ ┐
187+│ 0.19999999999999998 │
188+└ ┘
189+λ>
190+```