Constrained generation of well-typed programs
summary
Approach reuses constraint-based type inference (Pottier & Rémy style) by parameterizing constraint generation over a search monad, representing partial untyped terms with subcomputations (do nodes) and running incremental constraint solving after each generation step. Prototype generates simply-typed and Hindley-Milner-style terms, elaborates solutions, and enumerates or samples solutions. Performance beats naive rejection sampling (practical up to size ~200–300; size 300 takes seconds), but generation speed needs further optimization for heavy fuzzing.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:15Efficient well-typed generation
- 3:21Type-directed challenges
- 6:33Type inference guidance
- 12:07Syntax with subcomputations
- 20:51Prototype generator demo
- 24:00Performance and scalability
- 26:51Comparison with rejection sampling
- 29:23Q&A
related talks
33mSolving constraints during type inference
20mGenerating Well-Typed Terms that are not "Useless"
18mDeveloping a Dependently Typed Language with Runtime Proof Search
56mOn Type-Based Techniques for Program Manipulation
32mHole Refinements for Polymorphic Type-and-Example Driven Synthesis
18mConcrete Type Inference for Code Optimization using Machine Learning with SMT S...
19mType Inference Logics
19mCovering All the Bases: Type-Based Verification of Test Input Generators