Inductive Families Need Not Store Their Indices

Edwin Brady, Conor McBride, James McKinna

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

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 languageUndefined/Unknown
Title of host publicationTypes for Proofs and Programs, International Workshop, TYPES 2003
Subtitle of host publicationTorino, Italy, April 30 - May 4, 2003, Revised Selected Papers
Place of PublicationBerlin
PublisherSpringer Berlin
Pages115-129
Number of pages15
Volume3085
ISBN (Electronic)978-3-540-24849-1
ISBN (Print)978-3-540-22164-7
DOIs
Publication statusPublished - 2004
EventTypes for Proofs and Programs: International Workshop TYPES 2003 : Torino, April 30 - May 4, 2003 Selected Papers - Torino, Italy
Duration: 30 Apr 20034 May 2003
Conference number: 9
https://link.springer.com/conference/types

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume3085

Conference

ConferenceTypes for Proofs and Programs: International Workshop TYPES 2003
Abbreviated titleTYPES 2003
Country/TerritoryItaly
CityTorino
Period30/04/034/05/03
Internet address

Keywords

  • Type Theory
  • Dependent Type
  • Functional Language
  • Elimination Rule
  • Alternative Implementation

Cite this