PAUL HOOGENDIJK a1andOEGE DE MOOR a2 a1 Philips Research Laboratories, Prof. Holstlaan 4, 5656 AA Eindhoven, The Netherlands a2 Programming Research Group, Oxford University, Wolfson Building, Parks Road, Oxford OX1 3QD, UK
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.
