Epigram: Dependent Types for Practical Programming

Conor McBride (University of Durham)

Why do dependent types matter? Types matter. That's what they're for---to classify data with respect to criteria which matter: how they should be stored in memory, whether they can be safely passed as inputs to a given operation, even who is allowed to see them. Dependent types are types expressed in terms of data, explicitly relating their inhabitants to that data. As such, they enable you to express more of what matters about data. Dependent types are better at mattering on your behalf, and that is why I hope they might matter to you.

Of course, the capacity to express more aspects of what is supposed to matter about data is no use if it makes programming with that data more difficult. If dependent types were only a means to structure the extra effort required to make a program reliable, many people would rightly pass them by, preferring to trust to their judgment. There has to be some practical as well as moral benefit to saying more of what you mean in the type of a data structure or program---otherwise why bother? Epigram is a programming platform---a language equipped with mechanical support---designed to extract that practical benefit.

The Epigram language has already been set out in "The view from the left" (McBride & McKinna, JFP 14(1)), together with its explanation in terms of an underlying dependent type theory---Luo's UTT. In this course, we shall study not just programs in Epigram, but programming in Epigram, for dependent types do not only capture stronger properties of programs and data, they can express richer techniques for constructing them.

Epigram lives on the web at
http://www.dur.ac.uk/CARG/epigram


Last update 12 April 2004