Epigram: Practical Programming with Dependent Types

11 years 2 months ago
Epigram: Practical Programming with Dependent Types
Abstraction and application, tupling and projection: these provide the ‘software engineering’ superstructure for programs, and our familiar type systems ensure that these operations are used compatibly. However, sooner or later, most programs inspect data and make a choice—at that point our familiar type systems fall silent. They simply can’t talk about specific data. All this time, we thought our programming was strongly typed, when it was just our software engineering. In order to do better, we need a static language capable of expressing the significance of particular values in legitimizing some computations rather than others. We should not give up on programming. James McKinna and I designed Epigram [27, 26] to support a way of programming which builds more of the intended meaning of functions and data into their types. Its style draws heavily from the Alf system [13, 21]; its substance from my to Randy Pollack’s Lego system [20, 23] Epigram is in its infancy and its i...
Conor McBride
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where AFP
Authors Conor McBride
Comments (0)