Research Project

Epigram: Innovative Programming via Inductive Families

Zhaohui Luo, James McKinna, Paul Callaghan, and Conor McBride
Dept of Computer Science, Royal Holloway, University of London

Funded by EPSRC, grant ref. GR/R72259 (Dec. 2001 - Aug 2005)
In collaboration with the ALTA Systems Ltd. and the Centre for Educational Measurement at Belfast

Abstract of the project proposal

This is an adventurous proposal, seeking to investigate a novel approach to the practice of functional programming. We believe that a dependent type system centered on inductive families of datatypes can have a radical and positive impact on the way we define data structures and express computations over them. Inductive families are new to programming, and a distinct advance on the weaker technology made available by languages like DML, Cayenne and Haskell. Our objective is to demonstrate the value of this approach and make it accessible to programmers.

Our method is to develop a platform, Epigram, and write programs: we will address substantial problems and compare our results with current practice. Epigram is the first proposed platform to take inductive families seriously as data structures, and also the first to explore the benefits of dependent types for program code itself. This project is about learning to program in a new way.