Hole Refinements for Polymorphic Type-and-Example Driven Synthesis

Abstract

Many synthesizers implicitly benefit from using polymorphic types, since parametric polymorphism reduces the search space. Additional synthesis constraints may interfere with parametricity. In particular, a polymorphic type may cause otherwise feasible input-output examples to contradict each other. We present Taxi (type-and-example based inferencer), a tool for efficiently reasoning about the feasibility of polymorphic programs specified by input-output examples, and Driver, a tactic language for top-down program synthesis that uses feasibility reasoning to prune the search space. Taxi guarantees that every search state corresponds to a correct (albeit possibly partial) implementation. In addition, it allows for shortcutting the synthesis when a subspecification covers all cases. We show that these techniques have the potential to speed up top-down enumerative type-and-example driven synthesizers.