Measures are a type constructor $M T$ . They map subsets of the event space $T$ to $[0, 1]$ :

$M T : σ (T) \to [0, 1]$

Measures are functors: if we have a measure of type $M T$ and a function $f : T \to U$ then we can define an object of type $M U$ .

Under certain conditions, measures have a density $\mathdd d ν : T \to R^{+}$ .

We can also define $Rand [T] : Ω \to T$ .

import aeppl.random as ar
 
mu = at.scalar()
sigma = at.scalar()
 
x = ar.normal(mu, sigma)
y = ar.halfnormal(x, 1.)

In this case the first ar.normal is a function $normal : R \times R^{+} \to MR$ , and the second $halfnormal : MR \to M R^{+}$ .

We pass from $halfnormal$ , a probability measure over probability measures to a probabilty measures by defining an evaluation map $μ$ , $μ$ acts by integrating or averaging (or sampling?).
We define a map $μ : T \to M T$ for passing from a space $T$ to a probability measure over $T$ , typically by sending $x \in T$ to the Dirac measure over $x$ .
We define an assignment $M$ on maps so that a map of spaces $f : T \to U$ extends to a map of spaces of probability measures $M f : M T \to M U$ , this takes the form of the pushforward definition.

The probability monad

References