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...

• Type: Conference
• Year: 2004
• Where: AFP
• Authors: Conor McBride
• Keywords: AFP 2004, Familiar Type Systems, Programs Inspect Data, ‘software Engineering