Authors: Neil Ghani, Thorsten Altenkirch, Tarmo Uustalu, Michael Abbott
Title: Higher Order Datatypes Via Containers
Abstract: 
Type systems of functional languages such as Haskell permit the
definition of sophisticated datatypes incorporating advanced features
such as variable binding and structural constraints. Classic examples
of these phenomena are lambda calculus syntax, explicit substitutions
and balanced trees. However, the traditional presentation of such
datatypes hides the fact that they are concrete data structures in
that they store data in certain locations. This is unfortunate as a
number of algorithms specifically exploit this structure.

We rectify the situation by showing that a wide class of nested
datatypes (inductive constructors of rank 2) are examples of our
recently introduced idea of containers. The direct pay off for this is
that we can then show how algorithms, eg Huet's zipper, which rely on
the storage of data at locations can be generalised to such datatypes.