Programming as Conversation: Type-Driven Development in Action

本项目旨在改进程序开发过程，采用“类型驱动开发”的过程。我们相信，为了实现最高水平的生产力，编程应该是程序员和机器之间的对话。在类型驱动的开发中，我们首先给出一个类型作为程序的计划。这样，机器就不会被视为拒绝不完整或不正确程序的对手，而是程序员的助手。这种思想的一种有限形式存在于现代集成开发环境中：当在文本缓冲区中输入“x”时，环境将显示“x”实现的方法。这个项目将把这个想法更进一步。我们不仅可以对部分程序提供反馈，还可以使用类型及其结构来生成程序的重要部分，并指导更复杂组件（如通信和安全协议）的实现。在开发过程中，程序的大部分时间都处于不完整状态，编程行为与实现完整程序所需的步骤和最终结果一样多。因此，语言实现和工具必须支持编辑过程以及检查和编译最终结果。在这个项目中，我们将基于良好的理论基础，开发必要的工具来支持交互式类型驱动的开发。此外，我们将使工具本身可编程：基础将本质上给出一种编程“策略”语言，这将是可组合的，为自动程序构建引入复杂的方法，由类型指导。我们将始终与行业保持联系，以确保我们开发的技术非常适合商业相关问题。

This project aims to improve the program development process, using a process of "Type-driven Development". We believe that in order to enable the highest levels of productivity, programming should be a conversation between the programmer and the machine. In type-driven development, we begin by giving a type as a plan for a program. Then the machine, rather than being seen as an adversary which rejects incomplete or incorrect programs, is the programmer's assistant. A limited form of this idea exists in modern integrated development environments: when typing "x." into a text buffer, the environment will show with methods "x" implements. This project will take this idea several steps further. Not only can we give feedback on partial programs, we can also use types and their structure to generate significant parts of a program and direct the implementation of more complex components such as communication and security protocols.During development, programs spend most of their time in an incomplete state, and the act of programming is as much about the steps required to achieve a complete program as it is about the end result. Accordingly, language implementations and tools must support the editing process as well as check and compile the end result. In this project, we will develop the necessary tooling to support interactive type-driven development, based on sound theoretical foundations. Furthermore, we will make the tooling itself programmable: the foundations will essentially give a language of programming "tactics", which will be composable intro sophisticated methods for automatic program construction, directed by the type. We will liaise with industry throughout to ensure that the techniques we develop are well-suited to commercially relevant problems.