Program Synthesis from Linear and Graded Types

Graded types are a class of resourceful types which allow for finegrained quantitative reasoning about data-flow in programs. Tracing their roots from linear types, the use of resource annotations (or grades) on data, allows a programmer to express structural or semantic properties of their program at the type level. Such systems have become increasingly popular in recent years, mainly for the expressive power that they offer to programmers; judicious use of grades in type specifications significantly reduces the number of typeable programs. These additional constraints on types lend themselves naturally to typedirected program synthesis, which leverage the information provided by types to prune ill-resourced programs from the search space of candidate programs. In synthesis, this grade information can be exploited to constrain the search space of programs even further than in standard type systems. We present an approach to program synthesis for linear and graded type systems, where grades form an arbitrary pre-ordered semiring. Harnessing this grade information in synthesis is non-trivial, and we explore the issues involved in designing and implementing a resource-aware program synthesis tool, culminating in an efficient and expressive program synthesis tool for the research programming language Granule, which uses a graded type system. We show that by harnessing grades in synthesis, the majority of our benchmarking synthesis problems (many of which involve recursive functions over recursive ADTs) require less exploration of the synthesis search space than a purely type-driven approach and with fewer needed input-output examples. Our type-and-graded-directed approach is demonstrated in the Granule but we also adapt it for synthesising Haskell programs that use GHC’s Linear Types extension, demonstrating the versatility of our approach to resourceful program synthesis.