0 | module Statistics.Probability
  1 |
  2 | import public Data.Double.Bounded
  3 |
  4 | import Data.Fin
  5 | import Data.Fin.Properties
  6 | import Data.Nat
  7 |
  8 | %default total
  9 |
 10 | --- Data definition ---
 11 |
 12 | public export
 13 | data Probability : Type where
 14 |   P : DoubleBetween 0 1 -> Probability
 15 |
 16 | --- Literals syntax ---
 17 |
 18 | public export %inline
 19 | fromDouble : (x : Double) -> (0 _ : So $ 0 <= x && x <= 1) => Probability
 20 | fromDouble x @{bds} = P $ fromDouble x @{fst $ soAnd bds} @{snd $ soAnd bds}
 21 |
 22 | public export %inline
 23 | fromInteger : (n : Integer) -> (0 _ : Either (n = 0) (n = 1)) => Probability
 24 | fromInteger n = fromDouble (cast n) @{believe_me Oh}
 25 |
 26 | --- Conversions ---
 27 |
 28 | public export %inline
 29 | Cast Probability Double where
 30 |   cast $ P x = x.asDouble
 31 |
 32 | public export %inline
 33 | Cast Probability (DoubleBetween 0 1) where
 34 |   cast $ P x = x
 35 |
 36 | public export %inline
 37 | Cast (DoubleBetween 0 1) Probability where
 38 |   cast = P
 39 |
 40 | public export %inline
 41 | (.asDouble) : Probability -> Double
 42 | (.asDouble) = cast
 43 |
 44 | public export %inline
 45 | (.value) : Probability -> DoubleBetween 0 1
 46 | (.value) = cast
 47 |
 48 | public export
 49 | maybeP : Double -> Maybe Probability
 50 | maybeP = map P . maybeBoundedDouble
 51 |
 52 | namespace FromDoubles
 53 |
 54 |   export
 55 |   (/) : (num, den : Double) -> (0 _ : So $ 1 < num && num <= den) => Probability
 56 |   num / den = fromDouble (num / den) @{believe_me Oh}
 57 |
 58 | export
 59 | ratio : (num, den : Nat) -> (0 _ : num `LTE` den) => (0 _ : IsSucc den) => Probability
 60 | ratio num den = (cast num / cast den) @{believe_me Oh}
 61 |
 62 | export
 63 | successesRatio : {den : Nat} -> (num : Fin $ S den) -> (0 _ : IsSucc den) => Probability
 64 | successesRatio num = do
 65 |   let LTESucc _ = elemSmallerThanBound num
 66 |   ratio (finToNat num) den
 67 |
 68 | public export
 69 | (.percent) : DoubleBetween 0 100 -> Probability
 70 | x.percent = P $ x / 100
 71 |
 72 | --- Composition operations ---
 73 |
 74 | public export
 75 | (*) : Probability -> Probability -> Probability
 76 | P x * P y = P $ x * y
 77 |
 78 | public export
 79 | Semigroup Probability where
 80 |   (<+>) = (*)
 81 |
 82 | public export
 83 | Monoid Probability where
 84 |   neutral = P 1
 85 |
 86 | public export
 87 | (/) : Probability -> DoubleBetween 1 (1/0) -> Probability
 88 | P x / y = P $ x / y
 89 |
 90 | public export %inline
 91 | inv : Probability -> Probability
 92 | inv $ P x = P $ 1 - x
 93 |
 94 | public export %inline
 95 | (.inv) : Probability -> Probability
 96 | (.inv) = inv
 97 |
 98 | --- Comparison operations ---
 99 |
100 | public export %inline
101 | Eq Probability where
102 |   P x == P y = x == y
103 |
104 | public export %inline
105 | Ord Probability where
106 |   compare (P x) (P y) = compare x y
107 |
108 | --- Printing ---
109 |
110 | export
111 | Show Probability where
112 |   show $ P x = show x
113 |