Hole Refinements for Polymorphic Type-and-Example Driven Synthesis
summary
Toolchain combines a parametricity-aware feasibility reasoner and a tactic-driven synthesizer: Taxi computes polymorphic input–output normal forms and guarantees every search state is a correct partial implementation, and Driver is a tactic language that top-down refines holes into constructors, eliminators and recursive combinators. Benchmarks show a modest ~10% win from feasibility alone, a single 3.66× case, and combined techniques that shortcut search achieving nearly 5x speedups on targeted examples.
AI-written summary · about
chapters (10)
- 0:00Whole refinements for synthesis
- 1:03Type-driven hole suggestions fail
- 6:23Valid refinements via equational reasoning
- 7:07Taxi reasoner for polymorphic constraints
- 9:36Program extraction from polymorphic examples
- 11:24Refinements to program synthesis
- 15:18Tactic language for refinement control
- 18:25Synthesis performance benchmarking
- 21:17System overview and summary
- 21:59Q&A
related talks
25mRecursive Program Synthesis using Paramorphisms
39mDependent Type Driven Program Synthesis in Idris
26mProgram Synthesis Using Example Propagation
23mInductive Program Synthesis by Meta-Analysis-Guided Hole Filling
30mConstrained generation of well-typed programs
31mLetting users do the undecidable: lessons from program synthesis
56mOn Type-Based Techniques for Program Manipulation
19mExtensible Metatheory Mechanization via Family Polymorphism