There are some linguistics papers going into a notion of probabilistic type theory.<p>It&#x27;s definitely an interesting area to think about.  After all, Homotopy Type Theory has been teaching us that types are <i>spaces</i>, with topological structure.  So hypothetically, how would you construct probability measures over those spaces?  Could you then take points&#x2F;proofs&#x2F;programs as samples?  What would the samples tell you about the overall measure?<p>What would it all mean?<p>Well, the probability monad already gives us a way to compute with distributions, and thus do probabilistic programming, but I&#x27;m not sure that really tells us anything type-theoretical, since the distributions are all <i>over</i> preexisting data types.