Haskell Types with Added Value

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.

This project seeks to deliver useful and usable programming technology based on novel techniques and original theoretical research, via the SHE preprocessor for the functional programming language Haskell. SHE will achieve impact outside academia by putting tools for productivity with precision in the hands of programmers: SHE already has this impact on our own software projects, here at Strathclyde, notably the implementation of Epigram. The project is focused on library design, packaging the key abstractions for systematic deployment. Our case studies will show the new technology in effective action and provide examples that other programmers can readily adapt.

Our primary impact is a contribution to the knowledge base, with scientific advances and new software techniques made available and ready to use for a significant and growing community of software professionals. We shall remain active in promoting uptake: new knowledge for the field will become new skills for people, as we equip them to face complex issues in modern applications development with precise and modular technology. Our longer term agenda impacts on society and the economy by making it increasingly feasible, on a technical level, to insist on higher standards of acceptable software behaviour, stronger security policies, clearer articulation of component capabilities, and more precise compliance with agreed protocols. By expressing more of `the rules of the game' in types, we shift more quality assurance responsibility into the basic discipline enforced by the compiler. Our libraries and case studies will show that it is feasible to work effectively to that high level of assurance, and thus reasonable to demand it!

Our work will reach Haskell programmers directly, as our preprocessor is already available and the libraries we develop in this project will be distributed with a suitable open source licence. We have a track record in attracting programmers to fresh ideas. We pursue uptake by participating in the online community and engaging with practitioners and their real world problems at first hand. It is not enough to write academic papers!

Moreover, we shall continue to work with the designers of the Glasgow Haskell Compiler to standardise our technology and techniques in the standard Haskell language and libraries, thus delivering the standard of support needed for industrial-strength deployment. The work to make GHC absorb SHE has already started!

This project addresses a real software problem: in our world of multiple communicating devices, we need reliable ways to express interfaces for meaningful communication and enforce that components respect those interfaces. We seek new programming language technology to cope with the increasing complexity of our computing environments. If we can bring about a step-change in what can feasibly be achieved with Haskell, we shall raise the quality assurance bar for everyone, and other more mainstream programming languages will surely step up too.