A Few Constructions on Constructors

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ˆole in Epigram [25].

• Type: Conference
• Year: 2004
• Where: TYPES
• Authors: Conor McBride, Healfdene Goguen, James McKinna
• Keywords: Constructions, Formal Methods, Inductive Datatype, Pattern Matching Style, TYPES 2004