record Traced : (Type -> Type) -> Type -> Type A tracing monad where only a subset of random choices are traced.
The random choices that are not to be traced should be lifted from the transformed monad.
Totality: total
Visibility: public export
Constructor: MkTraced : Weighted (FreeSampler Identity) a -> m (Trace a) -> Traced m a
Projections:
.model : Traced m a -> Weighted (FreeSampler Identity) a.traceDist : Traced m a -> m (Trace a)
Hints:
Monad m => Applicative (Traced m)Monad m => Functor (Traced m)Monad m => Monad (Traced m)MonadCond m => MonadCond (Traced m)MonadInfer m => MonadInfer (Traced m)MonadSample m => MonadSample (Traced m)
.model : Traced m a -> Weighted (FreeSampler Identity) a- Visibility: public export
model : Traced m a -> Weighted (FreeSampler Identity) a- Visibility: public export
.traceDist : Traced m a -> m (Trace a)- Visibility: public export
traceDist : Traced m a -> m (Trace a)- Visibility: public export
hoistT : (m x -> m x) -> Traced m a -> Traced m a- Visibility: export
marginal : Monad m => Traced m a -> m a Discard the trace and supporting infrastructure.
Visibility: exportmhStep : MonadSample m => Traced m a -> Traced m a A single step of the Trace Metropolis-Hastings algorithm.
Visibility: public exportmh : MonadSample m => (n : Nat) -> Traced m a -> m (Vect (S n) a) Full run of the Trace Metropolis-Hastings algorithm with a specified
number of steps.
Visibility: public export