
  0 | module Control.Monad.Sample.Definition
  1 | 
  2 | import Data.Fin
  3 | 
  4 | import Data.Container.Base
  5 | import Data.Tensor
  6 | import Control.Monad.Distribution
  7 | 
  8 | ||| Interface for sampling from a distribution
  9 | ||| We require that there is at least one element in the distribution
 10 | ||| TODO add temperature as a implicit parameter with a defualt value of 1.0
 11 | public export
 12 | interface Monad m => MonadSample m where
 13 |   sample : {name : AxisName} -> {i : Nat} -> (isSucc : IsSucc i) =>
 14 |     Dist name i -> m (Fin i)
 15 | 
 16 | ||| Sampling as a costate on the container of distributions
 17 | public export
 18 | Sample : MonadSample m => {name : AxisName} -> {n : Nat} -> IsSucc n =>
 19 |   (m <!> Dist name n) =%> Scalar
 20 | Sample = toCostate sample
 21 |