# Affine Monads and Lazy Structures for Bayesian Programming

Swaraj Dash  ,  Younesse Kaddar  ,  Hugo Paquet  and  Sam Staton  Univ. Oxford

(2023)

###### Abstract.

We show that streams and lazy data structures are a natural idiom for
programming with infinite-dimensional Bayesian methods such as Poisson
processes, Gaussian processes, jump processes, Dirichlet processes, and Beta
processes. The crucial semantic idea, inspired by developments in synthetic
probability theory, is to work with two separate monads: an affine monad of
probability, which supports laziness, and a commutative, non-affine monad of
measures, which does not. (Affine means that $T(1)\cong 1$.) We show that the
separation is important from a decidability perspective, and that the recent
model of quasi-Borel spaces supports these two monads.

To perform Bayesian inference with these examples, we introduce new inference
methods that are specially adapted to laziness; they are proven correct by
reference to the Metropolis-Hastings-Green method. Our theoretical development
is implemented as a Haskell library, LazyPPL.

††copyright: rightsretained††doi: 10.1145/3571239††journalyear:
2023††submissionid: popl23main-p324-p††journal: PACMPL††journalvolume:
7††journalnumber: POPL††publicationmonth: 1

##  1\. Introduction

Bayesian statistical models often naturally involve infinite-dimensional
spaces, and in this paper we show that these can be dealt with
programmatically using lazy structures. To show this, we provide a monadic
metalanguage for probabilistic programming that admits streams and other lazy
data structures (§2). The general key point is that an ‘affine’ monad can
support lazy programming, but a non-affine one cannot (see §1.3 and Theorems
2.1 and 2.2). For probabilistic programming, we thus consider two monads: an
affine monad of probability, and a non-affine monad of measures. We
demonstrate the expressive compositional power of this through a wealth of
examples (§1.2, §3, §4; [18]). We show that these are feasible by giving new
Metropolis-Hastings inference algorithms (§1.4, §6, §7) that work in a lazy
setting. Our development is motivated by new compositional methods in
categorical measure theory, such as quasi-Borel spaces: in Section 5 we give a
new formulation of this together with an implementation as a Haskell library,
LazyPPL [18].

###  1.1. Monte Carlo methods, Bayesian models, and unnormalized measures

It is often said that Monte Carlo methods are the reason for the explosion in
practical Bayesian statistics over the past 30 years (e.g. [26, §1.1], [27,
§1.4]). One account of Monte Carlo methods is that they are methods for
sampling from a probability distribution that is specified as an
_unnormalized_ measure, that is, a measure that is only specified up to an
unknown normalizing constant (e.g. [26, 79]). This matches the three primitive
aspects of Bayesian statistics, which are:

  * •

prior — a probability measure;

  * •

likelihood — often expressed by a density, or weight, contributing to the
unnormalized aspect of the measure;

  * •

posterior — a probability measure that is proportional to the product of the
likelihood and the prior, which is what the Monte Carlo method provides
samples from.

Our aim here is to explore the role of laziness in building and composing
these measures. Our motivation comes from two directions: practical and
theoretical.

On the practical side, probabilistic programming languages for Bayesian
modelling (such as Bugs [49], Church [29], Stan [10] and others) can often be
regarded as programming languages describing unnormalized measures, that are
endowed with efficient Monte Carlo samplers. Many focus on finite dimensional
models, but some allow unbounded dimension, notably Church, which is a key
starting point for our work. (See §8 for a fuller discussion of prior work.)

On the theoretical side, researchers have recently proposed categorical or
synthetic accounts of probability theory [12, 21] and measure theory [43, 70,
34], with the aim of developing compositional structures based on commutative
and affine monads and monoidal categories. There are various aims in that
work, some axiomatic, and some seeking to sidestep cumbersome issues with
measure theory, such as the absence of function spaces and of a strong monad
of measures (see §5, where we treat this). In this way, probabilistic
programming can be viewed as a _practical measure theory_ , with
compositionality built in, and where types are spaces, and programs are
suitably good measures on the spaces. By exploring fully expressive
probabilistic programming languages, we are exploring the abstract and higher-
order spaces of synthetic measure theory.

###  1.2. Practical illustration: the Poisson process

To illustrate further on the practical side, we briefly consider a ‘non-
parametric’ model now: the one-dimensional homogenous Poisson point process.
This is a random countable collection of points on the positive real line,
such that within any finite interval $[a,b]$ the expected number of points is
proportional to $(b-a)$, and the number of points in disjoint regions is
independent. Some draws from a Poisson point process are shown in Figure 1
(a). A Poisson point process is easy to define using laziness, and we flesh
out this definition in Section 3.1.

Of course, the pictures in Figure 1 (a) each show a finite number of points,
but this is because we have constrained the viewport to a finite window. In
practice we may want to use the point process as part of a larger model, and
in Section 3.2 we use it as part of a regression problem. Then it is unclear
where to truncate it to an arbitrary viewport in advance, and, as we
demonstrate, this can break the compositionality. This is often the case in
statistical models, as in other areas of programming: if we just focus on
running whole programs, we lose perspective of the conceptual and practical
building blocks. We illustrate this further with other examples of non-
parametric processes including Dirichlet process clustering (§3.3) and
Gaussian process regression (§4.1).

###  1.3. Theoretical aspects: affine monoidal structure and synthetic spaces

To illustrate the theoretical side, we recall that in the categorical
foundations of measure theory, a morphism $X\to I$ into the monoidal unit
describes a parameterized measure on the one-point space. If we focus on
normalized probability measures, there should be exactly one measure on the
one point space. So in the normalized setting, $I$ should be a terminal
object, in other words, we are working with an affine monoidal category (e.g.
[12, 21, 38, 15, 71, 22]). This is shown diagrammatically in Figure 1 (b), and

Figure 1.  (a) Four samples from a 1D Poisson point process with rate $1$,
with viewport restricted to $[0,4]$. (b) The law for affine monoidal
categories in string diagram form. (c) Visualizing dataflow in a lazy infinite
process.

we can regard the diagram as a dataflow diagram. To see where laziness comes
in, we regard the Poisson point process again, now as a dataflow diagram (Fig.
1 (c)). The infinite process is on the left, and the cloud represents the
plotting routine, or whatever happens next; intuitively, those morphisms on
the left that are not used in what follows need never be inspected, and in
that case the process can be truncated via Fig. 1 (b). Thus, affine monoidal
categories are related to laziness.

As is well known, we can program with monoidal categories using monads (e.g.
§5.1). The key conceptual contribution of this paper is the observation that
we should program with two separate monads: an affine monad Prob of
probability measures, allowing laziness, and a non-affine monad Meas of
unnormalized measures, allowing the Bayesian Monte Carlo methods (§1.1). This
is the basis of our metalanguage in Section 2. Theorem 2.1 demonstrates the
way that lazy structures work with probability, in terms of infinite streams
of samples. Proposition 2.2 shows that, once we have this functionality, we
have to separate Prob and Meas to avoid deciding the halting problem.

When we regard types in probabilistic programming languages as spaces of
synthetic measure theory, we see spaces from non-parametrics, such as function
spaces and infinite lists, behaving intuitively and straightforwardly, even
though they can be subtle from the traditional measure-theoretic approach. We
give a semantic model of our metalanguage in quasi-Borel spaces ( Section 5),
but a novelty here is to fix the basic probability space to a space of lazy
rose trees (§6.2). This lends itself to an implementation in the form of our
Haskell library LazyPPL [18].

###  1.4. New Metropolis-Hastings-based inference algorithms

To experiment with these examples involving laziness, we introduce new
inference algorithms that build on earlier inference methods for probabilistic
programming (e.g. [85]). These take as an argument a program describing an
unnormalized measure, and produce a stream of samples as output.

Traditional uses of Monte Carlo algorithms often assume a finite-dimensional
state space; sometimes they can adapt to changing dimensions (e.g. [32]). But
in a purely lazy setting, the distributions are implicitly infinite-
dimensional, and indeed our basic probability space is the infinite
dimensional space of rose trees. To resolve this, we provide new
instantiations of the Metropolis-Hastings-Green algorithm, that do apply in
this setting, and which we have also implemented in Haskell [18].

  * •

Our main algorithm (§6) is purely lazy. It operates lazily over the entire
infinite-dimensional state space, mutating different parts at random.

  * •

Our other algorithms work by mixing kernels (§7). In particular, we are able
to implement roughly the algorithm of [85], adapted to this lazy setting, by
using Haskell internals (ghc-heap) to identify which dimensions are actually
being used in a given run of the program.

We can show that these algorithms are correct (via Theorems 6.2, 6.3, 7.1).
Generally speaking, general purpose algorithms such as these will not work as
efficiently as hand-crafted inference methods for specific scenarios.
Nonetheless, they are useful for prototyping the numerous examples we consider
in this paper to illustrate laziness and monads in probabilistic programming
(§3, §4).

##### Acknowledgements.

We have benefited from many helpful discussions, including with Victor
Blanchi, Reuben Cohn-Gordon, Cameron Freer, Ohad Kammar, Dan Roy, Adam
Ścibior, Matthijs Vákár, Frank Wood, Hongseok Yang, Mathieu Huot and other
colleagues in Oxford. Thanks also to anonymous reviewers. We also benefited
from presenting aspects of this work at various venues, including ACT,
AIPLANS, FSCD, LAFI, PROBPROG and an early version in taught courses in OPLSS
2019 and Oxford (BSPP 2020). Research supported by AFOSR award number
FA9550-21-1-0038; the ERC BLAST grant; and a Royal Society University Research
Fellowship.

##  2\. A monadic metalanguage for probability and measure

The idea of Monte Carlo based inference is that we define an unnormalized
measure, by weighting different random choices, and then Monte Carlo inference
provides samples from the normalized form of this measure.

${{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{\boxed{\begin{aligned}
&\text{\emph{Types: }
}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}},\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}}}}}\
\mathrel{{:}{:}=}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}RealNum}}}}}}~{}|~{}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small()}}}}~{}|~{}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}},{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}})}}}}~{}|~{}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}}}}}~{}|~{}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords3}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}Prob}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}~{}|~{}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}Meas}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}~{}|~{}\dots\\\
&\text{\emph{Terms:}
}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}},\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}}}}}\
\mathrel{{:}{:}=}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}}}}}~{}|~{}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small\textbackslash{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}}~{}|~{}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}}}}}~{}|~{}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}\textbraceright}}}}~{}|~{}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}}~{}|~{}\dots\\\
\ &\text{\emph{Typing judgement}
}(\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}})\text{\emph{:}}\\\
&\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
142.63959pt\hbox{$\displaystyle\penalty
1\phantom{\Gamma\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}}}-\phantom{\Gamma\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=445.76268pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}::{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}},\Gamma^{\prime}\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
26.27075pt\hbox{$\displaystyle\penalty
1\Gamma,\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}::{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}}}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=485.31975pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small\textbackslash{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}}}}}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}}}}}\quad\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=481.06973pt\hbox{}}}\hbox{\kern
33.70274pt\hbox{$\displaystyle\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}}}}}$}}}}\
\\\\[3.0pt] &\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 104.78763pt\hbox{$\displaystyle\penalty
1\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=491.06436pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}m}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}m}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}\quad\Gamma,\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}::{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}m}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}}}}}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=585.48112pt\hbox{\kern
3.00003pt$\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}m}}}}}}\in\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords3}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}Prob}}}}}},\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}Meas}}}}}}\\}$}}}\hbox{\kern
49.08066pt\hbox{$\displaystyle\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}\textbraceright{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}m}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}}}}}$}}}}\\\\[3.0pt]
&\emph{Typed constants:}\\\ &\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small(){\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}()}}}}\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small(,){\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}},{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}})}}}}\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}fst}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}},{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}){\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}snd}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}},{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}){\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}}}}}\\\
&\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small
0,1{\@listingGroup{ltx_lst_space}{ }}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}RealNum}}}}}}\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small\textasteriskcentered{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}RealNum}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}RealNum}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}RealNum}}}}}}\quad\dots\\\
&\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}sample}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords3}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}Prob}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}Meas}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}score}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}RealNum}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}Meas}}{\@listingGroup{ltx_lst_space}{
}}()}}}}\quad\end{aligned}}$ Figure 2. Summary of the types and terms of the
monadic metalanguage.

In this section, we encapsulate this in programming terms by using two monads,
describing normalized and unnormalized measures. To make this formal, we set
up an instance of Moggi’s monadic metalanguage ([52]) outlined in Figure 2. We
discuss the syntax now, with a first example in Section 2.1. We then provide a
basic equational theory (§2.2) and use it to show that the separation between
these monads is crucial for exploring lazy data structures (§2.3, Theorem 2.1
and Proposition 2.2). Throughout the section, we consider simple extensions of
the metalanguage that support lazy structures.

In the metalanguage, there is a distinguished type RealNum, thought of as the
real numbers, and there are two monads:

  * •

A probability monad Prob (in green font) so that (Prob a) intuitively contains
probability measures on a. We typically have stock probability measures, such
as uniform :: Prob RealNum and normal :: RealNum $\rightarrow\;$ RealNum
$\rightarrow\;$ Prob RealNum, but we do not need to postulate these at this
point.

  * •

A measures monad Meas (in red font), so that (Meas a) intuitively contains
unnormalized measures on a.

There are two key operations:

  * •

sample :: Prob a $\rightarrow\;$ Meas a, which allows us to regard a
probability measure as an unnormalized measure;

  * •

score :: RealNum $\rightarrow\;$ Meas (), which provides a measure with given
weight on a single point; this is an unnormalized measure unless the weight is
$1$.

The score operation is often used with a probability density, to incorporate
the likelihood in a Bayesian scenario. One can use all kinds of distributions
for observations, using their densities. For example, to incorporate a
Bayesian observation of data point x from a normal distribution with mean
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mu$ and
standard deviation
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\sigma$,
we write score (normalPdf
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mu$
$\;\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\sigma$
x), where
$({\mathtt{normalPdf}\;\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mu\;\sigma\;\mathtt{x}})=e^{-({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathtt{x}}-{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mu})^{2}/(2{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\sigma})^{2}}/({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\sigma}\sqrt{2\pi})$.
We use a Haskell notation for the metalanguage; we have implemented the
metalanguage in Haskell (see §5.7, §6, [18]) and so all the examples can be
run.

###  2.1. First example: Bayesian linear regression

We illustrate the metalanguage with a simple 1-dimensional Bayesian regression
model. (See §3 for further illustrations.) The problem of regression is that
we have some data points observed, and we want to know which function
generated those points. Bayesian regression does not produce one single ‘line
of best fit’, but rather a probability distribution over the functions that
might have generated the points. We start with a fairly uninformative prior
distribution over linear functions, incorporate the likelihood of the
observations, and produce a posterior by Monte Carlo simulation.

In statistical notation, we might define the prior by writing

$a\sim\mathcal{N}\mathit{ormal}(0,3)\qquad
b\sim\mathcal{N}\mathit{ormal}(0,3)\qquad f(x)=ax+b$

Here, the slope a and intercept b are both drawn from normal distributions.

In the metalanguage (extended with mild syntactic sugar) we can write

⬇

linear :: Prob (RealNum $\rightarrow\;$ RealNum)

linear = do { a $\leftarrow\;$ normal 0 3 ; b $\leftarrow\;$ normal 0 3 ; let
f x = a*x + b ; return f }

We do not want to assume that the data points are exactly colinear, and so we
do not want observe the likelihood of the data points being exactly f x.
Rather, we use a likelihood for the points being normally distributed around f
x, for some small standard deviation $\sigma$. The inference problem might be
written in statistical notation as:

$f\sim\mathcal{L}inear\qquad
y_{i}\sim\mathcal{N}\mathit{ormal}(f(x_{i}),\sigma)\qquad\text{What is
$P(f|(y_{i}=d_{i})_{i})$?}$

where $d_{i}$ are the observed values at $x_{i}$. To this end, we define a
general purpose function regress, which takes a standard deviation $\sigma$, a
prior over the function space prior, and a list of (x,y) observations dataset.
For convenience, we add a type of lists, and routines for operating over
lists.

⬇

regress :: RealNum $\rightarrow\;$ Prob (a $\rightarrow\;$ RealNum)
$\rightarrow\;$ [(a,RealNum)] $\rightarrow\;$ Meas (a $\rightarrow\;$ RealNum)

regress
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\sigma$
prior dataset =

do {f $\leftarrow\;$ sample prior; forM_ dataset (\\(x,d) $\rightarrow\;$
score (normalPdf (f x)
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\sigma$
d)); return f}

Figure 3. Bayesian regression in LazyPPL for the data set indicated by the
dots. We illustrate the posteriors starting from three different priors on the
function space. From left to right: (a) linear (§2.1), (b) piecewise linear
(§3.2), and (c) Gaussian processes (see §4.1).

So linear regression in particular is achieved by performing Monte Carlo
inference on the program (regress 0.1 linear dataset), see Figure 3 (a). We
discuss inference in Section 6.

###  2.2. Equational reasoning

To begin to look more formally at the meaning of the programming syntax, we
now consider equations between programs. We give a denotational model in
Section 5. One could also give an operational semantics, and we give an
implementation in Section 5.7. Either way is slightly technical, so for now we
work axiomatically, by listing some equations that we intend to hold. The idea
is that the equations are sound, in that any programs that are derivably equal
should be equal in any good denotational interpretation, or observationally
equivalent for an operational semantics.

The equational theory is not intended to be a complete system, nor is it
intended as a definitional semantics by rewriting, although the equations here
are useful in practice, for example as compiler transformations.

We begin with the standard equational theory of the monadic metalanguage
(Figure 4), which is sound for strong monads on a cartesian closed category.
Our interface has two monads, and we now state some additional equations that
they should satisfy.

First, we impose that sample :: Prob a $\rightarrow\;$ Meas a should be a
monad morphism, i.e.:

(1) sample (return t)
${\displaystyle=\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}Meas}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}$
sample (do {x $\leftarrow\;$ p ; q})
${\displaystyle=\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}sample}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}sample}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}q}}\textbraceright{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}Meas}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}b}}}}}}$

for t :: a, p :: Prob a, q :: Prob b.

The measures monad should satisfy commutativity (e.g. [41]): for mx :: Meas a
and my :: Meas a,

(2)
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}mx}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}y}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}my}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}},{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}y}})\textbraceright}}}}\quad=\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}y}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}my}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}mx}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}},{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}y}})\textbraceright}}}}$

where
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}}}}}\not\in\mathrm{freevars}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}my}}}}}})$,
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}y}}}}}}\not\in\mathrm{freevars}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}mx}}}}}})$.
The probability monad should satisfy commutativity, and also affinity (e.g.
[42, 37]):

(3) ${{{\text{if
\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}mx}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords3}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}Prob}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}},
then:}\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}mx}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}()\textbraceright}}}}\qquad=\qquad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}()}}}}$

Finally, scores should combine multiplicatively, and a score of $0$ should
trivialize:

(4)
${{{{\displaystyle\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}score}}{\@listingGroup{ltx_lst_space}{
}}1}}}}\ =\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}(){\@listingGroup{ltx_lst_space}{ }}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}Meas}}{\@listingGroup{ltx_lst_space}{
}}()}}}}\qquad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}score}}{\@listingGroup{ltx_lst_space}{
}}0{\@listingGroup{ltx_lst_space}{ }};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}mx}}\textbraceright}}}}\
=\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}score}}{\@listingGroup{ltx_lst_space}{
}}0{\@listingGroup{ltx_lst_space}{ }};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}my}}\textbraceright{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}Meas}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}$
${{\displaystyle\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}score}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}r}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}score}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}s}}\textbraceright}}}}\quad=\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}score}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}r}}{\@listingGroup{ltx_lst_space}{
}}\textasteriskcentered{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}s}}){\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}Meas}}{\@listingGroup{ltx_lst_space}{
}}()}}}}$

for r,s :: RealNum and mx,my :: Meas a.

${{{{{{{{{{{{{{{{{{{{{{{{{{{\boxed{\begin{aligned} &\text{\emph{Typed
equational theory:} we define a relation
$\Gamma\vdash{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}}}}}}{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small::{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}}$
over typed terms
$\Gamma\vdash{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}},\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}}}}}}{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small::{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}a}}}}}}}$.}\\\
&\text{Mostly the type and environment are clear from context; the exception
is the unit axiom:}\\\ &\ \text{If
}\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{ }}()}}}}\text{ then
}\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small(){\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{ }}()}}}}\\\
&\begin{array}[]{@{}ll}\text{Other
axioms:}&\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}y}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}s}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}\textbraceright{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}\textbraceright}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}s}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}y}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}\textbraceright\textbraceright}}}}\quad[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}}}}}\not\in\mathrm{fv}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}}}}})]\\\\[2.0pt]
&\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}\textbraceright}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}[{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}/{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}]}}}}\qquad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}\textbraceright}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}}\end{array}\\\
&\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}fst}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}},{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}})}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}}\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}snd}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}},{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}})}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}}}}}\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small({\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}fst}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}},{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}snd}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}})}}}}\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small(\textbackslash{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}){\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}[{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}/{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}]}}}}\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small(\textbackslash{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}))}}}}\end{aligned}}$
Figure 4. Basic equational theory of the monadic metalanguage. We give
additional equations in (1)–(5).

###  2.3. Affine probability monads, laziness, and iid sequences

We now show the connection between the affine monad law (3) and lazy data
structures. The reader might already glimpse a connection between (3) and
laziness, since the law says that if the result x of a program expression mx
is not used in what follows (left-hand side), then mx need not be considered
at all (right-hand side).

To formally investigate this with lazy data structures, we suppose that the
metalanguage is extended with types Stream a of streams, and standard accessor
methods such as

hd :: Stream a $\rightarrow\;$ a tl :: Stream a $\rightarrow\;$ Stream a (:)
:: a $\rightarrow\;$ Stream a $\rightarrow\;$ Stream a

together with syntactic sugar, and equations such as

(5)
${{{{{{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}hd}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}:{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}})}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}}}}}\qquad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}tl}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}:{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}})}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}}}}}\qquad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}hd}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}):({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}tl}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}})}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}}}}}$

We also suppose that we have a mechanism iid for generating ‘independent and
identically distributed’ infinite random sequences. This should satisfy the
following recursive equation:

⬇

iid :: Prob RealNum $\rightarrow\;$ Prob (Stream RealNum)

iid p = do { x $\leftarrow\;$ p ; xs $\leftarrow\;$ iid p ; return (x : xs) }

We emphasise that the equation is for now regarded as an equational
specification, not a recursive program definition with a given evaluation
strategy. Although the recursive call appears to make an infinite number of
random choices, we can deduce from the basic equational laws that it must be
treated lazily:

###### Theorem 2.1.

For any finite sequence i1$,\dots,$ in of distinct indices, the following
programs of type Prob (RealNum,...,RealNum) are equal:

  1. (1)

do {xs $\leftarrow\;$ iid p ; return (xs !! i1,$\dots$, xs !! in)}

  2. (2)

do {x1 $\leftarrow\;$ p ; $\dots$ ; xn $\leftarrow\;$ p ; return (x1 ,
$\dots$, xn)}

###### Proof notes.

For instance (and omitting do for brevity):

xs $\leftarrow\;$ iid p ; return (xs !! 2,xs !! 1) [iid equation, 3 times]
${\displaystyle=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{0}\;$}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{1}\;$}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{2}\;$}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}iid}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}(({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{0}$}}:{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{1}$}}:{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{2}$}}:{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}})!!2,({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{0}$}}:{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{1}$}}:{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{2}$}}:{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}})!!1)}}}}$
${\displaystyle=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{0}\;$}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{1}\;$}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{2}\;$}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}iid}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{2}$}},{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{1}$}})}}}}$
[(5)]
${\displaystyle=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{1}\;$}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{2}\;$}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{2}$}},{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{1}$}})}}}}$
[(3)]
${\displaystyle=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{1}\;$}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{2}\;$}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{1}$}},{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{2}$}})}}}}$
$\displaystyle\text{[\eqref{eqn:comm} and rename variables]}\qed$

To emphasise the connection with lazy structures, we make the following
remarks. Our equational theory has thus far not discussed ‘termination’,
however, in any reasonable semantics, program (2) in Theorem 2.1 would be
regarded as terminating. Thus program (1), being equal to (2), should also be
regarded as terminating. Thus the call to iid induces an unbounded stream of
results, despite terminating, which is the essence of laziness.

Using similar arguments, we can assume a more general primitive that generates
a stream of results by iterating a function b $\rightarrow\;$ Prob (a, b).
This is subject to the following equation:

⬇

unfold :: (b $\rightarrow\;$ Prob (a, b)) $\rightarrow\;$ b $\rightarrow\;$
Prob (Stream a)

unfold f y = do { (x, y’) $\leftarrow\;$ f y; xs $\leftarrow\;$ unfold f y’;
return (x : xs)}

We note that we could define iid by iid p = unfold (\_ $\rightarrow\;$ do {x
$\leftarrow\;$ p; return (x, ())}) ().

####  2.3.1. Discussion of problems with laziness in general measures monads

We do not ask that the general measures monad, Meas a, is affine, because then
the score construct would disappear. In practice, this means that we cannot
expect to construct lazy data structures using recursive definitions in the
Meas monad, as we now explain.

Suppose for a moment that we did have the equivalent of unfold and iid in the
Meas monad:

(6) unfoldM :: (b $\rightarrow\;$ Meas (a, b)) $\rightarrow\;$ b
$\rightarrow\;$ Meas (Stream a) iidM :: Meas RealNum $\rightarrow\;$ Meas
(Stream RealNum)

For instance, iidM m = do { x $\leftarrow\;$ m ; xs $\leftarrow\;$ iidM m ;
return (x : xs)}. Consider the program do { xs $\leftarrow\;$ iidM (do {score
2 ; return 42}) ; return (hd xs)} :: Meas RealNum.  We are unable to use the
equations of the monadic metalanguage to simplify this program, because we
cannot use (3), and the semantics is unclear. (Possible semantics include: the
program does not terminate, or, the program terminates with infinite score,
since $2^{n}\to\infty$ as $n\to\infty$.)

It is still possible to use lazy data structures when building unnormalized
measures: for instance we can write sample (iid p) :: Meas (Stream a) whenever
p :: Prob a. But we show now that implementing a general unfoldM and iidM such
that sample (iid p) = iidM (sample p) is impossible, whenever our equations
hold.

###### Proposition 2.2.

Suppose that there are terms unfoldM and iidM as in (6) such that we have iidM
(return t) = sample (iid (return t)). Then among the programs

${{{{{\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}}~{}|~{}\exists\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}r}}}}}},\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}}}}}\text{
such that
}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}t}}}}}}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}score}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}r}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}u}}\textbraceright{\@listingGroup{ltx_lst_space}{
}}::{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}Meas}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}RealNum}}}}}}\\}$

the score r is undecidable.

###### Proof.

Pick an arbitrary Turing machine $M$. We exhibit a program h such that we have
either h = score 0 ; return 0 if $M$ halts, and h = score 1 ; return 42
otherwise. Thus it is in general undecidable whether the score is $0$ or $1$.
To this end, write steps n if $M$ halts after simulating it for n steps.
Suppose we extend the metalanguage with this steps construction.

⬇

h :: Meas Integer

h = hd <$> (unfoldM (\n $\rightarrow\;$ do{ score (if (steps n) then 0 else
1); return (42,n+1) })) 0

(where (t <$> u) = do {x $\leftarrow\;$ u ; return (t x)}). Suppose that $M$
terminates at time $n$. Then, unrolling <$> and the recursive equation for
unfoldM, and simplifying using (1)–(5) and Fig. 4:

h
${{\displaystyle=\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}unfoldM}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{}{$\dots$}}{\@listingGroup{ltx_lst_space}{
}}){\@listingGroup{ltx_lst_space}{ }}0{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}hd}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}})\textbraceright}}}}\;=\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}unfoldM}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{}{$\dots$}}{\@listingGroup{ltx_lst_space}{
}}){\@listingGroup{ltx_lst_space}{ }}1{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}42\textbraceright}}}}$
${\displaystyle=\quad\dots\quad=\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}unfoldM}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{}{$\dots$}}{\@listingGroup{ltx_lst_space}{
}}){\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}n}}{\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}42\textbraceright}}}}$
${{\displaystyle=\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}score}}{\@listingGroup{ltx_lst_space}{
}}0{\@listingGroup{ltx_lst_space}{ }};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}unfoldM}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{}{$\dots$}}{\@listingGroup{ltx_lst_space}{
}}){\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}n}}+1){\@listingGroup{ltx_lst_space}{
}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}42\textbraceright}}}}\;=\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}score}}{\@listingGroup{ltx_lst_space}{
}}0{\@listingGroup{ltx_lst_space}{ }};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}0\textbraceright}}}}\text{.}$

On the other hand, if the machine $M$ does not halt, then h = hd <$> iidM
(return 42). By the assumption in the theorem, h = hd <$> sample (iid (return
42)), and so by (1) and (4), we have

h
${\displaystyle=\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}hd}}{\@listingGroup{ltx_lst_space}{
}}\textless{\@listingGroup{}{$\mbox{\textdollar}$}}\textgreater{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}sample}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}iid}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}42)){\@listingGroup{ltx_lst_space}{ }};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}(42{\@listingGroup{ltx_lst_space}{ }}:{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}){\@listingGroup{ltx_lst_space}{
}}\textbraceright}}}}$ [iid & (1)]
${\displaystyle=\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}sample}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}iid}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}42)){\@listingGroup{ltx_lst_space}{ }};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}42\textbraceright}}}}$ [<$> & (4)]
${{\displaystyle=\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}sample}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}xs}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}iid}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}42){\@listingGroup{ltx_lst_space}{ }};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}42\textbraceright)}}}}\;=\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}sample}}{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}42)}}}}$ [(1) & (3)]
${{\displaystyle=\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}42}}}}\;=\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}score}}{\@listingGroup{ltx_lst_space}{
}}1{\@listingGroup{ltx_lst_space}{ }};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}42\textbraceright}}}}$ [(1) & (4)]

If the score is undecidable, this means the system is not amenable to Monte
Carlo simulation, because the score is needed to know whether or not to reject
a run of the program. For the example in the proof of Proposition 2.2, a Monte
Carlo simulation would have to always reject if the machine $M$ terminates,
and always accept if the machine $M$ does not terminate, so it would have to
decide the Halting problem, which is absurd. There are other decidability
problems in probabilistic programming (e.g. [2, 36]), but this barrier occurs
even without any statisticial primitives.

In summary, we can program random lazy data structures using the affine Prob
monad and constructions like iid, and execution must treat them lazily
(Theorem 2.1). By contrast, we cannot hope to program lazy data structures
using the Meas directly, for decidability reasons (Proposition 2.2).
Nonetheless we can build random lazy data structures using the Prob monad, and
constructions such as iid, and then regard them as arbitrary measures using
sample :: Prob a $\rightarrow\;$ Meas a.

###  2.4. Comparison with prior work on synthetic measure theory

Previous work considered a synthetic measure theory based on a cartesian
closed category with countable sums and products and a commutative monad $M$
that is countably additive [43, 70]. We can then construct an affine submonad
$P\subseteq M$ as an equalizer, and an object of scalars $R=M(1)$. Any such
model is a model of the metalanguage in Sections 2.2:
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords3}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}Prob}}}}}}=P$,
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}Meas}}}}}}=M$,
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}RealNum}}}}}}=R$,
sample is the inclusion, and score is the identity function.

This connects to other axiomatizations too: for a model of synthetic measure
theory, the Kleisli category of $M$ is a CD/GS-category [12, 24, 76], and the
Kleisli category of $P$ is a Markov category [21, 23]. Infinite processes such
as iid have recently been studied in Markov categories [25], but not in the
unnormalized setting.

One difference between our metalanguage and synthetic measure theory is that
Meas, Prob and RealNum are given as explicit ingredients here; Prob is not
necessarily an equalizer and RealNum is not necessarily equal to Meas (). We
found it helpful to make these distinctions in practice. For instance, the
expression do {x $\leftarrow\;$ sample uniform ; score (f x)} :: Meas ()
intuitively corresponds to the RealNum that is the integral
${\int_{0}^{1}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}f}}}}}}(x)\,\mathrm{d}x$,
but for general f, this can only be calculated approximately, e.g. via Monte
Carlo simulation.

##  3\. Examples taking advantage of laziness

We now give examples of probabilistic programs with lazy data structures,
using the metalanguage from Section 2. We are able to run the programs by
using our implementation (LazyPPL, §5.7, [18]).

The examples show that laziness, and two separate monads Prob and Meas, allow
compositional programming; without this, we cannot use iid, and we have to
pass around truncation bounds.

###  3.1. Point processes as lazy streams of points

A random collection of points is called a _point process_. A first example of
an infinite point process is a _Poisson_ point process on the positive reals
(see also Figure 1 (a)). In statistical notation, we consider a sequence of
real random variables $x_{0},x_{1},\dots$ such that the gaps are exponentially
distributed:

$x_{0}\sim\mathcal{E}\mathit{xponential}(r)\qquad\quad(x_{i+1}-x_{i})\sim\mathcal{E}\mathit{xponential}(r)$

This can be defined in a minor extension of our metalanguage, by giving a
random stream 111Henceforth we use [a] instead of (Stream a), recalling that
Haskell lists include infinite lists.:

⬇

poissonPP :: RealNum $\rightarrow\;$ Prob [RealNum]

poissonPP rate = do { steps $\leftarrow\;$ iid (exponential rate) ; return
(scanl (+) 0 steps) }

This returns an infinite random stream, illustrated in Figure 1 (a). Although
this is simple, it becomes powerful when we compose with other models, as we
show in the following sections. (See also [19], for more on programming with
point processes.)

##### Comments on avoiding lazy data structures

Without using infinite lazy data types, we can only implement a truncated
Poisson point process, where an upper bound is specified:

⬇

poissonPPbounded :: RealNum $\rightarrow\;$ RealNum $\rightarrow\;$ RealNum
$\rightarrow\;$ Prob [RealNum]

poissonPPbounded rate lower upper = do

step $\leftarrow\;$ exponential rate

let x = lower + step

if x > upper then return []

else do {xs $\leftarrow\;$ poissonPPbounded rate x upper; return (x:xs)}

This truncated form is an obstacle to compositional modelling, because when
the Poisson point process is used as part of a more complex model, we will
have to calculate an upper bound and pass it around manually, as we will
discuss further in Section 3.2.

(As an aside, we mention that although the bounded program will always return
a finite list in practice, this relies on a mathematical argument: any
sequence of draws from an exponential distribution will almost surely go above
a given upper bound in a finite number of steps. This is no problem in a
general purpose programming language, but may prove subtle in, say, a
dependently typed language with termination guarantees.)

Of course, some truncation must happen at some point. In practice, in LazyPPL,
it happens at the top level, the plotting routine stops looking at the stream
beyond the viewport, and the laziness propagates from here.

###  3.2. Piecewise regression with lazy change points

We combine the Poisson Point Process (§3.1) with the linear regression model
(§2.1), to obtain _piecewise_ linear regression, where the prior is over
piecewise linear functions. We define a function that will splice together
different draws from a random function given a random sequence of change
points:

⬇

spliceProb :: Prob [RealNum] $\rightarrow\;$ Prob (RealNum $\rightarrow\;$
RealNum) $\rightarrow\;$ Prob (RealNum $\rightarrow\;$ RealNum)

spliceProb pp f = do {xs $\leftarrow\;$ pp ; fs $\leftarrow\;$ iid f ; return
$ splice xs fs }

Here we assume a basic deterministic function

⬇

splice :: [RealNum] $\rightarrow\;$ [RealNum $\rightarrow\;$ RealNum]
$\rightarrow\;$ (RealNum $\rightarrow\;$ RealNum)

which splices together a sequence of functions at the given change points. The
sequence of change points can be infinite, so the function can have an
infinite number of pieces. But this is no problem if our probability monad is
affine, and this can be handled lazily.

We can perform piecewise linear regression using a Poisson point process, for
example via

⬇

piecewiseLinear :: Prob (RealNum $\rightarrow\;$ RealNum)

piecewiseLinear = spliceProb (poissonPP 0.2) linear

and then regress 0.1 piecewiseLinear dataset, which gives Fig. 3 (b), using
the inference in §6.

##### Comments on avoiding lazy data structures.

Our piecewise linear model demonstrates why it is important to have separate
Prob and Meas monads. As we have explained in Section 2.3, it is impossible to
have a general iid on arbitrary measures, but it is fine on probability
measures. We have used iid twice in this model. It is part of spliceProb, and
so it is crucial to know that the prior f is a probability measure on
functions.

This piecewise linear regression can be implemented without infinite lazy
structures, by using poissonPPbounded and rewriting spliceProb to just sample
a bounded number of functions fs, depending on the length of xs. For this
first example, the bound can come from the chosen viewport, or data range,
which might not be hard to calculate, but in general, propagating this is not
compositional. For example, we can quickly rescale a random function on the
$x$-axis:

⬇

rescale :: Prob (RealNum $\rightarrow\;$ RealNum) $\rightarrow\;$ Prob
(RealNum $\rightarrow\;$ RealNum)

rescale p = do { f $\leftarrow\;$ p ; return (\x $\rightarrow\;$ f(2 * x)) }

We can then perform regression with regress 0.1 (rescale piecewiseLinear)
dataset. To do this without lazy structures, with explicit bounds, we would
also need to rescale the bounds by hand. So compositionality with explicit
bounds is impossible.

As an aside, we point out the beauty of higher-order probabilistic programming
for compositional model building: it is very easy to switch the Poisson
process for a different point process, or to use piecewise _constant_
regression, and so on (see the repository [18] for more examples).

###  3.3. Clustering using a lazily broken stick

For a set of data points, clustering is the problem of finding the most
appropriate partition into clusters. In non-parametric clustering, the number
of clusters is unknown and unbounded. As we demonstrate, this is closely
connected to laziness. The separation into two monads, Prob and Meas, is
crucial for a compositional specification in our metalanguage.

####  3.3.1. Stick-breaking

In _Bayesian_ clustering, one considers a prior distribution over possible
partitions of the data into clusters. This is usually described in terms of
stick-breaking, where the unit interval $[0,1]$ is broken into an infinite
number of sticks, each representing a cluster, and the size of the stick is
the proportion of points in that cluster.

As an example, we consider stick-breaking for a Dirichlet process (e.g. [27]),
where at each step we break off a portion of the remaining interval according
to a beta distribution. This is often written in statistical notation as

$r_{k}\sim\mathcal{B}\mathit{eta}(1,\alpha)\qquad\textstyle
v_{k}=r_{k}\cdot\prod_{i=1}^{k-1}(1-r_{i})$

The random sequence $(v_{0},v_{1},\dots)$ has the property that
$\sum_{i=0}^{\infty}v_{i}=1$, almost surely.

Stick-breaking is easy to define as a random stream stickBreaking $\ \alpha$
in our metalanguage.

Figure 5. From left to right: (a) Dirichlet process clustering by stick-
breaking (§3.3); (b) Feature extraction for a psychological experiment (§3.4):
the features (columns) are automatically inferred and often interpretable.

⬇

stickBreaking :: RealNum $\rightarrow\;$ Prob [RealNum]

stickBreaking
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\alpha$
= do rs $\leftarrow\;$ iid $ beta 1
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\alpha$

let vs = zipWith (*) rs $ scanl (*) 1 $ map (1-) rs

return vs

We can then regard this sequence of probabilities, which sums to $1$, as a
distribution on natural numbers. One way to do this is to use a uniform sample
in $[0,1]$ to index into the sequence, via elementary functional programming.

⬇

toProb :: [RealNum] $\rightarrow\;$ Prob Int

toProb vs = do {r $\leftarrow\;$ uniform; return $ findIndex (> r) (scanl (+)
0 vs)}

For clustering, we also assign some parameters to each cluster, i.e. to each
part of the stick. For example, if the clusters are located geometrically, we
might associate a random position value to each cluster, assuming that the
data points in this cluster follow a normal distribution around that position.
The parameters are taken from a ‘base’ measure. The general procedure is the
Dirichlet Process:

⬇

dp :: RealNum $\rightarrow\;$ Prob a $\rightarrow\;$ Prob (Prob a)

dp
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\alpha$
base = do {vs $\leftarrow\;$ stickBreaking
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\alpha$;

xs $\leftarrow\;$ iid base; return $ do {n $\leftarrow\;$ toProb vs; return
(xs!!n)}}

We can then piece together a Dirichlet Process clustering model.

⬇

cluster :: RealNum $\rightarrow\;$ (Prob a) $\rightarrow\;$ ((b, a)
$\rightarrow\;$ RealNum) $\rightarrow\;$ [b] $\rightarrow\;$ Meas [(b,a)]

cluster
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\alpha$
base likelihood dataset = do

p $\leftarrow\;$ sample $ dp
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\alpha$
base

xs $\leftarrow\;$ sample $ iid p

let taggedData = zip dataset xs

mapM_ (score . likelihood) taggedData

return taggedData

This model (cluster $\
\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\alpha\ $
base likelihood dataset) partitions the data into random clusters via stick-
breaking, draws a value from base for each cluster, and incorporates a score
for each data point using likelihood.

##### Comments on avoiding lazy data structures

Our clustering model demonstrates why it is important to have a separate Prob
monad. We have used iid three times in this model. As previously mentioned, it
is impossible to have a general iid on arbitrary measures, but it is fine on
probability measures (§2.3). For example, iid is used in dp, and so it is
crucial to know that the argument base is a _probability_ measure.

In the literature, there are various ways of avoiding the infinite lazy data
structure of stick breaking. One common approach is to truncate the
distribution. For example, we might pick some small $\epsilon$, and then find
$n$ such that $(1-\sum_{i=1}^{n}v_{i})<\epsilon$, so that the chance of
needing $v_{i}$ with $i\geq n$ is small enough to be ignored. Care needs to be
taken, then, to ensure that this $\epsilon$ is chosen suitably for the model,
which is potentially difficult and non-compositional when stick-breaking is
part of a complex model.

###  3.4. Non-parametric feature assignment

Clustering assigns a single cluster to each data point. We briefly also
mention the task of _feature assignment_ , which assigns a finite set of
features to each data point. A feature assignment for a data set consists of a
finite set of features, together with a subset of these features for each data
point. For example we can have a set of movies, and a feature assignment could
be a set of genres for each movie. In the non-parametric setting, the number
of features is unbounded even for a fixed data set.

As an application, we consider a basic problem from applied psychology [58].
The problem is as follows. We have a set of countries together with a
similarity coefficient for each pair of distinct countries, calculated based
on answers from participants in a study. The goal is to infer a set of
underlying features which characterize the countries in the participants’
minds, and influence their judgement. The outcome is shown in Figure 5 (b), as
a Boolean matrix indicating assignments of features (columns) to countries
(rows). Notice that the inferred features do match actual perceived features,
such as continent (column 1), industry (col. 2), development (col. 4),
conflict (col. 7).

We now describe the model, and where the laziness comes in. The overall
process is described as a function

⬇

bp :: RealNum $\rightarrow\;$ Prob a $\rightarrow\;$ Prob (Prob [a])

that corresponds to a combination of Beta and Bernoulli processes (e.g. [78]).
This generalizes the Dirichlet process dp :: RealNum $\rightarrow\;$ Prob a
$\rightarrow\;$ Prob (Prob a) (§3.3) by producing a list rather than a single
value. See [18] for details.

##### A note about implementation

The Beta process can be constructed using a variant of stick-breaking: each
stick now corresponds to a feature and its size is the proportion of points
with that feature [60]. But in practice this construction can only be used as
an approximation, because we can only look at a finite number of sticks and
the features are unbounded. By contrast, for the Dirichlet process we can stop
stick-breaking once we have found a cluster. These difficulties appear to
coincide with continuity issues in the analysis of the Beta process (e.g. [66,
Sl. 6], also [64, 65, 2]).

In our implementation [18] we avoid these issues by making use of some amount
of hidden state. We set up an Indian Buffet process [33], which is a way to
assign features to data points sequentially by keeping track of features
assigned to previous points. This terminates, and gives the same model [78].
The state is safely encapsulated (see e.g. [3]), and we use streams to deal
with the unbounded aspects.

##  4\. Further examples with random functions

Our examples so far have focused on random streams (§3) and the iid
construction (§2.3). The type of streams is often isomorphic to the function
type Nat $\rightarrow\;$ a, regarding a stream as the function that returns
its value at each index. In this section we briefly discuss the role of the
affinity of the monad Prob in exploring function types.

We have seen random functions linear and piecewiseLinear :: Prob (RealNum
$\rightarrow\;$ RealNum) in Section 3. We now consider Gaussian Processes
(§4.1) and stochastic memoization (§4.2), as other ways of building random
functions. There are plenty more besides; in the repository we define random
functions based on random programs, so that regression becomes program
induction [18].

###  4.1. Gaussian process regression

A Gaussian process (e.g. [27, Ch. 11]) is a random function $f$ with the
property that for a finite input sequence $(x_{1}\dots x_{n})$ the output
distribution $(f(x_{1})\dots f(x_{n}))$ is a multivariate normal distribution.
For simplicity, we focus on 1-dimensional Gaussian processes, which are random
functions $\mathbb{R}\to\mathbb{R}$. As with any function, we can call these
with an unbounded number of arguments: $n$ is not fixed.

A Gaussian process is parameterized by a mean function
$m:\mathbb{R}\to\mathbb{R}$ and a covariance function
$k:\mathbb{R}^{2}\to\mathbb{R}$. Gaussian processes admit conditioning: in
statistical notation, if $f\sim\mathcal{GP}(m,k)$, then

$\text{for all $x_{0}\in\mathbb{R}$, }\quad
f(x_{0})\sim\mathcal{N}\mathit{ormal}(m(x_{0}),\sqrt{k(x_{0},x_{0})})\quad\text{
and }\quad f|(x_{0}\mapsto y)\sim\mathcal{GP}(m|_{x_{0}\mapsto
y},k|_{x_{0}\mapsto y})$

where $m|_{x_{0}\mapsto y},k|_{x_{0}\mapsto y}$ are respectively the
conditional mean and covariance functions222$m|_{x_{0}\mapsto
y}(x)=m(x)+\frac{k(x_{0},x)(y-m(x_{0}))}{k(x_{0},x_{0})}$, and
$k|_{x_{0}\mapsto
y}(u,v)=k(u,v)-\frac{k(u,x_{0})k(x_{0},v)}{k(x_{0},x_{0})}$.. To formalize
this in our metalanguage, we extend it with a Gaussian process primitive

⬇

gp :: (RealNum $\rightarrow\;$RealNum) $\rightarrow\;$ (RealNum
$\rightarrow\;$RealNum $\rightarrow\;$RealNum) $\rightarrow\;$ Prob (RealNum
$\rightarrow\;$RealNum)

and consider the following equation at type Prob (RealNum $\rightarrow\;$
RealNum), for any x0:

(7)
${{\displaystyle\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}gp}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}m}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}k}}}}}}\
\
=\quad\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}}}}}$
y $\leftarrow\;$ normal (m x0) (sqrt (k x$\color[rgb]{0,0,0.7}{}_{0}\;$ x0)) f
$\leftarrow\;$ gp (m’ x$\color[rgb]{0,0,0.7}{}_{0}\;$ y) (k’
x$\color[rgb]{0,0,0.7}{}_{0}\;$ y) return (\x $\rightarrow\;$ if
x==x$\color[rgb]{0,0,0.7}{}_{0}\;$ then y else f x)

where m’ x$\color[rgb]{0,0,0.7}{}_{0}\;$ y and k’
x$\color[rgb]{0,0,0.7}{}_{0}\;$ y are the conditional mean and covariance
functions. To lazily evaluate a Gaussian process we can use (7) to unroll it
as necessary, using different values for x0, and then use the affine property
of the probability monad (3) to remove any reference to gp (c.f. Theorem 2.1).

Once gp is in our metalanguage, we can combine Gaussian processes with other
random functions. For example, we can use a random linear function (§2.1) as a
mean for a Gaussian process:

⬇

gpWithLinear:: Prob (RealNum $\rightarrow\;$ RealNum)

gpWithLinear = do { f $\leftarrow\;$ linear ; return $ gp f (rbf 1 1) }

(using the standard radial basis kernel rbf). The result of running regress
0.3 gpWithLinear dataset is a posterior over smooth curves fitting the points,
shown in Figure 3 (c).

##### Note about implementation

Although the defining equation (7) is straightforward and reminiscent of
Theorem 2.1, it is different from the other distributions so far in that it is
not a Haskell-style definition. We implemented gp in LazyPPL [18] by first
making an infinite sequence of standard normals, using iid (normal 0 1), and
then by using a hidden memo table and standard linear algebra for conditional
probability in Gaussian processes. In general, hidden state would violate the
affine and commutativity properties; in this setting, since we validate (7),
the affine and commutative properties of Prob (2,3) remain satisfied.

##### Comments on the role of lazy structures

Our Gaussian process regression example terminates because (7) allows us to
regard the value of the function f at certain inputs, and disregard its value
at unused arguments. The input values are the points of the data observations,
and the points used for plotting, which are dependent on the viewport and the
resolution.

Since gp uses the affine Prob monad, and not the Meas monad, it can be passed
to the second-order distributions above from Section 3. We can write
spliceProb (poissonPP r) (gp m k) to make a piecewise Gaussian process, which
amounts to what is called a ‘jump process’ in statistics. We can write dp
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\alpha$
(gp m k) for a Dirichlet process mixture of Gaussian processes.

The function space of the metalanguage is here being used to hide a lazy
process. One _could_ replace the call to gp with a multivariate normal
distribution of fixed dimension, but then the plotting points and observation
points would need to be passed manually as an input to the function
gpWithLinear. The dimension would need to be picked based on the number of
data points and the plotting resolution.

With the lazy behaviour of gpWithLinear, we can easily rescale the function,
for example using rescale gpWithLinear :: Prob(RealNum $\rightarrow\;$
RealNum). (We can consider more exotic rescalings too, such as ‘deep Gaussian
processes’ [17], by composing Gaussian processes.) With a non-lazy version
based on explicit multivariate normal distributions, one would also need to
take care to manually rescale the viewport, resolution, and the observation
points, which would not be compositional.

###  4.2. Stochastic memoization

In standard programming, memoization is a form of laziness where a function
caches previous results instead of re-calculating [51]. In functional
probabilistic programming, memoization becomes a powerful method for building
infinite-dimensional probability measures (e.g. [29, 64, 86]). We now discuss
memoization in the setting of the metalanguage, with the separation of Prob
and Meas.

In statistical terms, suppose we have a parameterized distribution,
$\mathcal{P}(x)$ over a space $B$, with parameters $x$ in a space $A$.
Stochastic memoization provides a random function $F:A\to B$ with

$\forall x\in A.\quad F(x)\ \sim\ \mathcal{P}(x)\text{.}$

We can study stochastic memoization in our metalanguage by adding a constant

⬇

memoize :: (a $\rightarrow\;$ Prob b) $\rightarrow\;$ Prob (a $\rightarrow\;$
b)

The idea is that memoize p :: Prob (a $\rightarrow\;$ b) randomly picks an
assignment of results for each argument, informally by sampling once from (p
x) for every (x :: a). We consider the following equation at type Prob (a
$\rightarrow\;$ b):

(8)
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}memoize}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}}}}}=\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\small{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}do}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}y}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{0}$}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}f}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\leftarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}memoize}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}p}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}return}}{\@listingGroup{ltx_lst_space}{
}}(\textbackslash{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{ltx_lst_space}{
}}\@listingLiterate{$\rightarrow\;$}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}if}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}=={\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}}{\@listingGroup{}{$\color[rgb]{0,0,0.7}{}_{0}\;$}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}then}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}y}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}else}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}f}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}x}})\textbraceright}}}}$

As with gp, if the memoized function is only called with a finite collection
of arguments, we can unroll equation (8) for each of the arguments, and then
use the affine law (3) to remove any reference to memoize.

####  4.2.1. Memoization on countable types

By regarding Nat $\rightarrow\;$ a as isomorphic to Stream a, we can define
memoize with domain type Nat just using basic primitives for lazy monadic
streams, according to the following equation:

⬇

memoize :: (Nat $\rightarrow\;$ Prob b) $\rightarrow\;$ Prob (Nat
$\rightarrow\;$ b)

memoize f = do { ys $\leftarrow\;$ mapM f [0..] ; return $ \x $\rightarrow\;$
ys !! x }

(In practice [18], we define memoize more efficiently using tries; c.f. [35].)
We can see, in particular, that memoize (\_ $\rightarrow\;$ p) corresponds to
iid p. With this in mind, following Proposition 2.2, we cannot hope to have
memoizeMeas :: (a $\rightarrow\;$ Meas b) $\rightarrow\;$ Meas (a
$\rightarrow\;$ b), and the restriction to the probability type is crucial.

####  4.2.2. Illustrations of using memoization

In Section 3.3 we have seen the Dirichlet process applied to clustering. One
common method in statistics is to regard the Dirichlet process as a random
measure, by applying it to a generic base measure, for example,

⬇

dp
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\alpha$
uniform :: Prob (Prob RealNum)

That is to say, rather than assigning informative parameters to the clusters
(such as mean position) from the outset, we begin by assigning each cluster a
name, picked uniformly from $[0,1]$.

Later on, of course, we would like to assign a position in (say) 2D space to
each cluster. Since the clusters are named by real numbers, this assignment of
positions to names of clusters is a random function
$f:\mathbb{R}\to\mathbb{R}^{2}$ such that, say,

$\forall r.\,f_{1}(r)\sim\mathcal{N}\mathit{ormal}(0,3)\quad\&\quad
f_{2}(r)\sim\mathcal{N}\mathit{ormal}(0,3)\text{.}$

This can be implemented in our metalanguage by using memoization:

⬇

p $\leftarrow\;$ dp
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\alpha$
uniform; xpos $\leftarrow\;$ memoize (\_ $\rightarrow\;$ normal 0 3); ypos
$\leftarrow\;$ memoize (\_ $\rightarrow\;$ normal 0 3)

If we return do {r $\leftarrow\;$ p ; return (xpos r,ypos r)}, then this whole
program is equivalent to using a different base distribution, dp
$\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\alpha$
(mvnormal (0,0) (3,3)). However, the memoized form is more compositional: we