We explore the use of parameterized monads for ensuring additional properties of distributions constructed by probabilistic programs. As a specific example we demonstrate how to statically ensure that conditioning in probabilistic programs does not depend on random choices made during execution. This allows us to ensure safety of application of inference algorithms such as Sequential Monte Carlo. We believe there are more potential uses of parameterized monads for probabilistic programming, such as restricting the latent space or keeping track of data types used for conditioning.

Adam Scibior and Andrew D. Gordon

What do the laws of your parametrized monad look like?

Dist is a monad by itself with standard laws.

For CDist we basically have the standard laws with lifting where necessary:

(return x :: CDist a) >>= (f :: a -> Dist b) = Pure (f x)

(d :: CDist a) >>= (return :: a -> Dist a) = d

(m :: CDist a) >>= (f :: a -> Dist b) >>= (g :: b -> Dist c) = m >>= (\x -> f x >>= g)

Note that in the last law the type of the second bind changes from (CDist b -> (b -> Dist c) -> CDist c) to (Dist b -> (b -> Dist c) -> Dist c) going from left to right of “=”.