|
Abstract : |
Data categories and functors, and the strong natural transformations between them provide a universe in which to model parametric polymorphism. Data functors are distinguished by being decomposable into shape and data, i.e. they represent types that store data. Every strong transformation between two such is given by a uniform algorithm, and so may represent a polymorphic term. The data functors are closed under composition, finite products and sums, exponentiation by an object, final co-algebras and initial algebras. For any two such, the collection of strong natural transformations between them is representable by an object. The covariant type system supports parametric polymorphism on data types, and can be modelled in, |
