git.iko.soy/laop
on alternative help sign in
laop/app/Examples.hs
185 lines 4.6 kB history raw
1{-# LANGUAGE GADTs #-}
2{-# LANGUAGE DeriveGeneric #-}
3{-# LANGUAGE FlexibleContexts #-}
4{-# LANGUAGE TypeOperators #-}
5{-# LANGUAGE TypeApplications #-}
6{-# LANGUAGE DataKinds #-}
8module Examples
9 ( exec
10 )
11 where
13import LAoP.Matrix.Type
14import qualified LAoP.Relation as R
15import LAoP.Utils
16import LAoP.Dist
17import GHC.TypeLits
18import Data.Coerce
19import qualified GHC.Generics as G
20import Prelude hiding (id, (.))
22-- Monty Hall Problem
23data Outcome = Win | Lose
24 deriving (Bounded, Enum, Eq, Show, G.Generic)
26switch :: Outcome -> Outcome
27switch Win = Lose
28switch Lose = Win
30firstChoice :: Matrix Double () Outcome
31firstChoice = colL [1/3, 2/3]
33secondChoice :: Matrix Double Outcome Outcome
34secondChoice = fromF switch
36-- Dice sum
38type SS = Natural 1 6 -- Sample Space
40sumSS :: SS -> SS -> Natural 2 12
41sumSS = coerceNat (+)
43sumSSM = fromF (uncurry sumSS)
45condition :: (Int, Int) -> Int -> Int
46condition (fst, snd) thrd = if fst == snd
47 then fst * 3
48 else fst + snd + thrd
50conditionSS :: (SS, SS) -> SS -> Natural 3 18
51conditionSS = coerceNat2 condition
53conditionalThrows = fromF (uncurry conditionSS) . kr (kr die die) die
55die :: Matrix Double () SS
56die = colL $ map (const (1/6)) [nat @1 @6 1 .. nat 6]
58-- Sprinkler
59data G = Dry | Wet
60 deriving (Bounded, Enum, Eq, Show, G.Generic)
62data S = Off | On
63 deriving (Bounded, Enum, Eq, Show, G.Generic)
65data R = No | Yes
66 deriving (Bounded, Enum, Eq, Show, G.Generic)
68rain :: Matrix Double () R
69rain = matrixBuilder gen
70 where
71 gen (_, No) = 0.8
72 gen (_, Yes) = 0.2
74sprinkler :: Matrix Double R S
75sprinkler = matrixBuilder gen
76 where
77 gen (No, Off) = 0.6
78 gen (No, On) = 0.4
79 gen (Yes, Off) = 0.99
80 gen (Yes, On) = 0.01
82grass :: Matrix Double (S, R) G
83grass = matrixBuilder gen
84 where
85 gen ((Off, No), Dry) = 1
86 gen ((Off, Yes), Dry) = 0.2
87 gen ((On, No), Dry) = 0.1
88 gen ((On, Yes), Dry) = 0.01
89 gen ((Off, No), Wet) = 0
90 gen ((Off, Yes), Wet) = 0.8
91 gen ((On, No), Wet) = 0.9
92 gen ((On, Yes), Wet) = 0.99
94tag f = kr f id
96state g s r = tag g . tag s . r
98grass_wet :: Matrix Double () (G, (S, R)) -> Matrix Double One One
99grass_wet state = rowL [0,1] . fstM . state
101rainning :: Matrix Double (G, (S, R)) One
102rainning = rowL [0,1] . sndM . sndM
104-- Alcuin Puzzle
106data Being = Farmer | Fox | Goose | Beans
107 deriving (Bounded, Enum, Eq, Show, G.Generic)
109data Bank = LeftB | RightB
110 deriving (Bounded, Enum, Eq, Show, G.Generic)
112eats :: Being -> Being -> Bool
113eats Fox Goose = True
114eats Goose Beans = True
115eats _ _ = False
117eatsR :: R.Relation Being Being
118eatsR = R.toRel eats
120cross :: Bank -> Bank
121cross LeftB = RightB
122cross RightB = LeftB
124crossR :: R.Relation Bank Bank
125crossR = R.fromF cross
127-- | Initial state, everyone in the left bank
128locationLeft :: Being -> Bank
129locationLeft _ = LeftB
131locationLeftR :: R.Relation Being Bank
132locationLeftR = R.fromF locationLeft
134-- | Initial state, everyone in the right bank
135locationRight :: Being -> Bank
136locationRight _ = RightB
138locationRightR :: R.Relation Being Bank
139locationRightR = R.fromF locationRight
141-- Properties
143-- Being at the same bank
144sameBank :: R.Relation Being Bank -> R.Relation Being Being
145sameBank = R.ker
147-- Risk of somebody eating somebody else
148canEat :: R.Relation Being Bank -> R.Relation Being Being
149canEat w = sameBank w `R.intersection` eatsR
151-- "Starvation" property.
152inv :: R.Relation Being Bank -> Bool
153inv w = (w `R.comp` canEat w) `R.sse` (w `R.comp` farmer)
154 where
155 farmer :: R.Relation Being Being
156 farmer = R.fromF (const Farmer)
158-- Arbitrary state
159bankState :: Being -> Bank -> Bool
160bankState Farmer LeftB = True
161bankState Fox LeftB = True
162bankState Goose RightB = True
163bankState Beans RightB = True
164bankState _ _ = False
166bankStateR :: R.Relation Being Bank
167bankStateR = R.toRel bankState
169-- Main
170exec :: IO ()
171exec = do
172 putStrLn "Monty Hall Problem solution:"
173 prettyPrint (secondChoice . firstChoice)
174 putStrLn "\n Sum of dices probability:"
175 prettyPrint (sumSSM . kr die die)
176 putStrLn "\n Conditional dice throw:"
177 prettyPrint conditionalThrows
178 putStrLn "\n Checking that the last result is indeed a distribution: "
179 prettyPrint (bang . sumSSM . kr die die)
180 putStrLn "\n Probability of grass being wet:"
181 prettyPrint (grass_wet (state grass sprinkler rain))
182 putStrLn "\n Probability of rain:"
183 prettyPrint (rainning . state grass sprinkler rain)
184 putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
185 print (inv bankStateR)