A new kind of Continuation-like Monad?

Learn
#21

Mathematically, there is a strong connection between selection and probability: For any Borel measure, or any valuation on a locale, there is the notion of support of a measure, which is the complement of the largest open set with probability zero. This yields a monad morphism from the probability monad to the Hoare powerspace monad of closed sets, which is the monad of subspaces admitting continuous existential quantification. Thus it is not unreasonable to conjecture that if we restrict ourselves to measures with compact support, we could have a monad morphism from such a probability monad to J or G.

#22

Well, I don’t think the original idea works, but here we go.

newtype Stream m a = Stream (m (StreamF m a))
data StreamF m a = a :< Stream m a
newtype M m a = M ((a -> Stream m Double) -> Stream m a)

m is intended to be an instance of something like StatefulGen or MonadRandom. With this, I could generate some as, generate streams of probabilities from the continuation for each a, and then pull values from the streams using some sort Metropolis-Hastings variant to generate a stream of as. At least, that was the general idea. It couldn’t support score :: Log Double -> M m (), which is how I ended up looking at forall x. (a -> Stream m (Log Double, x)) -> Stream m (Log Double, x). There isn’t any difference between that and forall x. (a -> Stream (WriterT (Log Double) m) x) -> Stream (WriterT (Log Double) m) x. Codensity doesn’t use the Monad instance of whatever it transforms anyway.

I think you might have been expecting me to be looking for the Giry monad, and I do think that there should at least be a monad morphism from whatever I come up with to the Giry monad. I was just playing type tetris and seeing what happens.

#23

There are some problems with this, which you want to avoid for probabilistic programming: The mathematical Giry monad is affine and commutative, and using StateT anywhere destroys at least the affine property. But we’re reeling off topic here and should split the probabilistic stuff into a separate thread. Only so much: Have a look at Sam Staton’s LazyPPL library.

Questions that are relevant to @viercc and @IncredibleHannes as well:

  1. The original selection monad J is affine and almost commutative in the sense that the selected elements may differ, but stem from the same search space described by the selector. Does the same hold true for the codensity monad G?
  2. There is a theorem characterizing the monad morphisms into the continuation monad: Monad morphisms T -> Cont r are in bijective correspondence with T-algebra structures on r. Since the continuation monad is the codensity monad of the functor Const r, it seems plausible that there exists a more general version of this theorem for the codensity monad. Maybe @ekmett knows something about this?
2 Likes