Parsing randomness
Harrison Goldstein, Benjamin C. Pierce
Abstract
Random data generators can be thought of as parsers of streams of randomness. This perspective on generators for random data structures is established folklore in the programming languages community, but it has never been formalized, nor have its consequences been deeply explored. We build on the idea of freer monads to develop free generators, which unify parsing and generation using a common structure that makes the relationship between the two concepts precise. Free generators lead naturally to a proof that a monadic generator can be factored into a parser plus a distribution over choice sequences. Free generators also support a notion of derivative, analogous to the familiar Brzozowski derivatives of formal languages, allowing analysis tools to "preview" the effect of a particular generator choice. This gives rise to a novel algorithm for generating data structures satisfying user-specified preconditions.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 017c00c6-36f9-442c-9e24-1eec1e9b0773Cited by top-tier papers7
- Property-Based Testing in PracticeHarrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce et al.ICSE 2024 · 21 citations
- Bennet: Randomized Specification Testing for Heap-Manipulating ProgramsZain K. Aamer, Benjamin C. PierceOOPSLA 2025 · 4 citations
- Ratte: Fuzzing for Miscompilations in Multi-Level Compilers Using Composable SemanticsPingshi Yu, Nicolas Wu, Alastair F. DonaldsonASPLOS 2025 · 3 citations
- Finite-Choice Logic ProgrammingChris Martens, Robert J. Simmons, Michael ArntzeniusPOPL 2025 · 3 citations
- Tuning Random Generators: Property-Based Testing as Probabilistic ProgrammingRyan Tjoa, Poorva Garg, Harrison Goldstein, Todd D. Millstein et al.OOPSLA 2025 · 2 citations
Builds on1
Related papers
- Exact Recursive Probabilistic ProgrammingDavid Chiang, Colin McDonald, Chung-chieh ShanOOPSLA 2023 · 12 citations
- Interaction trees: representing recursive and impure programs in CoqLi-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur et al.POPL 2020 · 133 citations
- Zippy LL(1) parsing with derivativesRomain Edelmann, Jad Hamza, Viktor KuncakPLDI 2020 · 13 citations
- Combining Nondeterminism, Probability, and Termination: Equational and Metric ReasoningMatteo Mio, Ralph Sarkis, Valeria VignudelliLICS 2021 · 14 citations
- Stream TypesJoseph W. Cutler, Christopher Watson, Emeka Nkurumeh, Phillip Hilliard et al.PLDI 2024 · 7 citations
