Indexed families of types are a way of associating run-time data with
compile-time abstractions that can be used to reason about them. We
propose an extensible theory of indexed types, in which programmers can
define the index data appropriate to their programs and use them to
track properties of run-time code. The essential ingredients in our
proposal are (1) a logical framework, which is used to define index
data, constraints, and proofs, and (2) computation with indices, both at
the static and dynamic levels of the programming language. Computation
with indices supports a variety of mechanisms necessary for programming
with extensible indexed types, including the definition and
implementation of indexed types, meta-theoretic reasoning about indices,
proof-producing run-time checks, computed index expressions, and
run-time actions of index constraints.
Programmer-defined index propositions and their proofs can be
represented naturally in a logical framework such as LF, where variable
binding is used to model the consequence relation of the logic.
Consequently, the central technical challenge in our design is that
computing with indices requires computing with the higher-order terms of
a logical framework. The technical contributions of this paper are a
novel method for computing with the higher-order data of a simple
logical framework and the integration of such computation into the
static and dynamic levels of a programming language. Further, we
present examples showing how this computation supports indexed
programming.