"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."
The functional programming language Haskell has an advanced type system, the design of which we have strongly influenced. As a result, it has become possible to capture strong safety and correctness properties in the type system of an industrial strength programming language. In particular, we demonstrated that it is possible to model aspects a program's awareness of the state of the environment it runs in, ensuring that the information it requests is adequate to justify the actions it performs.