I came upon this when thinking about the semantics of probabilistic programs. Say you have a generative model

N ~ Poisson()
for n = 1:N
  X[i] ~ Normal()

Then the size of X will stochastically depend on N. Thinking about this as dependent pairs, I would intuitively write something like

$$ X : \sum_{n \sim \operatorname{Poisson}()} \operatorname{Vect} n $$

Has anyone come up with such a theory of representing stochastic structure by dependent types?

For a bit of context, I am interested in ways how trace types could be extended to more dynamic settings, in the sense of probabilistic programs that would require a trace type whose key space is itself random (i.e., the encountered variables and their shapes can vary in sampling).

  • 1
    $\begingroup$ I noticed the downvote, which I suspect to come from "lack of research"; but using all my Google-fu, I wasn't able to come up with any search terms indicating that there is an overlap between research in dependent types and semantics of dynamic probabilistic programs. All seems to be focused on measure theory. $\endgroup$ Sep 21 '20 at 8:59
  • 2
    $\begingroup$ My DuckDuckGo fu is stronger than your Google fu. $\endgroup$ Sep 21 '20 at 13:42
  • $\begingroup$ Well done. I am familiar with the Giry monad and a bit with Fritz' work, but the references there also only talk about the "static case", as far as I see. In that setting, I guess we would need an indexed Giry monad, where the type of the the result of bind is parametrized in the types of its arguments: (rpoisson()::Prob Nat >>= \n -> rnorm(n)::Prob (Pi_{n:Nat} Vect n))::Prob (Sigma_{n:Nat} Vect n), or something like that? $\endgroup$ Sep 21 '20 at 19:44
  • $\begingroup$ What's the "static case"? In dependent type theory the distinction between the static and dynamic phases is not as clear-cut, so it could mean several things. $\endgroup$ Sep 21 '20 at 20:45
  • $\begingroup$ Ah, I wasn't talking about type theory here, but the structure of the probabilistic program. In a static one, the structure of the trace is determinstic (given the arguments); in a dynamic one, it may change in size or even structure. In the example, we have X change size based on N, so it is dynamic. $\endgroup$ Sep 22 '20 at 6:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.