Categories

Download

categories-list@categories.org.au

October 1995

1 participants
1 discussions

Shape papers
by Barry Jay 31 Oct '95

31 Oct '95

The following papers on SHAPE may be of interest to category theorists and computer scientists. The titles are: "A semantics for shape" shape_semantics.ps.Z "Data categories and functors" datacats.dvi.Z "Covariant types" covtypes.dvi.Z "Polynomial Polymorphism" (in directory P2) "Type-free term reduction for covariant types" typefree.dvi.Z "Shape analysis for parallel computing" parshape.dvi.Z All are available by anonymous ftp from ftp.socs.uts.edu.au in the directory Users/cbj *Some* can be acessed from my www home page at http://linus.socs.uts.edu.au/~cbj The rest of this message describes the main results of the papers, and some of the goals of the Shape project. Barry Jay University of Technology, Sydney cbj(a)socs.uts.edu.au Reply-To: cbj21(a)newton.cam.ac.uk (until 30/11/95) A semantics for shape ===================== The basic observation behind shape theory is that most of the functors F used to model data types share a common characteristic; they have a cartesian natural transformation into a functor used to store unstructured data. In the simplest case, the latter is the list (or free monoid) functor: data: F => L The main result of this paper is that in a locos (an extensive category with all finite limits and lists) all functors shapely over lists are closed under the formation of initial algebras. The proof is constructive - simply build a parser for the initial algebra, using the existing lists and pullbacks. Data categories and functors ============================ The functors which are cartesian over lists are good for handling first order structures, but they are not closed under exponentiation, and so are inadequate for higher-order types. This defect is remedied by changing the functor used to store data from lists to a *position functor* given by an object of positions P. Such a functor maps an object A to the object P --> A+1 . A *data functor* is a functor F with a given cartesian transformation to such a position functor. Now, for any object X the functor which maps A to the object X --> FA is also a position functor, with object of positions XxP. The key result about data functors is that every natural transformation between two such is given by a uniform, or parametric natural transformation. More precisely, if F is a data functor with object of positions P, and G is a data functor, then every natural transformation F ==> G is determined by a morphism F1 --> GP This fact makes the data functors suitable for modelling higher types. Covariant Types =============== The data categories, in which the theory of data functors is developed, include the usual semantic categories, such as Sets, and bottomless c.p.o.'s. However, Reynolds proved that "Polymorphism is not set-theoretic" by showing that the second-order polymorphic lambda calculus (system F) has no set-theoretic models. This leads us to ask what kind of polymorphism is modelled by the data functors. This leads to the covariant type system in which function types are replaced by *transformation types*. The system is strong enough to capture the usual polymorphism of lists and trees, while still having set-theoretic models. Thus, Polymorphism *can* be set-theoretic Polynomial Polymorphism ======================= As a sub-system of F, the covariant types do not capture functoriality. For shape (or functorial) polymorphism to make sense, there must be a polymorphic algorithm for evaluating the action of functors on morphisms, i.e. a polymorphic map. Such an algorithm was first developed in the type system P2, as described in the following paper. Type-free term reduction for covariant types ============================================ A generic algorithm for mapping requires the detection of the data to which the mapped function must be applied. One method of doing this is to *tag* the data using a single system of tags appropriate for all the functors under discussion. A naive approach leads to the tagged types of this paper. Functorial types ================ Current work aims to have functors represented directly by types so that, for example, composition of functors is a primitive operation on types. This is intended to extend the notion of category theory as a programming technique. Shape analysis for parallel computing ===================================== While shape polymorphism allows us to "ignore" the shape, shape analysis uses detailed shape information to improve errr detection and compilation. This is particularly important in parallel programming, where the shape of the data structures, and their distribution, are central concerns. This paper presents a survey of the issues, and a computational paradigm, that will be developed by the Algorithms and Languages Group University of Technology, Sydney http://linus.socs.uts.edu.au/~shape

1 0