TY - GEN
T1 - A few constructions on constructors
AU - McBride, Conor
AU - Goguen, Healfdene
AU - McKinna, James
PY - 2006
Y1 - 2006
N2 - 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ôle in Epigram [25].
AB - 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ôle in Epigram [25].
UR - http://www.scopus.com/inward/record.url?scp=33745152658&partnerID=8YFLogxK
U2 - 10.1007/11617990_12
DO - 10.1007/11617990_12
M3 - Conference contribution
AN - SCOPUS:33745152658
SN - 9783540314288
T3 - Lecture Notes in Computer Science
SP - 186
EP - 200
BT - Types for Proofs and Programs. TYPES 2004
PB - Springer
T2 - International Workshop on Types for Proofs and Programs 2004
Y2 - 15 December 2004 through 18 December 2004
ER -