ñòð. 10 |

An arrow or homomorphism of sketches F :

to the graph 0 for which, if D is a diagram in

morphism from the graph

then F Â± D lies in 0 ; if p : v Â¡ D is a cone in then F (p) is a cone in 0; and

!

0

if c : D Â¡ v is a cocone in

! then F (c) is a cocone in .

Note that if in the sketch the sets of diagrams, cones and cocones are all

to 0 is precisely a graph homomorphism from

empty, then an arrow from

to 0.

3.1.2 Example Let denote the impoverished sketch which has one node we

will call e and no arrows, diagrams, cones or cocones. Any assignment of e to a

node of any sketch is a morphism of sketches.

3.1.3 Example The sketch for graphs has the graph

source

aÂ¡ Â¡Â¡ n

Â¡Â¡!

Â¡Â¡Â¡

Â¡Â¡!

target

26

3.1 Homomorphisms of sketches 27

and no cones or diagrams. There is a graph homomorphism from the graph of the

sketch of 4.2.17 to the graph just given that takes 0 to a, 1 to n, and u to source.

This is a sketch homomorphism since there are no diagrams, cones or cocones

in either sketch. (Of course, there is another sketch homomorphism taking u to

target.)

3.1.4 Example In ES 2.1.4, we modifed the sketch for graphs by adding a cone

making it the sketch for simple graphs. The inclusion of the sketch for graphs into

the sketch for simple graphs is a homomorphism of sketches.

3.1.5 Example A Â¯eld has an associative binary operation of addition on it, so

one would suspect that there is a homomorphism from the sketch for semigroups

in 7.2.1 to the sketch for Â¯elds in ES 1.2. That is the case. The homomorphism

takes s to f , s Â£ s to f Â£ f and s Â£ s Â£ s to f Â£ f Â£ f , and the arrow c to the arrow

+. The homomorphism must take projection arrows of cones to corresponding

projection arrows, and of course the associativity diagram (7.8) then is mapped

to the diagram implied by FE{1 of ES 1.2.

3.1.6 The sketch underlying a category Let be a category. There is an

underlying sketch of , call it Sk( ), whose graph consists of the objects of

as nodes and the arrows of as arrows. This underlying sketch is not in general

Â¯nite or even small. The commutative diagrams of this sketch are all diagrams

that are commutative in . Similarly we take for cones all those that are limit

cones in and for cocones all those that are colimit cocones. An arrow from

to Sk( ) is then exactly what we have called a model of in in ES 2.4.2.

We note that although the composition in has been forgotten, it can be

completely recovered from the knowledge of which diagrams commute. For ex-

ample, the information f Â± g = h is equivalent to the information that

g-

Â¢ Â¢

@

h@ f

@

@?

R

Â¢

commutes so that we could recover the category entirely from the underlying

sketch (in fact, just from the graph and the commutative triangles).

3.1.7 The category of sketches With the deÂ¯nition of homomorphism of

sketches given above, sketches themselves form a category which we will call

Sketch. By restricting the shape graphs for the diagrams, cones and cocones

one obtains many full subcategories of Sketch, for example the category of FP

sketches, the category of FD sketches, and so on.

28 The category of sketches

One consequence of this is that all constructions that we can carry out in any

category make sense in the category of sketches. The particular construction that

interests us here is the formation of colimits, particularly pushouts.

3.1.8 Exercise

1. Let be the sketch with one node and no arrows, diagrams, cones or cocones.

Show that the category of models of in a category is isomorphic to . In

particular, the category of models of in Set is isomorphic to Set.

3.2 Parametrized data types

as pushouts

One thing a theory of data types should do is give a way of saying how the

data types of stacks of integers, say, is like the type of stacks of reals or for that

matter of stacks of arrays of trees of characters. In other words, we need a way

of talking about an abstract stack in a way that leaves it open to Â¯ll in the blank

corresponding to the thing that it is stacks of. The data type is the parameter.

The way we do this is to describe a sketch for stacks of d where d stands for

an abstract data type and then use a pushout construction to identify d with a

concrete data type in any particular application. The point is that pushouts are

the general way we use to identify things. We give several illustrations.

3.2.1 Abstract stacks Consider the sketch whose graph consists of nodes

s; t; d; d Â£ s and 1. The idea is that s stands for the set of stack conÂ¯gurations,

t the set of nonempty stack conÂ¯gurations, and d the data. There are operations

push : d Â£ s Â¡ t, pop : t Â¡ d Â£ s, empty : 1 Â¡ s and incl : t Â¡ s. In order to

! ! ! !

state the equations we also have two arrows iddÂ£s and idt which will be forced to

be identity arrows.

There are four equations (diagrams). Two of them, iddÂ£s = ()dÂ£s and idt = ()t ,

force those arrows to be identities, and the following two, which express the

essence of being a stack:

pop Â± push = iddÂ£s

and

push Â± pop = idt

There are the cones to express 1 as terminal and d Â£ s as a product, and one

cocone

1 t

@ Â¡

Â¡ incl

empty@

@ Â¡

@

R Â¡

Âª

s

3.2 Parametrized data types 29

So far, this sketch is not very interesting, since the type of d is still undetermined.

In fact its initial model I has I(d) = I(t) = ; and I(s) = femptyg. Note that

femptyg is not empty. It contains one element which we interpret as representing

the empty stack. Since the type d of data is empty, the empty stack is the only

kind of stack there is in the model I.

If there were constants in the data type d, then I(s) would be the set of all

possible conÂ¯gurations of a stack of data of type I(d), and I(t) would be the set

of all possible conÂ¯gurations other than the empty stack.

3.2.2 Stacks of natural numbers In 4.7.7, we described the sketch with two

nodes, 1 and n, two operations zero : 1 Â¡ n and succ : n Â¡ n. There are no

! !

equations (diagrams), just the cone describing 1 as terminal and no cocones.

This sketch, which we called Nat, has models that can be reasonably viewed as

describing natural numbers. We described a more elaborate sketch in ES 1.1.4

which could also be used in what follows.

Let us consider the following diagram in the category of sketches, where

is the trivial sketch deÂ¯ned in Example ES 3.1.2 and the arrows F and G are

deÂ¯ned by letting F e = n and Ge = d.

F-

Nat

(3.1)

G

?

Stack

A pushout of this diagram is a sketch Stack(Nat) made by forming the union

of Nat and Stack and then identifying the node n of Nat with the node d of

ñòð. 10 |