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  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.
|Name||Lecture Notes in Computer Science|
|Conference||3rd Annual Workshop of the Types Working Group 2003|
|Abbreviated title||TYPES 2003|
|Period||30/04/03 → 4/05/03|