0 | module Control.Monad.Distribution
 1 |
 2 | import Data.Vect
 3 | import Data.Vect.Quantifiers
 4 | import Control.Monad.Identity
 5 | import System.Random
 6 |
 7 | import Data.Num
 8 | import Misc
 9 |
10 | ||| Convex combination of a finite set of types, a point in a simplex △^(i-1)
11 | ||| i=2 -> △¹ -> line segment
12 | ||| i=3 -> △² -> triangle
13 | ||| ...
14 | ||| Probabilities are here represented as logits
15 | ||| Since this is used in `Data.Container.Products.ConvexComb`, we cannot use
16 | ||| `Tensor` here
17 | public export
18 | data Dist : (i : Nat) -> Type where
19 |   ||| Probabilities are represented as logits
20 |   MkDist : Vect i Double -> Dist i
21 |
22 | public export
23 | toVect : Dist i -> Vect i Double
24 | toVect (MkDist xs) = xs
25 |
26 | ||| Logit representation of the uniform distribution
27 | public export
28 | uniform : {i : Nat} -> (isSucc : IsSucc i) => Dist i
29 | uniform = MkDist (replicate i 0)
30 |
31 | ||| Logit representation of dirac delta
32 | public export
33 | diracDelta : {i : Nat} -> IsSucc i =>
34 |   (j : Fin i) -> Dist i
35 | diracDelta @{ItIsSucc {n}} j = MkDist $ insertAt j 0 (replicate n minusInfinity)
36 |