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.