In our view, one of the key contributions of the probabilistic programming language Church is a class of constructs, called exchangeable random primitives (or XRPs for short), that can be used to extend the language with stochastic primitives whose implementations use stateful computation.

Surprisingly, XRPs are not mentioned in the paper introducing the language and are buried in the original implementation, dubbed MIT-Church. Despite being reimplemented and generalized in several languages descending from Church, XRPs are poorly documented and, as a result, poorly understood.

XRPs are built from three components: a sampler, an unsampler, and a scorer. We give a rigorous definition for the samplers of XRPs, and give a representation theorem characterizing their essential form and conditional independence structure. A formalization like the one we provide could serve as part of a foundation for deriving a semantics for Church programs with XRPs. A formalization of all three components of XRPs — including the unsampler and scorer — would be necessary to prove the correctness of the MCMC Church algorithm in the presence of XRPs. We highlight some challenges associated with formalizing the scorer. (We also have some ideas for circumventing these obstacles that do not appear in the paper but that we would be happy to discuss.) We are also looking forward to discussing semantic questions surrounding XRPs, especially those involving purity and referential transparency, and would be interested to learn of other possible connections between XRPs and the PL theory literature.