A few constructions on constructors

Conor McBride*, Healfdene Goguen, James McKinna

*Corresponding author for this work

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

13 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ôle in Epigram [25].

Original languageEnglish
Title of host publicationTypes for Proofs and Programs. TYPES 2004
Number of pages15
ISBN (Electronic)9783540314295
ISBN (Print)9783540314288
Publication statusPublished - 2006
EventInternational Workshop on Types for Proofs and Programs 2004 - Jouy-en-Josas, France
Duration: 15 Dec 200418 Dec 2004

Publication series

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


ConferenceInternational Workshop on Types for Proofs and Programs 2004
Abbreviated titleTYPES 2004

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


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

Cite this