A program derivation is said to be polytypic if some of its parameters are data types. Polytypic program derivations necessitate a general non inductive definition of ‘data type’. Here we propose such a definition: a data type is a relator that has membership. It is shown how this definition implies various other properties that are shared by all data types. In particular, all data types have a unique strength, and all natural transformations between data types are strong.
|Name||Computing science reports|