altenkirch2009-indexed-containers

Abstract

We show that the syntactically rich notion of inductive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. Indexed containers generalize simple containers, capturing strictly positive families instead of just strictly positive types, without having to extend the core type theory. Other applications of indexed containers include datatype-generic programming and reasoning about polymorphic functions. The construction presented here has been formlized using the Agda system.

Introduction

Examples:

• Fin
• Untyped Lambda Calculus

Type Theoretic Preliminaries

Indexed Functors

$$\begin{array}{rl}(F_{\mathrm{Fin}}A{)}_n& :=\Sigma m:\mathbb{N}.(n=\mathrm{suc}m)\text{texttimes}(1+A_m)\\ (F_{\mathrm{Lam}}A{)}_n& :=\mathrm{Fin}n+A_n\text{texttimes}{A}_n+A_{\mathrm{suc}n}\end{array}$$

See also polynomial endofunctor

Initial Algebras of Indexed Functors

Indexed Container

Initial Algebra of Containers

Strictly Positive Families

Conclusions and Further Work

Paper