Introduction

Categories are often used to give an abstract view of programming language features. For example, most programming languages have a features such as tuples, records, or objects which allows data to be collected together. Different languages have different syntax, but by viewing the languages categorically, we can see what they have in common, and where there are important semantic differences. For example, in some languages records might correspond categorically to products, where in another they might correspond to monoidal structure. Looking at languages categorically allows us to concentrate on semantics rather than syntax.

Since Moggi's seminal paper on computational monads there has been much interest in the semantics of non-trivial computation, such as mutable state (Pitts), concurrency (Jeffrey), and I/O (Gordon). Power and Robinson have suggested premonoidal categories as an alternative presentation of computational monads, and in this paper we show how premonoidal categories provide a formal notion of data/control flow graphs for programs.

The presentation we adopt here is a slight variant of Power and Robinson's original presentation where we consider three categories, all with the same objects:

- V is a category of values, which are terms in normal form. It is a category with finite products.
- C is a category of central terms, which may have side-effects, but for which order of evaluation is unimportant. These terms might include nondeterminism, unique name generation, channel generation or new variable generation. For example, most of Pitts and Stark's nu-calculus might live in this category. It is a symmetric monoidal category.
- P is a category of processes, which are terms which may have arbitrary side-effects, including non-termination, assignment, concurrency or I/O. It is a symmetric premonoidal category.

These categories are included in each other:

V C P

These inclusions respect the product/monoidal/premonoidal structure of the three categories, and are the identity on objects.

This gives us enough structure to model simple expressions, but for more realistic examples we need to add functions and recursion. Functions are treated by adding adjunctions to the product/monoidal/premonoidal structure:

V[X, Y Z] V[X Y, Z]
V[X, Y Z] C[X Y, Z]
V[X, Y Z] P[X Y, Z]

Recursion is treated by allowing functions from P to be traced, in an adaptation of Joyal, Street and Verity's monoidal traced categories. This is similar to Hasegawa's use of traced monoidal categories to model recursive declarations, except that where he uses tracing in P to model call-by-name, we use tracing in V to model call-by-value.

We can give a syntactic presentation of these categories as a simple programming language, and a graphical presentation using mixed dataflow and controlflow graphs. This presentation is similar to Gardner's name-free presentation of Milner's control structures, and in the conclusion some ideas for future work are presented, showing how Milner's operational semantics for control structures might be adapted to the premonoidal setting.

Previous | Next