[Prev][Next][Index][Thread]

Shape papers


[-------The Types Forum---------http://www.dcs.gla.ac.uk/~types-------]

The following papers on 

		SHAPE

may be of interest to type theorists, particularly the covariant
types.  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@socs.uts.edu.au

Reply-To: cbj21@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