Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online

We provide a solution to the problem of polymorphic type-guided synthesis via enumerative search. Related problems have been explored before, in Myth, Tygar, and Synquid. Our synthesis \textit{problem} consists of a component library, a query type, and optional input-output examples. A \textit{solution} to the synthesis problem is a Haskell code snippet that only contains applications, $\lambda$-abstractions, and variables (including components), and that has the desired type and works for the optionally given examples. We evaluated Petsy on 20 benchmarks that we took from Tygar’s paper. We used the same set of 130 components in all experiments. When comparing Petsy with Tygar, Petsy, both tools perform quite similarly in terms of speed and solution quality.