Container types categorically

Abstract

A program derivation is said to be polytypic if some of its parameters are data types. Often these data types are container types, whose elements store data. Polytypic program derivations necessitate a general, non-inductive definition of 'container (data) type'. Here we propose such a definition: a container type is a relator that has membership. It is shown how this definition implies various other properties that are shared by all container types. In particular, all container types have a unique strength, and all natural transformations between container types are strong.