Inductive Families Need Not Store Their Indices

Edwin Brady, Conor McBride, James Mckinna

Research output: Chapter in Book/Report/Conference proceedingChapter

44 Citations (Scopus)

Abstract

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
PublisherSpringer
Pages115-129
Number of pages15
ISBN (Electronic)9783540248491
ISBN (Print)9783540221647
DOIs
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
Volume3085
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd Annual Workshop of the Types Working Group 2003
Abbreviated titleTYPES 2003
CountryItaly
CityTorino
Period30/04/034/05/03

Cite this

Brady, E., McBride, C., & Mckinna, J. (2004). Inductive Families Need Not Store Their Indices. In Types for Proofs and Programs. TYPES 2003 (pp. 115-129). (Lecture Notes in Computer Science; Vol. 3085). Springer. https://doi.org/10.1007/978-3-540-24849-1_8