<p>I came upon this when thinking about the semantics of probabilistic programs.  Say you have a generative model</p>
<pre><code>N ~ Poisson()
for n = 1:N
  X[i] ~ Normal()
</code></pre>
<p>Then the size of <code>X</code> will stochastically depend on <code>N</code>.  Thinking about this as dependent pairs, I would intuitively write something like</p>
<p><span class="math-container">$$
X : \sum_{n \sim \operatorname{Poisson}()} \operatorname{Vect} n
$$</span></p>
<p>Has anyone come up with such a theory of representing stochastic structure by dependent types?</p>
<p>For a bit of context, I am interested in ways how <a href="https://dl.acm.org/citation.cfm?id=3371087" rel="nofollow noreferrer">trace types</a> 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).</p>

CC BY-SA 4.0
2020-09-21T08:59:24.167Z
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.
phipsgabler
CC BY-SA 4.0
2020-09-21T13:42:11.973Z
[My DuckDuckGo fu](https://www.reddit.com/r/dependent_types/comments/irkrdd/dependent_types_for_giry_probability_monads_eg/) is stronger than your Google fu.
Andrej Bauer
CC BY-SA 4.0
2020-09-21T19:44:36.667Z
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?
phipsgabler
CC BY-SA 4.0
2020-09-21T20:45:14.387Z
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.
Andrej Bauer
CC BY-SA 4.0
2020-09-22T06:28:01.487Z
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.
phipsgabler
CC BY-SA 4.0
2020-09-22T07:39:40.767Z
You said "dependent pair", you were talking about dependent type theory, whether you like it or not :-)
Andrej Bauer
CC BY-SA 4.0
2020-09-22T07:42:10.793Z
Let's say I accidentially used a non-disjoint union of both :D
phipsgabler
CC BY-SA 4.0
2020-10-02T16:56:37.700Z
I feel like this question is legitimate, even if there is some secret incantation that can return interesting results on some search engine. This feels different from, say, asking about records in dependent type theory (though there are many non-trivial things to say there as well).
cody
<type-theory><pr.probability><dependent-type><denotational-semantics>
Is there a known notion of "stochastic dependent pair"?
phipsgabler
# Is there a known notion of "stochastic dependent pair"?

(Asked by: username_0 on 2020-09-20)

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

**Tags:** type-theory, pr.probability, dependent-type, denotational-semantics

> **Comments:**
> **username_0**: 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.  
> **username_1**: [My DuckDuckGo fu](https://www.reddit.com/r/dependent_types/comments/irkrdd/dependent_types_for_giry_probability_monads_eg/) is stronger than your Google fu.  
> **username_0**: 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?  
> **username_1**: 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.  
> **username_0**: 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.  
> **username_1**: You said "dependent pair", you were talking about dependent type theory, whether you like it or not :-)  
> **username_0**: Let's say I accidentially used a non-disjoint union of both :D  
> **username_2**: I feel like this question is legitimate, even if there is some secret incantation that can return interesting results on some search engine. This feels different from, say, asking about records in dependent type theory (though there are many non-trivial things to say there as well).  

---

## 0 answers

