Strongly Typed Tracing of Probabilistic Programs (cancelled, alas)
A commonly encountered concept in probabilistic programming literature is that of a trace, which is a record of all the random variables sampled during the program execution. Traces serve two roles, namely providing observed values for some of the variables on which to perform conditioning and facilitating implementations of certain inference algorithms. Typical examples of such inference algorithms are importance sampling, where a guide program with a trace matching the original program is provided as a proposal distribution, and MCMC where a part of the trace is updated at each iteration.
In this work we propose a method for constructing traces in PPLs in a statically typed fashion using lenses. Our approach statically ensures absence of certain bugs, such as misspelling a name of a random variable, and can be used to statically enforce certain properties of the program, such as the restriction of having a fixed number of random variables of fixed types, used in Stan programs. We focus on a situation where the user provides explicit names for the random variables. This is in contrast to the situation where the random variables are not explicitly given unique names and these have to be assigned automatically using a heuristic, such as in the work of Wingate et al. (2011).