Inductive Families Need Not Store Their Indices

Edwin Brady, Conor McBride, James Mckinna

Research output: Chapter in Book/Report/Conference proceedingChapter

58 Citations (Scopus)


We consider the problem of efficient representation of dependently typed data. In particular, we consider a language TT based on Dybjer’s notion of inductive families [10] and reanalyse their general form with a view to optimising the storage associated with their use. We introduce an execution language, ExTT, which allows the commenting out of computationally irrelevant subterms and show how to use properties of elimination rules to elide constructor arguments and tags in ExTT. We further show how some types can be collapsed entirely at run-time. Several examples are given, including a representation of the simply typed λ-calculus for which our analysis yields an 80% reduction in run-time storage requirements.
Original languageEnglish
Title of host publicationTypes for Proofs and Programs. TYPES 2003
Number of pages15
ISBN (Electronic)9783540248491
ISBN (Print)9783540221647
Publication statusPublished - 2004
Event3rd Annual Workshop of the Types Working Group 2003 - Torino, Italy
Duration: 30 Apr 20034 May 2003

Publication series

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


Conference3rd Annual Workshop of the Types Working Group 2003
Abbreviated titleTYPES 2003


Dive into the research topics of 'Inductive Families Need Not Store Their Indices'. Together they form a unique fingerprint.

Cite this