Indexed Containers

11 years 11 months ago
Indexed Containers
The search for an expressive calculus of datatypes in which canonical algorithms can be easily written and proven correct has proved to be an enduring challenge to the theoretical computer science community. Approaches such as polynomial types, strictly positive types and inductive types have all met with some success but they tend not to cover important examples such as types with variable binding, types with constraints, nested types, dependent types etc. In order to compute with such types, we generalise from the traditional treatment of types as free standing entities to families of types which have some form of indexing. The hallmark of such indexed types is that one must usually compute not with an individual type in the family, but rather with the whole family simultaneously. We implement this simple idea by generalising our previous work on containers to what we call indexed containers and show that they cover a number of sophisticated datatypes and, indeed, other computational...
Thorsten Altenkirch, Peter Morris
Added 24 May 2010
Updated 24 May 2010
Type Conference
Year 2009
Where LICS
Authors Thorsten Altenkirch, Peter Morris
Comments (0)