Reusability and Dependent Types

Project: Research

Project Details


Robin Milner coined the slogan well typed programs cannot go wrong , advertising the strength of typed functional languages like MLand Haskell in using types to catch runtime errors. Nowadays, we can and want to go further: dependently typed programming exploits the power of very expressive type systems to deliver stronger guarantees but also additional support for software development, using types to guide the development process. This is witnessed by a recent surge of language proposals with the goal to harness the power of dependent types, e.g. Haskell with GADTs, Agda, Coq, Omega, Concoqtion, Guru, Ynot, Epigram and so on. However, expressive type systems have their price: more specific types frequently reduce the reusability of code, whose too-specific implementation type may not fit its current application. This phenomenon already shows up in the traditional Hindley-Milner style type system of ML and Haskell; it becomes even more prevalent in a dependently typed setting. Luckily, all is not lost: dependent types are expressive enough that they can talk about themselves reflectively, making meta-programming one of its potential killer applications with the potential of combining expressive types and reusable software components. Based on and inspired by recent research at Nottingham on dependently typed programming (EPSRC EP/C512022/1) and container types (EPSRCEP/C511964/2) and at Oxford on data type-generic programming (EPSRCGR/S27078/01, EP/E02128X/1) we plan to explore the potential of dependent types to deliver reusable and reliable software components. To achieve this, we intend to explore two alternative roads - reusability by structure and reusability by design - and express both within a dependently typed framework. Our programme is to build new tools extending the Epigram 2 framework, investigate the underlying theory using container types, and most importantly establish novel programming patterns and libraries. We seek funding for an RA at Nottingham (Peter Morris, whose PhD laid much of the groundwork for this proposal), and two doctoral students (one each at Oxford and Strathclyde), together with appropriate support for equipment, coordination, travel, and dissemination (i.e. a workshop and a summer school)

Key findings

We have changed out understanding of parametricity - in particular our new understanding is based upon the notion of comprehension. The associated paper is up for a best-paper award.
Effective start/end date1/10/0930/09/13


  • EPSRC (Engineering and Physical Sciences Research Council): £151,124.00


Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.
  • Transporting functions across ornaments

    Dagand, P-E. & McBride, C., 2012, ICFP '12 Proceedings of the 17th ACM SIGPLAN international conference on Functional programming . New York, p. 104-113 10 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution book

    17 Citations (Scopus)
  • The gentle art of levitation

    Chapman, J., Dagand, P-E., Mcbride, C. & Morris, P., 2010, ICFP 2010 Proceedings of the 15th ACM SIGPLAN international conference on functional programming. Hudak, P. (ed.). New York, p. 3-14 12 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution book

    36 Citations (Scopus)