<p>I’d like to randomly sample from dependently-typed data structures.</p>
<p>Has anyone looked at extending <a href="https://en.wikipedia.org/wiki/Boltzmann_sampler" rel="nofollow noreferrer">Boltzmann sampling</a> to <a href="https://www.sciencedirect.com/science/article/pii/S0304397505003373" rel="nofollow noreferrer">containers</a> or <a href="https://www.irif.fr/%7Emellies/mpri/mpri-ens/articles/gambino-hyland-polynomial-functors.pdf" rel="nofollow noreferrer">dependent polynomials</a>?</p>

CC BY-SA 4.0
2021-04-22T12:09:35.483Z
What exactly do you want to sample, what syntax? (In any case, I doubt this has been done.)
Martin Berger
CC BY-SA 4.0
2021-04-23T08:47:56.777Z
I'd like to randomly generate well-formed elements of dependently-typed inductive datatypes (eg, for quickcheck-style property-based testing).
Neel Krishnaswami
<co.combinatorics><lo.logic><type-theory><dependent-type><sampling>
Boltzmann sampling for containers/dependent polynomials?
Neel Krishnaswami
# Boltzmann sampling for containers/dependent polynomials?

(Asked by: username_0 on 2021-04-22)

I’d like to randomly sample from dependently-typed data structures.

Has anyone looked at extending [Boltzmann sampling](https://en.wikipedia.org/wiki/Boltzmann_sampler) to [containers](https://www.sciencedirect.com/science/article/pii/S0304397505003373) or [dependent polynomials](https://www.irif.fr/%7Emellies/mpri/mpri-ens/articles/gambino-hyland-polynomial-functors.pdf)?

**Tags:** co.combinatorics, lo.logic, type-theory, dependent-type, sampling

> **Comments:**
> **username_1**: What exactly do you want to sample, what syntax? (In any case, I doubt this has been done.)  
> **username_0**: I'd like to randomly generate well-formed elements of dependently-typed inductive datatypes (eg, for quickcheck-style property-based testing).  

---

## 0 answers

