Haskell Types with Added Value

好的想法，就像闪电，采取最导电的路径到达地球。这个为期一年的项目利用新的技术见解，缩小从理论研究到编程主流的火花差距。在过去的十年中，依赖类型--捕获数据有效性的相对概念--已经从逻辑和证明系统跳到了编程中。原型语言，如卡宴，ATS，Agda和我们自己的Epigram教我们如何精确地描述数据，但没有一个有一个连贯的处理应用程序中的交互。这个项目将把依赖类型的基础知识带到应用程序开发中，不是通过原型，而是通过Haskell，一种成熟的函数式编程语言，由于格拉斯哥Haskell编译器（GHC），现在在微软的支持下开发。为了实现这一飞跃，我们必须对支撑交互式和分布式系统的数学结构的理论问题给出实际的答案。我们必须把黑板放到主板上。实现这个项目的工具是我们的GHC预处理器，Strathclyde Haskell Enhancement（SHE），它将“依赖类型的Haskell”部分转换为Haskell。启动和运行，SHE已经提供了我们方法的基础，导致一篇文章在2011年被Journal of Functional Programming接受，并刺激了对依赖类型交互的数学和扩展的工程挑战的更深入研究。通过理论研究、库设计和案例研究，我们将通过论文和开源软件在这一领域取得进展。GHC正在采用我们的功能，但我们不需要等待。SHE可以维持低成本的探索，现在将一个有效的工具包交给用户，并为Haskell中的依赖类型和下一代函数式语言中的编程交互提供未来的前景。Haskellers认识到需要：微软目前资助了Strathclyde的一个Haskell类型的数字依赖的博士学位。这个项目是一个双重修复：它将依赖类型从明天的语言导入到今天的语言中，并且它允许我们将明天的依赖类型语言引导到生产软件的原则方法中。我们在理论研究和专业软件开发方面有着良好的记录，有着改善编程的关键思想，有着提供世界领先研究的技能。

Good ideas, like lightning, take the most conductive path to earth. This one-year project takes advantage of fresh technological insights to narrow the spark-gap from theoretical research to the programming mainstream. In the last decade, dependent types --- capturing relative notions of data validity --- have jumped from logics and proof systems to programming. Prototype languages such as Cayenne, ATS, Agda and our own Epigram teach us how to characterize data precisely, but none has a coherent treatment of interaction in applications. This project will bring the basics of dependent types to application development now, not via a prototype, but with Haskell, a mature functional programming language with growing traction, thanks to the Glasgow Haskell Compiler (GHC), now developed under the Microsoft aegis. To make this jump, we must give practical answers to theoretical questions about the mathematical structures which underpin interactive and distributed systems. We must take the blackboard to the motherboard.The tool which enables this project is our GHC preprocessor, the Strathclyde Haskell Enhancement (SHE), which mechanizes a partial translation from 'dependently typed Haskell' to Haskell as it stands. Up and running, SHE has already delivered the basics of our approach, leading to an article accepted in 2011 by the Journal of Functional Programming, and spurring deeper investigation of both the mathematics of dependently typed interaction and the engineering challenge of scaling up. Through theoretical research, library design and case study, we shall deliver progress across this spectrum through papers and open source software. GHC is adopting our functionality, but we do not need to wait. SHE can sustain low-cost exploration, putting an effective toolkit in users' hands now, as well as informing the future prospectuses both for dependent types in Haskell and for programming interaction in the next generation of functional languages. Haskellers recognize the need: Microsoft currently funds a PhD at Strathclyde on numerical dependency in Haskell types.This project is, then, a double fix: it imports dependent types from tomorrow's languages to today's, and it allows us to guide tomorrow's dependently typed languages towards principled approaches to production software. We have proven track records in theoretical research and professional software development, key ideas to change programming for the better, and the skills to deliver world-leading research.