一句话:用自由生成器统一随机生成与解析,证明生成器可分解为解析器加选择序列分布,并借助导数实现带前置条件的数据生成。
随机数据生成器可视为随机性流的解析器,这一视角在 PL 社区虽为常识却未被形式化。本文基于 freer monad 提出 free generator,用统一结构刻画解析与生成,使二者关系精确化。由此证明一个 monadic 生成器可分解为解析器与对选择序列的分布。Free generator 还支持类似形式语言中 Brzozowski 导数的导数概念,使分析工具能“预览”某个生成器选择的效果。基于该理论,作者给出一种新算法,用于生成满足用户指定前置条件的数据结构。
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.