Sciweavers

Share
TYPES
2004
Springer

A Few Constructions on Constructors

10 years 3 months ago
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].
Conor McBride, Healfdene Goguen, James McKinna
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where TYPES
Authors Conor McBride, Healfdene Goguen, James McKinna
Comments (0)
books