A Word Sampler for Well-Typed Functions

TL;DR

The paper tackles the problem of uniformly sampling well-typed functions from a simply-typed, first-order language defined by an acyclic automaton. It achieves this by encoding the syntax-directed typing rules as a parameterized context-free grammar $G_\Gamma$, normalizing to CNF, and intersecting with the automaton to enable exact uniform sampling from $\mathcal{L}(α_{\varnothing})$. The authors provide a space-complexity analysis, demonstrate feasibility for small arities (k ≤ 3), and report practical sampling performance (≈5.6×10^5 samples/s on a typical device). This CFG-embedding approach offers a principled, type-safe foundation for program synthesis and analysis, with clear paths to generalization to richer typing systems and lazy generation strategies.

Abstract

We describe an exact sampler for a simply-typed, first-order functional programming language. Given an acyclic finite automaton, $α_{\varnothing}$, it samples a random function uniformly without replacement from well-typed functions in $\mathcal{L}(α_{\varnothing})$. This is achieved via a fixed-parameter tractable reduction from a syntax-directed type system to a context-free grammar, preserving type soundness and completeness w.r.t. $\mathcal{L}(α_{\varnothing})$, while retaining the robust metatheory of formal languages.

Figures (1)

• Figure 1: Slice sampling and type inference delay (log-scaled) vs. sequence length $|\sigma|=n$ for arities $k\in [1,3]$.