A Word Sampler for Well-Typed Functions
summary
An exact sampler takes an acyclic finite automaton α∅ and produces functions from a simply-typed first-order language that are uniformly without replacement drawn from the well-typed subset L(α∅). It compiles the syntax-directed type system into a vanilla context-free grammar via a fixed-parameter tractable reduction that preserves type soundness and completeness w.r.t. L(α∅), normalizes to Chomsky form, intersects with the finite regular slice, and supports both uniform and autoregressive decoding; benchmarks hit ≈22M tokens/s and CNF size grows to a few megabytes for nontrivial signatures.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:48Word sampler for well-typed functions
- 2:34Type theories into context-free grammars
- 5:27Typing judgments into grammar
- 7:14Toy language for function generation
- 9:00Context-free with regular constraints
- 10:25Sampling methods and benchmarks
- 11:06Tool demo and related work
- 11:59Q&A
related talks
30mRecognizing regular patterns in mixed type sequences using Symbolic Finite Automata
30mType-Checking Heterogeneous Sequences in a Simple Embeddable Type System
29mA Term Matching Algorithm and Substitution Generality
30mConstrained generation of well-typed programs
20mGenerating Well-Typed Terms that are not "Useless"
16mExtrinsically Typed Operational Semantics for Functional Languages
14mType-Sensitive Algebraic Macros
20mCertified Abstract Machines for Skeletal Semantics