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

Has anyone looked at extending Boltzmann sampling to containers or dependent polynomials?

  • $\begingroup$ What exactly do you want to sample, what syntax? (In any case, I doubt this has been done.) $\endgroup$ Apr 22, 2021 at 12:09
  • $\begingroup$ I'd like to randomly generate well-formed elements of dependently-typed inductive datatypes (eg, for quickcheck-style property-based testing). $\endgroup$ Apr 23, 2021 at 8:47


Your Answer

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