Meeting a Fanclub: A Lattice of Generic Shape Selectors

Abstract

The "fan" of a datatype F is a relation that holds between a value x and an arbitrary F structure in which the only stored value is x. Fans make precise the notion of the shape of a data structure. We formulate two different representations of shape selectors and exploit the properties of fans to prove that the two representations are order isomorphic and that shape selectors are closed under set intersection. For arbitrary datatypes F, G and H, we consider six different ways of composing their fans in order to construct F structures of G structures of H structures; each of the six imposes a different requirement on the shape of the substructures. We catalogue the relation between different combinations of the constructions. We apply the result to a problem that arose in a generic theory of dynamic programming concerning the shape properties of a natural transformation from G structures to FG structures.