Data Categories

C. Barry Jay
School of Computing Sciences, University of Technology, Sydney
cbj@socs.uts.edu.au

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 a data category. Since the category of sets is a data category, it follows that parametric polymorphism can have a set-theoretic model.

Conference Home Page