EAGER: Semi-automated Type-directed Programming

Grinnell College, Grinnell IA

Investigators

Abstract

Type-directed programming is a powerful programming paradigm found in strongly-typed functional languages where the types of a program are used to guide its development. Users of such languages frequently comment that their programs "write themselves" once they declare the appropriate types. In reality, the actual development process is far from automatic; developers still must apply manual reasoning principles to derive their program even though many of their choices are forced by the language's type system. This project aims to mechanize the type-directed programming process by leveraging techniques from program synthesis and type theory. The intellectual merits of this project are twofold: (1) the expansion of the theoretical foundations of program synthesis with types and (2) the application of these foundations towards program assistance tools that aid in type-directed programming. Beyond merely providing a tool that enhances the productivity of current functional programmers, the project's broader significance and importance is the crystallization of the benefits of type-directed programming in a form that allow non-functional programmers to understand, appreciate, and directly benefit from this programming paradigm. The project extends prior work in the foundations of program synthesis with types, addressing issues of expressiveness and scalability encountered when adopting these foundations into synthesis tools. Notably, the project unifies type-based and verification-based approaches to program synthesis, allowing rich support for both algebraic and primitive data types as well as providing a common framework for understanding both styles of synthesis. In addition, the project investigates semi-automated, rather than fully-automated, program synthesis where the user interacts with the synthesis tool throughout the synthesis process. The basis of this approach lies in adopting the refinement tree, a data structure that captures the potential shapes of programs that a synthesizer can produce, into a useful data structure for visualizing and interacting with this tool. By pursuing semi-automated synthesis, these tools scale up to real-world programming environments by using the developer as an oracle whenever the tool would otherwise take too long or get stuck searching for a solution.