@@ -0,0 +1,159 @@
1+{-# LANGUAGE DeriveGeneric #-}
2+{-# LANGUAGE FlexibleContexts #-}
3+{-# LANGUAGE TypeOperators #-}
4+{-# LANGUAGE TypeApplications #-}
5+{-# LANGUAGE DataKinds #-}
6+
7+module Examples
8+ ( exec
9+ )
10+ where
11+
12+import LAoP.Matrix.Type
13+import qualified LAoP.Relation as R
14+import LAoP.Utils
15+import LAoP.Dist
16+import GHC.TypeLits
17+import Data.Coerce
18+import GHC.Generics
19+import Control.Category hiding (id)
20+import Prelude hiding ((.))
21+
22+-- Monty Hall Problem
23+data Outcome = Win | Lose
24+ deriving (Bounded, Enum, Eq, Show, Generic)
25+
26+switch :: Outcome -> Outcome
27+switch Win = Lose
28+switch Lose = Win
29+
30+firstChoice :: Matrix Double () Outcome
31+firstChoice = col [1/3, 2/3]
32+
33+secondChoice :: Matrix Double Outcome Outcome
34+secondChoice = fromF' switch
35+
36+-- Dice sum
37+
38+type SS = Natural 1 6 -- Sample Space
39+
40+sumSS :: SS -> SS -> Natural 2 12
41+sumSS = coerceNat (+)
42+
43+sumSSM = fromF' (uncurry sumSS)
44+
45+condition :: (Int, Int) -> Int -> Int
46+condition (fst, snd) thrd = if fst == snd
47+ then fst * 3
48+ else fst + snd + thrd
49+
50+conditionSS :: (SS, SS) -> SS -> Natural 3 18
51+conditionSS = coerceNat2 condition
52+
53+conditionalThrows = fromF' (uncurry conditionSS) . khatri (khatri die die) die
54+
55+die :: Matrix Double () SS
56+die = col $ map (const (1/6)) [nat @1 @6 1 .. nat 6]
57+
58+-- Sprinkler
59+
60+rain :: Matrix Double () Bool
61+rain = col [0.8, 0.2]
62+
63+sprinkler :: Matrix Double Bool Bool
64+sprinkler = fromLists [[0.6, 0.99], [0.4, 0.01]]
65+
66+grass :: Matrix Double (Bool, Bool) Bool
67+grass = fromLists [[1, 0.2, 0.1, 0.01], [0, 0.8, 0.9, 0.99]]
68+
69+state :: Matrix Double () (Bool, (Bool, Bool))
70+state = khatri grass identity . khatri sprinkler identity . rain
71+
72+grass_wet :: Matrix Double (Bool, (Bool, Bool)) One
73+grass_wet = row [0,1] . kp1
74+
75+rainning :: Matrix Double (Bool, (Bool, Bool)) One
76+rainning = row [0,1] . kp2 . kp2
77+
78+-- Alcuin Puzzle
79+
80+data Being = Farmer | Fox | Goose | Beans
81+ deriving (Bounded, Enum, Eq, Show, Generic)
82+
83+data Bank = LeftB | RightB
84+ deriving (Bounded, Enum, Eq, Show, Generic)
85+
86+eats :: Being -> Being -> Bool
87+eats Fox Goose = True
88+eats Goose Beans = True
89+eats _ _ = False
90+
91+eatsR :: R.Relation Being Being
92+eatsR = R.toRel eats
93+
94+cross :: Bank -> Bank
95+cross LeftB = RightB
96+cross RightB = LeftB
97+
98+crossR :: R.Relation Bank Bank
99+crossR = R.fromF' cross
100+
101+-- | Initial state, everyone in the left bank
102+locationLeft :: Being -> Bank
103+locationLeft _ = LeftB
104+
105+locationLeftR :: R.Relation Being Bank
106+locationLeftR = R.fromF' locationLeft
107+
108+-- | Initial state, everyone in the right bank
109+locationRight :: Being -> Bank
110+locationRight _ = RightB
111+
112+locationRightR :: R.Relation Being Bank
113+locationRightR = R.fromF' locationRight
114+
115+-- Properties
116+
117+-- Being at the same bank
118+sameBank :: R.Relation Being Bank -> R.Relation Being Being
119+sameBank = R.ker
120+
121+-- Risk of somebody eating somebody else
122+canEat :: R.Relation Being Bank -> R.Relation Being Being
123+canEat w = sameBank w `R.intersection` eatsR
124+
125+-- "Starvation" property.
126+inv :: R.Relation Being Bank -> Bool
127+inv w = (w `R.comp` canEat w) `R.sse` (w `R.comp` farmer)
128+ where
129+ farmer :: R.Relation Being Being
130+ farmer = R.fromF' (const Farmer)
131+
132+-- Arbitrary state
133+bankState :: Being -> Bank -> Bool
134+bankState Farmer LeftB = True
135+bankState Fox LeftB = True
136+bankState Goose RightB = True
137+bankState Beans RightB = True
138+bankState _ _ = False
139+
140+bankStateR :: R.Relation Being Bank
141+bankStateR = R.toRel bankState
142+
143+-- Main
144+exec :: IO ()
145+exec = do
146+ putStrLn "Monty Hall Problem solution:"
147+ prettyPrint (secondChoice . firstChoice)
148+ putStrLn "\n Sum of dices probability:"
149+ prettyPrint (sumSSM `comp` khatri die die)
150+ putStrLn "\n Conditional dice throw:"
151+ prettyPrint conditionalThrows
152+ putStrLn "\n Checking that the last result is indeed a distribution: "
153+ prettyPrint (bang . sumSSM . khatri die die)
154+ putStrLn "\n Probability of grass being wet:"
155+ prettyPrint (grass_wet . state)
156+ putStrLn "\n Probability of rain:"
157+ prettyPrint (rainning . state)
158+ putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
159+ print (inv bankStateR)