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