6
$\begingroup$

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).

Improve this question
$\endgroup$
8
  • 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$
    – phipsgabler
    Commented Sep 21, 2020 at 8:59
  • 2
    $\begingroup$ My DuckDuckGo fu is stronger than your Google fu. $\endgroup$
    – Andrej Bauer
    Commented Sep 21, 2020 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$
    – phipsgabler
    Commented Sep 21, 2020 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$
    – Andrej Bauer
    Commented Sep 21, 2020 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$
    – phipsgabler
    Commented Sep 22, 2020 at 6:28

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.