A few constructions on constructors

C McBride, H Goguen, J McKinna

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

11 Citations (Scopus)


We present four constructions for standard equipment which can be generated for every inductive datatype: case analysis, structural recursion, no confusion, acyclicity. Our constructions follow a two-level approach-they require less work than the standard techniques which inspired them [11, 8]. Moreover, given a suitably heterogeneous notion of equality, they extend without difficulty to inductive families of datatypes. These constructions are vital components of the translation from dependently typed programs in pattern matching style [7] to the equivalent programs expressed in terms of induction principles [21] and as such play a crucial behind-the-scenes r (o) over cap le in Epigram [25].
Original languageEnglish
Title of host publicationTypes for Proofs and Programs
Number of pages15
ISBN (Electronic)978-3-540-31428-8
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'A few constructions on constructors'. Together they form a unique fingerprint.

Cite this