EAGER: Semi-automated Type-directed Programming

类型导向编程是在强类型函数式语言中找到的一种强大的编程范例，其中使用程序的类型来指导其开发。这类语言的用户经常评论说，一旦他们声明了适当的类型，他们的程序就“自己编写”了。在现实中，实际的开发过程远不是自动的；开发人员仍然必须应用手动推理原则来派生他们的程序，即使他们的许多选择是由语言的类型系统强制的。这个项目旨在通过利用程序综合和类型理论中的技术来机械化类型导向的编程过程。这个项目的智力价值有两个方面：(1)扩展了类型程序综合的理论基础；(2)将这些基础应用于帮助类型导向程序设计的程序辅助工具。除了提供一个工具来提高当前函数式程序员的生产力，该项目更广泛的意义和重要性是类型导向编程的好处的结晶，这种形式允许非函数式程序员理解、欣赏并直接受益于这种编程范例。该项目扩展了以前在使用类型的程序合成的基础上所做的工作，解决了在将这些基础应用到合成工具中时遇到的表现性和可伸缩性问题。值得注意的是，该项目统一了基于类型和基于验证的程序合成方法，允许对代数和原始数据类型提供丰富的支持，并为理解这两种合成风格提供了一个公共框架。此外，该项目研究半自动而不是全自动的程序合成，其中用户在整个合成过程中与合成工具交互。这种方法的基础是采用精化树，这是一种捕获合成器可以产生的程序的潜在形状的数据结构，成为用于可视化和与该工具交互的有用的数据结构。通过追求半自动合成，这些工具通过将开发人员用作先知来扩展到真实世界的编程环境，否则工具将花费太长时间或陷入搜索解决方案的困境。

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.