Computational Comonads
and Intensional Semantics
Stephen Brookes
Shai Geva
October 1991
CMU-CS-91-190

School of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213

This research was supported in part by National Science Foundation grant CCR-9006064 and in part by
DARPA/NSF grant CCR-8906483.
The views and conclusions contained in this document are those of the authors and should not be interpreted as
representing the ocial policies, either expressed or implied, of NSF, DARPA or the U.S. government.

Keywords: theory, applicative (functional) programming, semantics, parallelism, category

theory, lazy evaluation

Abstract
We explore some foundational issues in the development of a theory of intensional semantics. A
programming language may be given a variety of semantics, di ering in the level of abstraction; one
generally chooses the semantics at an abstraction level appropriate for reasoning about a particularkind of program property. Extensional semantics are typically appropriate for proving properties
such as partial correctness, but an intensional semantics at a lower abstraction level is requiredin order to reason about computation strategy and thereby support reasoning about intensional
aspects of behavior such as order of evaluation and eciency. It is obviously desirable to be able toestablish sensible relationships between two semantics for the same language, and we seek a generalcategory-theoretic framework that permits this.
Beginning with an \extensional" category, whose morphisms we can think of as functions of somekind, we model a notion of computation as a comonad with certain extra structure and we regard theKleisli category of the comonad as an intensional category. An intensional morphism, or algorithm,
can be thought of as a function from computations to values. This view accords with a lazyoperational interpretation of programs. Under certain rather general assumptions the underlying
category can be recovered from the Kleisli category by taking a quotient, derived from a congruence
relation that we call extensional equivalence. We then focus on the case where the underlying
category is cartesian closed. Under further assumptions the Kleisli category satis es a weak formof cartesian closure: application morphisms exist, currying and uncurrying of morphisms makesense, and the diagram for exponentiation commutes up to extensional equivalence. When theunderlying category is an ordered category we identify conditions under which the exponentiation
diagram commutes up to an inequality. We illustrate these ideas and results by introducing somenotions of computation on domains and by discussing the properties of the corresponding categoriesof algorithms on domains.

1 Introduction
Most existing denotational semantic treatments of programming languages are extensional, in thatthey abstract away from computational details and ascribe essentially extensional meanings toprograms. For instance, in the standard denotational treatment of imperative while-programs themeaning of a program is taken to be a partial function from states to states; and in the standard
denotational model of the simply typed -calculus, the meaning of a term of function type is taken
to be a continuous function. Extensional models are appropriate if one wants to reason only about
extensional properties of programs, such as partial correctness of while-programs. However, suchmodels give no insight into questions concerning essentially intensional aspects of program behavior,such as eciency or complexity. For instance, in a typical extensional model all sorting programs
denote the same function, regardless of their computation strategy, and therefore regardless of
their worst- or average-case behavior. It is desirable to have a semantic model in which sensible
comparisons can be made between programs with the same extensional behavior, on the basis of
their computation strategy.
We emphasize that we regard intensionality as a relative term; given a programming language
we might wish to provide an extensional semantics and also an intensional semantics that contains
more computational information and is thus at a lower level of abstraction. We would like to beable to extract extensional meanings from intensional meanings, and to show that the intensionalsemantics \ ts properly" on top of the extensional semantics. Suppose that we have an extensionalsemantics provided in a category whose objects represent sets of data values and whose morphisms
are functions of some kind; and that we have an intensional semantics in a category with thesame objects but with morphisms that we regard as algorithms, which correspond to functions
equipped with a computation strategy. It seems reasonable that we should be able to de ne anequivalence relation on algorithms (in the same hom-set) that identi es all pairs of algorithms withthe same \extensional part"; that composition of algorithms should respect this equivalence; andthat quotienting the algorithms from A to B by this equivalence relation should yield precisely theextensional morphisms.
In this paper we set out a basis for a category-theoretic approach to intensional semantics,
motivated by the following intuition. If the extensional meaning of a program may be modelled assome kind of function from data values to data values, then we can obtain an intensional semantics
by introducing a notion of computation and de ning an intensional meaning to be a function fromcomputations to values. This accords with an intuitive operational semantics for programs in which
the execution of a program proceeds lazily in a coroutine-like manner [10]: the program responds
to requests for output (say, from a user) by performing input computation until it has sucient
information to supply an output value. We formalize what we mean by a notion of computation in
abstract terms as follows. Suppose that extensional meanings are given in some category C . Then,for each object A, we specify an object TA of computations over A and we specify how to lift amorphism f from A to B into a morphism Tf from TA to TB ; we require that T be a functor on
C . We specify, for each object A, a morphism A : TA ! A from computations to values and amorphism A : TA ! T 2 A that maps a computation over A to a computation over TA. Intuitively,
 maps a computation to the value it computes, and  shows how a computation may itself becomputed. We require that (T; ; ) be a comonad over C . Then we regard the Kleisli category ofthis comonad as an intensional category; it has the same objects as C , and an intensional morphismfrom A to B is just a morphism in C from TA to B .
We say that a comonad is computational if there is a natural way to convert a data value intoa degenerate computation returning that value. This enables us to extract from an algorithm a1

function from values to values, and we obtain an extensional equivalence relation on algorithms byidentifying all pairs of algorithms that determine the same function. We show that if the comonadis computational then the Kleisli category collapses onto C under extensional equivalence.
We then show that, assuming certain further conditions concerning products, the Kleisli category satis es an intensional analogue of the cartesian closedness property. This generalizes fromthe known result that if the underlying category is cartesian closed and the (functor part of the)comonad preserves products then the Kleisli category is also cartesian closed. When the underlying category C is an ordered category, we identify conditions under which the Kleisli construction
preserves certain lax forms of cartesian closedness.
Throughout the paper we motivate our de nitions and results by means of notions of computation on domains. We focus primarily on three forms of computation at di ering levels of
abstraction. At the end of the paper we discuss brie y some further examples that indicate thebroader applicability of our ideas.
We assume familiarity with elementary category theory and domain theory. We refer the reader
to [11] and [1] for categorical background and to [8] for the relevant domain theory.

2 Computations, Comonads and Algorithms
Let C be a category that we regard as providing an extensional framework. We wish to encapsulate in abstract terms what a notion of computation over C is, and to build an \intensional"
category whose morphisms can be thought of as extensional morphisms equipped with additional
computational information. We model a notion of computation over C as a comonad over C , thefunctor part of which maps an object A to an object TA representing computations over A. The
two other components of the comonad describe how to extract a value from a computation, andhow a computation is built up from its sub-computations. We then take an intensional morphismfrom A to B to be an extensional morphism from TA to B , essentially a morphism from input
computations over A to output values in B . This leads us to use for our intensional category the
Kleisli category CT [11], which has the same objects as C and in which the morphisms from A to
B are exactly the C-morphisms from TA to B . Typically C is a category in which morphisms arefunctions of some kind, and we will refer to intensional morphisms in CT as algorithms to emphasize
their computational content. In case we need to compare Kleisli categories for di erent comonads over the same underlying category we will use the term T -algorithm, indicating the comonad
explicitly.

2.1 Comonads and the Kleisli category
De nition
2.1 A comonad over a category C is a triple (T; ; ) where T : C !: C is a functor,:

 : T ! IC is a natural transformation from T to the identity functor, and  : T ! T 2 is a naturaltransformation from T to T 2, such that the following associativity and identity conditions hold, forevery object A:
T (A )  A = TA  A
TA  A = T (A )  A = idTA :Figures 1 and 2 express these requirements in diagrammatic form.
De nition 2.2 Given a comonad (T; ; ) over C , the Kleisli category CT is de ned by:
2

Tf

TA

-

TB

TA

B

A

?

T 2A

A
?

A

f

-

Tf

TB
B

?

B

-

T 2f

-

?

T 2B

Figure 1: Naturality of  and  in a comonad: these diagrams commute, for all A, B , f : A !C B .

TA 

@
I
@

TA

T 2A

TA

A

idTA@

@

@
@
@

TA



6

@
@

-

TA

A

-

A

idTA

TA
?

T 2A

TA

T 2A

TA

-

?

T 3A

Figure 2: Identity and associativity laws of a comonad: these diagrams commute, for all A.

 The objects of CT are the objects of C .
 The morphisms from A to B in CT are the morphisms from TA to B in C.
 The identity morphism idb A on A in CT is A : TA !C A.
 The composition in CT of a : A !CT B and a0 : B !CT C, denoted a0  a, is the composition
in C of A : TA !C T 2 A, Ta : T 2 A !C TB and a0 : TB !C C , i.e.,a0  a = a0  Ta  A :The associativity and identity laws of the comonad ensure that CT is a category [11].

This use of morphisms from TA to B to model algorithms from A to B ts well with an intuitive
operational semantics based on the coroutine mechanism [10]. A program responds to requests for
output by performing some computation on its input (typically, to evaluate some portion of the
input) until it has enough information to determine what output value to produce. Execution islazy, in that computation is demand-driven. The operational behavior of algorithm composition
can be described as follows. Let a : A !CT B and a0 : B !CT C . Then a0  a responds to arequest for output (in C ) by performing an input computation t over A, transforming this into a
computation t0 over B by applying a to the pre xes of t, and supplying t0 as argument to a0 . For
further details concerning operational semantics we refer to [5].
33 Notions of computation on domains
Our main examples will be based on a category of domains and continuous functions. To avoid
repetition and to be precise, let us remark that by a domain we mean a directed-complete, boundedcomplete, algebraic partial order with a least element. That is, a domain (D; v) is a set D equippedwith a partial order v satisfying the following conditions: D has a least element, denoted ?D .
 Every non-empty directed subset X  D has a least upper bound F X .
 Every non-empty bounded (or consistent) subset X  D has a least upper bound F X .
 Every element of D is the least upper bound of its (directed set of) nite approximations.
A set X is directed i for all x; y 2 X there is a z 2 X such that x v z and y v z . A set X isbounded i there is a z 2 D suchthat x v z for all x 2 X . An element e 2 D is nite i , for allF
directed subsets X  D, if e v X then e v x for some x 2 X .
We remark that none of our example comonads really requires that the underlying domain be
algebraic, and nor does the presence of a least element play any prominent r^ole (except, of course,
in justifying the existence of least xed points). We could just as well work in the category of
directed-complete, bounded complete partial orders and continuous functions. Nevertheless, theproperty of algebraicity is very natural in the computational setting and all of our example functors
on domains preserve algebraicity. At the end of the paper we will discuss further examples basedon di erent categories and di erent types of domain.

3.1 Increasing paths

The rst notion of computation that we introduce models in abstract terms a sequence of time
steps in which some incremental evaluation is being performed. For example, a program with two
inputs may need to evaluate one or more of its input arguments and it may attempt to perform
evaluations in parallel or in sequence; moreover, it may only require partial information about its
arguments, as is typically the case, say, when an argument is a function and the program needs
to apply that argument to an already known parameter. One natural way to formalize this formof computation is as an increasing sequence of values drawn from a domain, whose partial orderre ects the amount of information inherent in a value.
We de ne the comonad T1 of \increasing paths" as follows1.

 For a given domain (D; v), let T1D be the set of nite or in nite increasing sequences overD, ordered componentwise. For convenience we represent a nite sequence as an eventuallyconstant in nite sequence. Thus, the elements of T1 D have form hdn i1
n=0 , where for each101n  0, dn v dn+1; and we de ne hdnin=0 vT1D hdnin=0 i for all n  0, dn vD d0n.
 For a continuous function f : D ! D0, let T1f : T1D ! T1D0 be the function that applies f
1
componentwise. That is, (T1f )hdn i1
n=0 = hfdn in=0 .
 For t 2 T1D let D t be the least upper bound of t. That is, hdni1n=0 = F1n=0 dn.
1This comonad, adapted for Scott domains, was rst introduced in [4].

4h>; >i@h>; ?ih?; >i@@h?; ?iFigure 3: The domain Two  Two.

 For t 2 T1D let D t be the sequence of ( nite) pre xes of t. That is, if t = hdni1n=0, then foreach n  0, (t)n = d0 . . . dn d!n .
Intuitively, a computation may be viewed as a (time-indexed) sequence of increments in the amountof information known about a data value, and the value \computed" by such a computation is its
least upper bound; each computation is itself built up progressively from its pre xes. Equivalently,
we can regard a computation over D as a continuous function from the domain VNat of \vertical" natural numbers (together with limit point ! ) to D. Our ordering on computations thencorresponds exactly to the pointwise ordering on such functions.
The least element of T1D is the sequence ?! . The nite elements of T1D are just the eventuallyconstant sequences all of whose elements are nite in D. It is easy to verify that T1 maps domains todomains and is indeed a functor. The comonad laws hold: naturality of  corresponds to continuityof f ; naturality of  states that the operation of applying a function componentwise to a sequence\commutes" with taking pre xes; every computation is the least upper bound of its pre xes; andevery pre x of a pre x of t is also a pre x of t.
For illustration, let Two be the domain f?; >g. The domain Two  Two is shown in Figure 3,
and Figure 4 shows the six continuous functions from Two  Two to Two, ordered pointwise. We givethese functions mnemonic names: ? and > are constant functions; l is strict in its left argument;r is strict in its right argument; b is strict in both arguments; poll returns > if either of its twoarguments is >, so that poll is not strict in either argument. Each function is depicted by a Hasse
diagram corresponding to Figure 3, in which the nodes are shaded to indicate their image under
the function being described:  corresponds to ?,  to >.
Figure 5 shows part of T1(Two  Two). Figure 6 shows some of the T1-algorithms from Two  Two
to Two, ordered pointwise. The notation for describing algorithms is based on Figure 5, again
with  representing ? and  representing >. In each case the intended algorithm is the least
continuous function on paths consistent with this description. The nomenclature is intended toindicate (as yet only informally) the function computed by each algorithm and what computation
strategy the algorithm uses. For instance, the algorithms pb, lb, rb and db all compute the functionb; pb computes both arguments in parallel immediately, lb computes left- rst and then right, rb
computes right- rst and then left, and db computes both arguments in either order. Since thediagram includes only one algorithm for poll, for ?, and for >, in these cases we use the same namefor the algorithm as for the function.
Since T1 (Two  Two) includes paths with repeated steps, we can also make distinctions between
algorithms which di er not in the order in which they evaluate their arguments, but in the amountof time they are prepared to wait for each successive increment to be achieved. For instance, forthe function b there are algorithms pbn , lbn , rbn and dbn for each n  0, characterized as the least

5

'$
&
%
'$
&
%
'$ '$
& %' $& %
&
%
'$
&%




@
@





@



@

@
@

>

@

 poll







@



@
@

l



@
@





@
@

@
@

b

@

?

@

@
@

r









@





Figure 4: Continuous functions from Two  Two to Two, ordered pointwise.

h>; >i!

""bbh>; ?i h>; >i!

h?; >i h>; >i!

h>; ?i!

h?; >i!

bb""h?; ?i!

Figure 5: Some paths in T1(Two  Two):
6

'$
&' %$
' $& %' $' $& %' $& %' $& %' $& %' $& %& %' $& %
&' %$
&%

" b
b "



" b





"

b

"

b

@





pl

@



sl

b "

@

@



"

b

poll

b "

@

b " 

@



>

"

b

"
"



db



lb

@

pr

@

@

b " 

@



b

b "

@

b "
 @



b


" b
b "



" b
b "


"
"

b


" b
b " 




b

b "


sr

rb

pb

?

Figure 6: Some T1-algorithms from Two  Two to Two, ordered pointwise.

7

functions on paths such thatpbn (h?; ?in h>; >i! ) = >lbn (h?; ?in h>; ?i h>; ?in h>; >i! ) = >rbn (h?; ?in h?; >i h?; >in h>:>i! ) = >dbn (h?; ?in h>; ?i h>; ?in h>; >i! ) = >dbn (h?; ?in h?; >i h?; >in h>; >i! ) = >:Informally, pbn is the algorithm which needs to evaluate both arguments and returns > provided
each evaluation succeeds (with result >) in at most n time steps. Similarly, lbn evaluates botharguments and returns > provided evaluation of the left argument succeeds in at most n time steps
and evaluation of the right argument succeeds in at most 2n + 1 time steps.
The following relationships hold, for all n  0:
pbn v lbn v pb2n+1
pbn v rbn v pb2n+1
dbn = lbn t rbn :Moreover, pbn v pbn+1 , lbn v lbn+1 , rn v rn+1 , and dbn v dbn+1 for all n  0. Each of thesesequences of algorithms has the same least upper bound, characterized as the algorithm b thatmaps every path with lub h>; >i to >. Of course, in Figure 6, pb is just pb0 , and so on.

3.2 Strictly increasing paths

In the comonad T1 a computation has a built-in measure of the number of time steps it takes between
successive proper increments. We obtain a more abstract notion of computation by retaining only
the increments themselves, so that we may still make distinctions on the basis of the order of
evaluation of arguments. To do this we model a computation as a \strictly increasing path". We
de ne the strictly increasing path comonad T2 as follows.
 Let T2D be the set of nite or in nite strictly increasing sequences over D. Again, forconvenience, we represent a nite sequence as an eventually constant in nite sequence. Thatis, the elements of T2D are either of form hdn i1
n=0 , with dn @D dn+1 for all n  0; or of form!
d0 . . . dN 1 dN , where N  0 and dn @D dn+1 for 0  n < N . Let vT2D be the least partial
order on T2D such thatd0 . . . dN 1d!N vT2D d0 . . . dN 1 t if t 2 T2D & dN vD t0:
This ordering is based on the pre x ordering on sequences, but adjusted to take appropriate account of the underlying order on data values. The order vT2 D is actually the stableordering [2] on T2 D, when we regard the elements of T2D as (strictly increasing, possibly
eventually constant) stable functions from VNat to D. Note that every continuous function
from VNat to D is also stable.
 For a continuous function f : D ! D0 we de ne T2f to be the function which applies fcomponentwise and suppresses any repetitions (except for constant suxes). That is, T2f is
the least continuous function such that for all d 2 D, for all d0 ; d1 2 D such that d0 @ d1, andfor all t 2 T2D,
T2f (d!) = (fd)!
T2f (d0d1t) = (fd0)(T2f (d1t))
if fd0 6= fd1= T2 f (d1t)
if fd0 = fd1:8

h>; ?i h>; >i! h?; >i h>; >i!
h>; >i!
%%

%

ee
e

%

e

h>; ?i!

h?; >i!

bb""h?; ?i!

Figure 7: Part of T2(Two  Two).

 For all t 2 T2D, let D t be the lub of t. That is, hdni1n=0 = F1n=0 dn .
 For all t 2 T2D, let D t be the sequence of pre xes of t. Again, if t = hdni1n=0 then for eachn  0, (t)n = d0 . . . dn d!n. Note that if t is strictly increasing, so is t.
The least element of T2 D is the sequence ?! . The lub of a directed (or consistent) set of strictlyincreasing paths is again a strictly increasing path2. The nite elements of T2 D are the eventuallyconstant sequences of form hd0 . . . dN 1 id!N , where N  0 and dN is a nite element of D. Every element of T2 D is the lub of its nite approximations. Thus, T2 maps domains to domains.

Functoriality is easily checked.
Although the order is not pointwise, it is still true that every t 2 T2D is the lub of its pre xes.
The comonad laws hold for (T2; ;  ).
Figure 7 shows some of the paths in T2(Two  Two). Figure 8 shows some of the T2 -algorithms
from Two  Two to Two, ordered pointwise, using a notation based on Figure 7. Again the nomenclature is chosen to indicate the function computed and the computation strategy. Each of theT1-algorithms of Figure 6 has a corresponding T2-algorithm, for which we use the same name; but
because of the di erent ordering on paths, there are three additional T2-algorithms. Note also thatsince T2D does not include paths with repeated elements, only pb0 and pb1 of the family of pbn
algorithms de ned above have corresponding T2 -algorithms.

3.3 Timed data

A simple notion of computation over domains is obtained by regarding a computation as a pairconsisting of a data value and a natural number, intuitively representing the amount of time or
the cost associated with the calculation of the value. With this intuitition it seems reasonable toregard one computation hd; ni as approximating another hd0; n0 i i d v d0 and n0  n; that is, abetter computation produces a more precise data value in less time. This suggests the use of thefollowing comonad: T3D = D  VNatop, ordered componentwise.
 For f : D ! D0, (T3f ) hd; ni = hfd; ni.
  hd; ni = d.
However, this would not be the case if we ordered T2 D componentwise, since T2 D is not directed-complete under
the componentwise ordering.
2

9

'$
&
%
'$
&
%
' $' $&%&%' $' $' $&' %$&%&%' $' $&' %$&%&%' $' $
& %&
%
&
%
'$
&%

 J >JH  J  poll
J
H 






TT


 J  prJH  J  pl
J
H 






TT





TT

 J  sl  J  db
J
J
H 
H 
 l

,
,

l
l

l
,
, l

l
,
, l

,


 J  sr
J
H 





 J  lb  J  d?  J  rb
J
J
J
H 
H 
H 
 l ,  l ,  J  l?
J
H 

@
@


 J  pb
J
H 



 J  r?
J
H 


@
@


 J ?
JH 


Figure 8: Some T2-algorithms from Two  Two to Two, ordered pointwise.

10  hd; ni = hhd;ni ; ni.
Here VNatop is the domain consisting of the natural numbers together with ! , ordered by thereverse of the usual ordering, so that ! is the least element. The least element of T3D is h?D ; ! i.
We may de ne for each continuous function f : D ! D0 and each n 2 VNat an algorithm fn
from D to D0 :fn hd; ki = fd
if k  n= ?
otherwise:
Clearly, whenever f v g we also get fn v gn . Moreover, because of our ordering on T3D, we
get fn v fn+1 for each n  0; and f! is simply  hd; ni :fd. The lub of the fn is the functionf =  hd; ni :(n = ! ! ?; fd); which is below f! . Using this nomenclature, we show some of theT3-algorithms from Two  Two to Two in Figure 9.
It is also possible to de ne a comonad based on the functor TD = D  VNat, using the usual
ordering on the integer component.

4 Relating algorithms and functions
4.1 Computational comonads

We will say that a comonad is computational if for each object A, every data value in A canbe regarded as a \degenerate" computation in TA, and degenerate computations possess certain
simple properties. This permits us to extract from an algorithm a function from values to values,
by looking at the algorithm's e ect when applied to degenerate computations. Two algorithms arecalled extensionally equivalent i they determine the same function.
More precisely, we require the existence of a natural transformation : IC !: T satisfying someaxioms which capture formally what we mean by degeneracy. We then show that this permits us
to de ne an \extensional equivalence" relation on each hom-set in CT . Extensional equivalence ispreserved by composition, so that we actually have a congruence on CT . The underlying category
C may then be recovered from CT by taking a quotient.

De nition 4.1 A computational: comonad over a category C is a quadruple (T; ; ; ) where (T; ; )
is a comonad over C and : IC ! T is a natural transformation such that, for every object A, A  A = idA A  A = TA  A.
Naturality guarantees that, for every morphism f : A !C B , Tf  A = B  f .
Figure 10 shows these properties in diagrammatic form.

As an immediate corollary of these properties, A is epi and A is mono, for every object A.

Proposition 4.2 If (T; ; ; ) is a computational comonad, then there is a pair of functors (alg; fun)between C and CT with the following de nitions and properties:

 alg : C ! CT is the identity on objects, and alg(f ) = f  A , for every f : A !C B .
11

>!

 >
 
 >
n+1
 


   >n 

poll!  

l!

@

l @@
@

@

ln+1 @@ @

@ 
 
poll@@@@polln+1@@ @@ @ @
polln @@ @ @@@@@ @@ @ @ r@ !
@@ @@ @
r
@
@ @@
@
r
@ n+1
@

@
@
@ @
ln @ @ @@
@
@
@
@ @
@
@
@
@ b!
@ @
@
@ @@ b @@ @@ bn+1@rn

bn?
Figure 9: Some T3-algorithms from Two  Two to Two, ordered pointwise.

12

idA

A

A
A

A
A
AA


A

A

AAU 

TA

-

A




A



A

A

-

TA

A

A

A

A
?

TA

TA

-

?

T 2A

f

-

B
B

?

TA

Tf

-

?

TB

Figure 10: Properties of a computational comonad: these diagrams commute, for all A, B , and allmorphisms f : A !C B .

 fun : CT ! C is the identity on objects, and fun(a) = a  A, for all a : A !CT B .
 fun induces an equivalence relation =e on CT , given by a1 =e a2 () fun(a1) = fun(a2):This relation is a congruence; that is, for all a1 ; a2 : A !CT B and a01 ; a02 : B !CT C ,a1 =e a2 & a01 =e a02 ) a01  a1 =e a02  a2:

 The quotient category of CT by =e is isomorphic to C.
 fun  alg = IC . That is, for all f : A !C B , fun(alg f ) = f .
 alg  fun =e ICT , in that for all a : A !CT B, alg(fun a) =e a.

Proof: Functoriality of alg and fun are straightforward. For instance:
fun(a0  a) = (a0  a) = (a0  Ta   ) = a0  Ta  since   = = a0   a 
by naturality of0= fun(a )  fun(a):A similar calculation shows that =e is a congruence.
The quotient of CT by =e has the same objects as CT (and therefore the same objects as C ),and the morphisms in the quotient category from A to B are the =e -equivalence classes ofmorphisms from A to B in CT . Let us write [a] for the equivalence class of a. Clearly, themap f 7! [alg(f )] is an isomorphism of hom-sets, showing that CT ==e is isomorphic to C .
The facts that fun  alg = IC and algfun =e ICT are elementary consequences of the de nitions.
We say that fun(a) is the extensional morphism computed by a. Since fun(algf ) = f , every
extensional morphism f is computed by some (not necessarily unique) intensional morphism.
These results show that every computational comonad can be used to produce an intensional
category that yields back the underlying extensional category when we take the extensional quotient. Next we show that fun and alg are natural transformations. Let Set be the category of sets
and functions.
13C (TA; B ) C (Tf; g-) C (TA0; B0)

C (TA; B) C (Tf; g-) C(TA0; B 0)
6

fun

fun
?

alg

?

C (A; B ) C (f; g)- C(A0; B 0)

6

alg

C(A; B ) C(f; g)- C (A0; B 0)

Figure 11: Naturality of fun and alg for a computational comonad: these diagrams commute, forall f : A0 !C A and g : B !C B 0.

De nition 4.3 The two-variable hom-functor C(T ( ); ) from Cop  C to Set takes a pair (A; B )of objects to C (TA; B ) and takes a pair of morphisms (f; g) with f : A0 !C A and g : B !C B 0 to
C (Tf; g) : C(TA; B ) ! C (TA0; B 0), where for all a : TA !C B,
C(Tf; g)(a) = g  a  Tf:
Similarly, the two-variable hom-functor C ( ; ) takes (A; B ) to C (A; B ) and (f; g ) to C (f; g ),where for all h : A !C B ,C(f; g)(h) = g  h  f:

Proposition 4.4 Let (T; ; ; ) be a computational comonad over a category C. Then fun and alg,as de ned in Proposition 4.2, are natural transformations:fun : C (T ( ); ) !: C ( ; )alg : C ( ; ) !: C (T ( ); ):That is, for all f : A0 !C A and g : B !C B 0 , the following identities hold:fun  C (Tf; g) = C (f; g)  fun
C (Tf; g)  alg = alg  C (f; g):Figure 11 expresses these properties in diagram form.

Proof: Straightforward, using naturality of and .
We now show that the three example comonads introduced earlier can be extended to become
examples of computational comonads.

144.2 Examples.

1. For the increasing paths comonad T1 , let D : D ! T1 D be de ned by D d = d! , for all d 2 D.
Clearly D is continuous, and is a natural transformation. Moreover, the computationalcomonad laws hold, since the lub of d! is d, and all pre xes of d! are equal to d! .
The functor fun maps each algorithm from Two  Two to Two into a function from Two  Two
to Two. In particular, fun(pb) = fun(lb) = fun(rb) = fun(db) = b. Similarly, fun(pbn ) = b for
all n  0, and fun(b ) = b. In fact, b = alg(b).
Figure 12 illustrates the result of taking the extensional quotient of Figure 6. Boxes enclose
equivalence classes of algorithms, arcs between boxes represent the quotient ordering, andwithin each box we retain the pointwise order to ease comparison with Figure 6. As expected,
the quotient gure is isomorphic to Figure 4 when we identify each equivalence class with thefunction computed.
2. For the strictly increasing paths comonad, we may again let D : D ! T2D be D d =d! . Again this is a continuous function, and is a natural transformation. Again thecomputational comonad laws hold. Figure 13 shows the quotient of Figure 8 by extensional
equivalence. Note that fun(d?) = fun(l?) = fun(r?) = fun(?) = ?.
Again the quotient diagram is isomorphic to Figure 4.
3. For the timed data comonad, we obtain a suitable by deciding what cost to associate witha degenerate computation. For each k 2 VNat we may take k d = hd; ki and obtain a naturaltransformation satisfying the requirements of a computational comonad. De ne funk to be
the functor whose action on algorithms is given by funk (a) = a  k , and let =e k be theequivalence relation induced by k . For example, we have, for each k  0:
funk (bn ) = b= ?

if k  n
if k > n:

Clearly, bn =e k bn+1 i k 6= n + 1.
Again the Kleisli category quotients onto the underlying category under the congruence induced by k . Figure 14 shows the quotient of Figure 9 under the equivalence induced by
n+1 .

5 Products and Exponentiation
5.1 Products

Now suppose that the underlying category C has products, and for each pair of objects A1 and A2
there is a distinguished product, which we denote A1  A2 , with i (i = 1; 2) being the projections.
It is easy to show that distinguished product objects in C are also product objects in CT , withprojections in CT given by:bi : A1  A2 !CT Ai
bi = Ai  T i
= i A1 A2 :Pairing of morphisms in CT is the pairing of morphisms in C , and the combination hT 1 ; T 2iplays a special r^ole in light of the following properties.
15

>

poll
@
@
@
@
@

pl
@
sl @@

@
@

db
lb

@
@

@
@

@

pr

sr
@
@

rb

pb

?

Figure 12: Quotient of Figure 6 by extensional equivalence.

16

>

poll
@
@
@
@
@

pl
@
sl @@

@
@

db
lb

@
@

@
@

@

pr

sr
@
@

rb

pb

d?
l?

@
@

@
@

r?

?

Figure 13: Quotient of Figure 8 by extensional equivalence.

17

>!
>
>n+1
poll!
poll
polln+1
@
@

l!
l

@
@
@
@

ln+1

r!
@

r
rn+1

@
@

@
@

b!
@
@

b

@

bn+1

>n
polln
ln

@
@

@
@

rn

bn

?

Figure 14: Quotient of Figure 9 by the equivalence induced by n+1 .
18

Proposition 5.1 If C has products then  : T (  ) !: T ( )  T ( ) de ned by:
A;B : T (A  B ) ! TA  TB
A;B = hT 1; T 2i

is a natural transformation such that, for all objects A and B ,(A  B )  A;B = AB
(A  B )  A;B = TA;TB  TA;B  AB
A;B  AB = A  B :Proof: Naturality of  follows from the universal property of products and the functoriality of T .
The remaining properties are easy consequences of naturality of ,  , and . Note the identity  T hf; gi = hTf; Tgi. In particular,   T = T 2 1; T 2 2 .

5.2 Exponentiation

Now suppose that the underlying category C is cartesian closed. That is, we assume that C has adistinguished terminal object and distinguished binary products, and that for every pair of objects
B and C there is a distinguished exponentiation object B ! C satisfying the usual requirements:
for all B and C there is a morphism appB;C : (B ! C )  B !C C such that, for all A and allmorphisms f : A  B !C C there is a unique morphism curry(f ) : A !C (B ! C ) such that
appB;C (curry(f )  idB ) = f .
Equivalently, a category is cartesian closed if it has nite products and there is a pair of natural
isomorphisms
curry : C (  B; C ) !: C ( ; B ! C )uncurry : C ( ; B ! C ) !: C (  B; C ):Here C (  B; C ) and C ( ; B ! C ) are contravariant hom-functors from C op to the category
Set , with the standard de nitions [1]. This is the same as requiring that curry(uncurry h) = h
and uncurry(curry g) = g , together with the following naturality conditions: for all f : A !C A0,
g : A0  B !C C , and h : A0 !C (B ! C),
curry(g  (f  id)) = (curry g)  f
uncurry (h)  (f  id) = uncurry(h  f ):It follows easily from these conditions that one can choose app = uncurry(id) as a suitableapplication morphism.
We want to give some general conditions under which analogous properties can be obtained for
the Kleisli category CT . Assuming that C is cartesian closed, the obvious candidate in CT for the
exponential object of B and C is TB ! C . Moreover, we know that there is a natural isomorphism
between CT (A; TB ! C ) and C (TA  TB; C ). Since CT (A  B; C ) is just C (T (A  B ); C ), it is clearthat we must make some assumptions about the relationship between T (A  B ) and TA  TB .
If T (A  B ) and TA  TB are naturally isomorphic it is easy to show that CT is cartesian closed
whenever C is. This is apparently a \Folk Theorem". The comonad T1 has this property, and we
gave in [4] a proof using this property that the Kleisli category of T1 is cartesian closed.
However, there are reasonable examples in which T does not preserve products, including T2
and T3 as described earlier. Instead, we will make a weaker assumption: that the comonad can beequipped with natural ways to move back and forth between T (A  B ) and TA  TB that interact
sensibly with the comonad operations ,  , and . This can be conveniently summarized by meansof two natural transformations split and merge satisfying certain combinational laws.
19

De nition 5.2 Let (T; ; ; ) be a computational comonad. A computational pairing is a pair ofnatural transformations
split : T (  ) !: T ( )  T ( )merge : T ( )  T ( ) !: T (  )such that, for all objects A and B , the following properties hold:(A  B )  splitA;B = AB
AB  mergeA;B = A  B
splitA;B  AB = A  B
mergeA;B ( A  B ) = AB(A  B )  split A;B = splitTA;TB T splitA;B AB
mergeTA;TB (A  B ) = T splitA;B AB  mergeA;B :Naturality of split and merge requires that for all f : A !C A0 and g : B !C B 0,
splitA ;B T (f  g) = (Tf  Tg)  splitA;B
mergeA ;B (Tf  Tg) = T (f  g )  mergeA;B :We summarize these properties in diagram form in Figure 15.
0

0

0

0



The properties listed above formalize the sense in which we require the splitting and merging
operations to interact sensibly with ,  , and . In particular, the following properties follow
immediately.

Corollary 5.3 Let (T; ; ; ) be a computational comonad and let split and merge form a computational pairing. Then for all A and B ,(A  B )  splitA;B  mergeA;B = (A  B )splitA;B  mergeA;B ( A  B ) = ( A  B )AB  mergeA;B  splitA;B = AB
mergeA;B  splitA;B  AB = AB :We have already seen that  = hT 1 ; T 2i quali es as a suitable split operation (Proposition 5.1). Despite this fact, split (and merge) are not generally uniquely determined by the computational pairing laws and we wish to permit the use of comonads with \non-standard" choicesof split. Moreover, naturality of split and merge does not by itself imply the computational pairinglaws.

5.3 Examples

1. Return again to the increasing path comonad T1. The natural transformation  = hT1 1 ; T1 2i
is given by: (u) = hn: 1 (un ); n: 2(un )i : This is actually an isomorphism, with inverse
given by merge(hs; ti) = n: hsn ; tn i : Intuitively, each of these two operations works \in parallel" on the two components.
Both  and merge are natural transformations, and they satisfy the computational pairinglaws, which state that: Merging and splitting commute with componentwise application of functions.
20g) T (A0  B0)
T (A  B) T (f  -g) TA0  TB 0
TA  TB T (f  -splitA ;B

splitA;B

0?

TA  TB Tf  Tg-

0mergeA ;B

mergeA;B?

0?

TA0  TB 0

T (A  B ) Tf  Tg-?

T (A0  B 0)
TA  TBTA  TB@@

mergeA;B0A B

A  B@@

mergeA;B

@
@

@
@
R
AB -@T (A  B) 
?

AB

?

AB - T (A  B )

AB



@
@

A  B

splitA;B



@

@
A B@

@

?

TA  TB

splitA;B@@@R ?

TA  TBTA  TBA  B-

mergeA;B

T 2A  T 2B
mergeTA;TB?

T (A  B)

AB - T 2(A  B) T splitA;B- T (TA ?TB )splitA;B

splitTA;TB?

TA  TBA  B-?

T 2A  T 2B

Figure 15: Properties of a computational pairing: these diagrams commute for all A, A0, B , B 0
and all f : A !C A0 , g : B !C B 0 .
21 Merging and splitting respect lubs of sequences.
 Merging and splitting respect pre xes.
 Merging two degenerate computations produces a degenerate computation, and splittinga degenerate computation produces a pair of degenerate computations.
2. There are other intuitively sensible ways to split and merge in the increasing paths comonad
T1. We can de ne a form of (left- rst) interleaving by:DE

lmerge(hs; ti) = n: sdn=2e; tbn=2c :For example, this gives:
lmerge(s0 s1 s!2 ; t0 t1 t!2 ) = hs0 ; t0 i hs1 ; t0 i hs1 ; t1 i hs2 ; t1 i hs2 ; t2 i! :To go with lmerge, we de ne a split that operates only on alternate steps of a computation:
split2 (u) = hn: 1(u2n ); n: 2 (u2n)i :We then obtain the identity split2  lmerge = id.
It is easy to verify that lmerge and split2 are natural transformations, and that the computational pairing properties hold, making use of the equalities bmin(i; 2j )=2c = min(bi=2c; j )and dmin(i; 2j )=2e = min(di=2e; j ).
There is clearly also a right- rst version of interleaving rmerge and this also interacts sensiblywith split2 as given above.
3. For the strictly increasing paths comonad, each of the split-merge combinations above adaptsin the obvious way, modi ed so as to ensure that the result of splitting a strictly increasing
sequence of pairs is a pair of strictly increasing sequences. Thus, for example,

(h?; ?i h>; ?i h>; >i! ) = h?>! ; ?>! imerge(?>! ; ?>! ) = h?; ?i h>; >i! :In fact T2(A  B ) and T2 A  T2B are not generally isomorphic, because a strictly increasing
sequence of pairs does not necessarily increase strictly in both components at each stage.
Nevertheless,  and merge are still natural transformations satisfying the requirements listed
above for a computational pairing, and we have the identity   merge = id.
The (appropriately adjusted) lmerge and split 2 operations also form a computational pairing,and split2  lmerge = id; similar properties hold for rmerge and split2.

5.4 Pairing, currying and uncurrying on algorithms

Using the split operation of a computational pairing provides a way to combine a pair of algorithms
into an algorithm on pairs. If split is taken to be  , this is the standard way to form the productof two morphisms in the Kleisli category. We can also use split to de ne intensional analogues tothe contravariant hom-functors C (  B; C ) and C ( ; B ! C ).
22

De nition 5.4 Let C be a category with nite products, let (T; ; ; ) be a computational comonad,
and let split be a natural transformation from T (  ) to T T . For f : A !CT A0 andg : B !CT B0 we de ne (f ^ g) : (A  A0 ) !CT (B  B 0 ) by f ^ g = (f  g)  split.
Proposition 5.5 Let C be a category with nite products, let (T; ; ; ) be a computational comonadand let split and merge form a computational pairing. Then there is a functor ^ from CT  CT
to CT that maps a pair of objects (A; B ) to A  B and maps a pair of morphisms (a; b) to(a ^ b) = (a  b)  split.
Proof: To show that ^ maps identity morphisms to identity morphisms:(idb A ^ idb B ) = (A  B )  split = AB = idb AB :To show that ^ preserves composition, let a : A !CT A0 , b : B !CT B 0, a0 : A0 !CT A00, andb0 : B 0 !CT B 00. Then:(a0 ^ b0)  (a ^ b) = ((a0  b0)  split)  ((a  b)  split)= (a0  b0 )  split T (a  b)  T split = (a0  b0 )  (Ta  Tb)  split T split = (a0  b0 )  (Ta  Tb)  (   )  split= ((a0  Ta   )  (b0  Tb  ))  split= ((a0  a)  (b0  b))  split= (a0  a) ^ (b0  b):
De nition 5.6 Let C be a cartesian closed category, let (T; ; ; ) be a computational comonad,

and let split and merge form a computational pairing. The contravariant functor CT ( ^ B; C ) from
CT op to Set is de ned as follows.

 On objects the functor maps A to CT (A  B; C ).
 On morphisms the functor maps f : A !CT A0 to the function g:g  (f ^ idb B ) from
CT (A0  B; C ) to CT (A  B; C ).
Similarly, the contravariant functor CT ( ; TB ! C ) from CT op to Set , is de ned by: On objects the functor maps A to CT (A; TB ! C ).
 On morphisms the functor maps f : A !CT A0 to the function h:h  f from CT (A0; TB ! C )to CT (A; TB ! C ).
Proposition 5.7 Let (T; ; ; ) be a computational comonad and let split and merge be a computational pairing. Given a : T (A  B ) !C C and b : TA !C (TB ! C ), de ned (a) : TA !C (TB ! C )d (b) : T (A  B ) !C C
curry
uncurryd (a) = curry(a  merge)d (b) = uncurry (b)  split :curry
uncurryThen:23

d and uncurryd are natural transformations: curry^ B; C ) !: CT ( ; TB ! C )d : CT ( curry: C ( d : CT ( ; TB ! C ) !
uncurry
T ^ B; C ):d (curryd (a)) =e a.
 For all a : A  B !CT C , uncurryd (curryd (alg f )) = alg f .
 For all f : A  B !C C , uncurry

Proof:^ idb B )) = (curryd amounts to the requirement that curryd (g  (f d g )  f , The naturality of curry
0
0
C
C
T
T
for all f : A ! A and g : A  B ! C . This follows from naturality of currying in C andthe properties of computational pairing:^ idb )) = curryd (g  (f d (g  T (f  )  T split  )curry
= curry(g  T (f  )  T split   merge)= curry(g  T (f  )  merge (  ))= curry(g  merge (Tf  T)  (   ))= curry(g  merge ((Tf   )  (T   )))= curry(g  merge ((Tf   )  id))= curry(g  merge)  (Tf   )d (g)  Tf  = curryd (g)  f:= curry^ idb ) = uncurryd we need uncurryd (h)  (f d (h  f ), for all Similarly, to show naturality of uncurry
0
0CCf : A ! T A and h : A ! T (TB ! C ). Again the proof is straightforward:^ idb ) = uncurry(h)  split T (f  )  T split d (h)  (f uncurry= uncurry(h)  (Tf  T)  split T split = uncurry(h)  (Tf  T)  (   )  split= uncurry(h)  ((Tf   )  (T   ))  split= uncurry(h)  ((Tf   )  id)  split= uncurry(h  Tf   )  split= uncurry(h  f )  splitd (h  f ):= uncurry Let a : A  B !CT C . Thend (curryd (a)) 
uncurry= uncurry(curry(a  merge))  split = (a  merge)  split = a  (merge  split  )= a ;d (curryd a) =e a.
showing that uncurry24 Let f : A  B !C C. Thend (curryd (alg f )) = uncurry(curry(alg(f )  merge))  split
uncurry= alg(f )  merge  split= f    merge  split
by Corollary 5.3= f 
= alg f:

We have shown that an intensional pairing produces a weak form of exponentiation structure:
we obtain notions of currying and uncurrying on algorithms that are natural transformations but
satisfy a weaker condition than isomorphism. We may rephrase these properties in terms of theexistence of a notion of \application" in the intensional category as follows.
Proposition 5.8 Let C be a cartesian closed category, (T; ; ; ) be a computational comonad andlet split and merge be a computational pairing. For all B and C there is an \application morphism"d B;C : [TB ! C ]  B !CT C
appsuch that, for all a : A  B !CT C^ idb B ) =e a:d (a) ad
ppB;C (curryb TB !C ) = uncurryd (idd (TB !C ): As a corollary of the naturality of
Proof: De ne ad
ppB;C = uncurryd (Proposition 5.7), we get:uncurryb )  (b 
^ idb )d (idadpp (b ^ idb ) = uncurrybd (id  b)= uncurryd (b):= uncurry^ idb ) = uncurryd (a) d (curryd (a)) =e a.
Thus, in particular, ad
pp (curryd (a) is not the unique morphism h such that ad
Note that although currypp (h ^ id) =e a, alld (h) =e a.
such morphisms satisfy the condition that uncurry
Thus, we have a weak form of cartesian closedness: instead of the usual diagram for exponentiation we replace = by =e and we relax the uniqueness condition. This is summarized in
Figure 16.
Next we consider what happens if we make further assumptions on the relationship between
split and merge.
Proposition 5.9 Let C be a cartesian closed category and (T; ; ; ) be a computational comonadwith a computational pairing split and merge.

d  curryd = id.
 If merge  split = id then uncurryd  uncurryd = id.
 If split  merge = id then curry

As a corollary we get the following version of the \Folk Theorem":
25

-C


a

AB
=e

^ idb
d (a) 
curry

ad
pp

?

(TB ! C )  B
Figure 16: When T has computational pairing this diagram in CT commutes up to extensional
equivalence, for all a : A  B !CT C .
Corollary 5.10 If C is cartesian closed and (T; ; ; ) is a computational comonad with a computational pairing such that merge  split = id and split  merge = id then the category CT is cartesianclosed.

Note the important fact that our de nitions are parameterized by the choice of split and merge.
d and uncurryd are determined uniquely. The Kleisli category itself
Once these are chosen, ad
pp, curry
is independent of split and merge; what happens, however, is that each choice of these two naturaltransformations induces a (weak form of) exponentiation structure on this category. The Kleisli
category may possess many di erent notions of merging and splitting, and therefore many di erent
ways to curry, uncurry and apply algorithms. This means that one may use the Kleisli category togive an interpretation to a functional programming language containing several syntactically andsemantically distinct forms of application. This would be desirable, for instance, if the language
included both a strict and a non-strict form of application.

5.5 Examples

1. The Kleisli category based on the increasing path comonad T1 is cartesian closed, with exponentiation structure built from the standard split-merge combination, which form an isomorphism.
Using the computational pairing lmerge and split2 , we obtain intensional forms of currying,d l , uncurryd l and ad
uncurrying, and application which we will call curry
ppl . This provides a
d l and uncurryd l are natural transformations, and for all
weak form of exponentiation: currya : A  B !CT1 C we get^ idb ) =e a:d l (a) adppl (curryd l (uncurryd l h) = h but uncurryd l (curryd l g) =e g: For
Since split2  lmerge = id, we have curry
example,d l (curryd l pb) = uncurryd l (curryd l lb) = pb;
uncurryd l (curryd l rb) is the least algorithm mapping the path h?; >ih?; >ih>; >i! to >.
and uncurryThis algorithm of course computes the function b.
Similar properties hold for the computation pairing rmerge and split2, with the derived operd r , uncurryd r and ad
ations curry
ppr .

26

2. The strictly increasing paths comonad T2, with computational pairing  and merge, again
d , uncurryd and adhas operations curry
pp that provide weak forms of exponentiation. As weremarked earlier,  and merge are not isomorphisms. Instead,   merge = id and for alld (uncurryd h) = hu 2 T2 (A  B ) the computation merge((u)) is pointwise above u. Hence, curryd (curryd g) =e g. As an example, we have:and uncurryd (curryd lb) = uncurryd (curryd rb) = uncurryd (curryd pb) = pb:
uncurry

The lmerge and split2 computational pairing also gives rise to a weak form of exponentiation,
as does the rmerge and split2 computational pairing.

6 Ordered categories
So far, although our principal examples were based on a cartesian closed category of domains, wehave not fully exploited the order structure. This permitted us to state and prove results that
hold in a more general category-theoretic setting. Next we suppose that the underlying category
is an ordered category: each hom-set is equipped with a complete partial order, and composition
is continuous. A functor T of ordered categories is required to respect the ordering, in that for
all f; g : A !C B if f  g then Tf  Tg. Moreover, T must also be continuous (in its action onmorphisms). All of our examples so far satisfy these conditions.
Suppose (T; ; ; ) is a computational comonad over an ordered category C . Then clearly CT
is again an ordered category. All of the results of the previous sections go through in the orderedsetting. In particular, the functors fun and alg introduced earlier respect the ordering; and theproof of Proposition 4.2 can be adapted to show that the extensional quotient of the ordering on
CT (A; B ) is just the order on C (A; B).
We can also obtain some slightly stronger results by taking advantage of the ordering. We omit
most of the proofs, which may be easily obtained from the results above, using monotonicity andcontinuity of composition.
Proposition 6.1 Let C be an ordered ccc and let (T; ; ; ) be a computational comonad over C

with a computational pairing.

d  uncurryd  id.
 If split  merge  id then curryd  uncurryd  id.
 If split  merge  id then curryd  curryd  id.
 If merge  split  id then uncurryd  curryd  id.
 If merge  split  id then uncurry

Next we introduce a simple generalization of the notion of cartesian closed ordered category,obtained by relaxing the requirement that currying and uncurrying form an isomorphism. Instead
we allow currying and uncurrying to form an adjunction in each homset, so that we have an example
of a local adjunction (see for example [9]) with additional properties. The relevance of \lax" notionsof adjunction such as these in computational settings (albeit with di erent motivations) has been
pointed out in di erent contexts by other authors, for instance in [14].

27De nition 6.2 An ordered category C is cartesian up-closed if and only if it has nite products andfor all pairs of objects B and C there is an object B ! C and a pair of lax natural transformations
curry, uncurry between C (  B; C ) and C ( ; B ! C ) satisfying:curry(uncurry h)  huncurry(curry g)  gcurry(g  (f  id))  curry(g)  f
uncurry (h)  (f  id)  uncurry(h  f ):Similarly, we say that C is cartesian down-closed i it has nite products and there is a pair oflax natural transformations curry, uncurry satisfying:curry(uncurry h)  huncurry(curry g)  gcurry(g  (f  id))  curry(g)  f
uncurry (h)  (f  id)  uncurry(h  f ):De nition 6.3 Let C be an ordered category with nite products.

 An up-exponential for objects B and C is an object B ! C of C together with a morphism
appB;C : (B ! C )  B !C C such that for every f : A  B !C C there is a least morphism
curry(f ) : A !C (B ! C ) such thatapp (curry(f )  id)  f:
 A down-exponential for objects B and C is an object B ! C of C together with a morphism
appB;C : (B ! C )  B !C C such that for every f : A  B !C C there is a greatest morphism
curry(f ) : A !C (B ! C ) such thatapp (curry(f )  id)  f:
The following result may be shown by adapting the usual proof that the two alternative de nitions of cartesian closed categories are equivalent.
Proposition 6.4 An ordered category C is cartesian up-closed i it has nite products and upexponentials.
An ordered category is cartesian down-closed i it has nite products and down-exponentials.
Note that if the same object B ! C and morphism appB;C quali es simultaneously as an
up- and a down-exponential then it forms the usual notion of exponentiation and the category iscartesian closed in the usual sense.
Proposition 6.5 Let C be a cartesian up-closed category, let (T; ; ; ) be a computational comonad,
and let split and merge be a computational pairing such thatsplit  merge  id
merge  split  id(  )  split  split T split 
merge (   )  T split   merge :Then CT is cartesian up-closed.
28

Proof:

 Let a : A  B !CT C and b : A !CT (TB ! C). Then:d (curryd a) = uncurry (curry(a  merge))  split  a  merge  split  auncurryd (uncurryd b) = curry(uncurry(b)  split  merge)  curry(uncurry b)  b:
curry
d is a lax natural transformation, let f : A !CT A0 and g : A0  B !CT C .
 To show that curryThen:^ idb )) = curryd (g  (f d (g  T (f  )  T split  )curry
= curry(g  T (f  )  T split   merge)
 curry(g  T (f  )  merge (  ))= curry(g  merge (Tf  T)  (   ))= curry(g  merge ((Tf   )  (T   )))= curry(g  merge ((Tf   )  id)) curry(g  merge)  (Tf  )
d (g)  Tf  = curryd (g)  f:= curryd is a lax natural transformation, suppose that f : A !CT A0 and To show that uncurry0C
h : A ! T (TB ! C ). Then

^ idb ) = uncurry(h)  split T (f  )  T split d (h)  (f uncurry uncurry(h)  (Tf  T)  split T split = uncurry(h)  (Tf  T)  (   )  split= uncurry(h)  ((Tf   )  (T   ))  split= uncurry(h)  ((Tf   )  id)  split
 uncurry(h  Tf  )  split= uncurry(h  f )  splitd (h  f ):= uncurry
A similar result holds for a cartesian down-closed category with a computational pairing satisfying
reversed inequalities.

7 Examples
We now return to the third comonad introduced earlier, after which we will introduce brie y somerelated of notions of computation on di erent categories of domains and functions.

7.1 Timed data

In the timed data comonad T3 , the standard split operation is:
split hha; bi ; ni = hha; ni ; hb; nii :29Given our interpretation of hd; ni as a computation yielding d at cost n, an obvious choice fora merge operation is:merge(ha; mi ; hb;ni) = hha; bi ; max(m; n)i :Both of these operations are natural transformations, and we obtain the following properties:
split  merge v id
merge  split = id(  )  split = split T3 split 
merge (   ) w T3 split   merge :The underlying category is cartesian closed, hence also cartesian up-closed. It follows from
Proposition 6.5 that the Kleisli category of T3 is cartesian up-closed.

7.2 Strict algorithms

The category of domains and strict continuous functions is not cartesian closed, although thecategory does have products. For each pair of domains D and D0, the set of strict continuousfunctions D !s D0 , ordered pointwise, is again a domain. The usual uncurrying operation on
functions preserves strictness, but the usual currying does not. Instead, we may de ne a variant
form of currying by:currys : (A  B !s C ) ! (A !s (B !s C ))currys (f ) = x:y:(x = ? _ y = ? ! ?; f (x; y )):When f is strict, currys (f ) is the best strict function approximating curry(f ) pointwise. For
instance, let lor, ror and sor be the left-strict, right-strict, and doubly-strict or-functions. Then
uncurry(currys lor) = uncurry(currys ror) = uncurry (currys sor) = sor :It is easy to check that currys is a natural transformation (and so is uncurry).
The following relationships hold, for all f : A  B !s C and all g : A !s (B !s C ):currys (uncurry g) = g
uncurry (currys f ) v f:
Hence, the category of domains and strict continuous functions is cartesian down-closed.
Let T1D be the set of increasing paths over D (not just the strict continuous maps from VNat
to D), ordered pointwise. The maps ,  and are all strict, as are all of the split and merge
operations above. We may therefore use the Kleisli construction to build a model of strict parallel
algorithms. To illustrate this model, note that all of the algorithms of Figure 6 also belong in thiscategory, with the exception of >, which is non-strict.
Since the underlying category is cartesian down-closed, each of the computational pairings
discussed earlier for T1 gives rise to a down-exponentiation structure, so that the category of
domains and strict algorithms is again cartesian down-closed.
We may also adapt the T2 and T3 comonads to this category.

30

7.3 Computation on e ectively given domains

The category of e ectively given domains and computable functions is cartesian closed. A domain ise ectively given i its nite elements are recursively enumerable (hence, countable), it is decidable
whether two nite elements are consistent, and (an index for) the lub of two consistent niteelements is decidable (as a function of their indices). An element of D is computable i the set of(indices of) its nite approximations is recursively enumerable.
The functor T1 can be adapted to this category, by de ning T1 D for an e ectively given domain
D to be the computable increasing paths over D (equivalently, the computable continuous functions
from VNat to D, ordered pointwise). All of the auxiliary operations (,  , , and so on) are computable. Hence we obtain a category of e ectively given domains and computable algorithms, andthis category quotients onto the underlying category of e ectively given domains and computablefunctions. This algorithms category is again cartesian closed.
The functor T3 maps e ectively given domains to e ectively given domains, and again theauxiliary operations are computable. We therefore obtain a category of e ectively given domains
and T3 -algorithms that quotients onto the underlying category and is cartesian up-closed.
The functor T2 preserves algebraicity but not ! -algebraicity, since T2 D may have uncountably
many nite elements. The T2 comonad therefore does not adapt to the category of e ectively given
domains and computable functions.

7.4 Computation on pre-domains

We use the term pre-domain for a \bottomless" domain: a directed-complete, bounded complete,
algebraic partial order with no requirement that there be a least element. The category of predomains and continuous functions is cartesian closed.
Let T4 D be the set of non-empty nite or in nite increasing sequences over D, ordered by
the pre x ordering. Clearly this forms a pre-domain, and the nite elements are just the nitesequences. T4D is generally a pre-domain rather than a domain, even if D has a least element,
because the pre x ordering does not relate sequences with di erent rst elements. We make T intoa functor by specifying that (as usual) T4f applies f componentwise.
Again we let  be the lub operation and let t be the sequence of (non-empty) pre xes of t.
Then (T4; ;  ) forms a comonad.
We may regard a computation of length 1 as degenerate, and this corresponds to de ning thefunction from D to T4D by d = hdi. Although this function is not continuous, so that
we cannot claim that T4 is a computational comonad, we still obtain a congruence relation on
algorithms by de ninga =e a0 () 8d 2 D:ahdi = a0 hdi:
Note that for all f; g : A ! B we have(f  ) =e (g  ) ) f = g:
It is then easy to modify the proof of Proposition 4.2 to show that the Kleisli category of thiscomonad quotients onto the underlying category under =e .
We may de ne splitting and merging operations as follows. The standard way to split is:
split(hx0; y0 i . . . hxk ; yk i) = hx0 . . . xk ; y0 . . . yk i
1
1
split(hxn ; yn i1
n=0 ) = hhxn in=0 ; hyn in=0 i :31Let merge be the least continuous function satisfying:merge(x0 . . . xk ; y0 . . . ym ) = hx0 ; y0 i . . . hxn ; yn i(n = min(m; k))merge(x0 . . . xk ; hyi i1
)
=
h
x
;
y
i
.
.
.
h
x
;
y
i
0 0
k k
i=0
merge(hxi i1
;
y
.
.
.
y
)
=
h
x
;
y
i
.
.
.
h
x
0
m
0
0
m ; ym ii=01 ) = hx ; y i1 :merge(hxn i1;hyin n n=0n=0 n n=0
Clearly, merge  split = id and split  merge v id. These two operations are obviously naturaland satisfy the computational pairing properties, except that   merge v   . The Kleisli category
is cartesian down-closed.

8 Conclusions
We have described a category-theoretic approach to intensional semantics, based on the idea thata notion of computation or intensional behavior may be modelled by means of a computationalcomonad, and that the Kleisli category thus obtained can be viewed as an intensional model. The
morphisms in this category map computations to values, and from such a morphism one may
recover a map from values to values. One may de ne an equivalence relation that identi es allalgorithms that compute the same function, and this equivalence relation can be used to collapse
the Kleisli category onto the underlying category.
We have identi ed a set of conditions under which the Kleisli category possesses exponentiations
or weaker types of exponentiation, based on the existence of natural ways to pair computations.
We described a series of examples to illustrate the applicability of our de nitions and results. In
doing so, we have placed our recent work [4] in a wider context.
Our work arose out of an attempt, begun in [3], to generalize an earlier intensional model ofBerry and Curien [6]. They de ned a category of deterministic concrete data structures and sequential algorithms, showed that this category is cartesian closed, and that it collapses onto thecategory of deterministic concrete data structures and sequential functions under an obvious notionof extensional equivalence. The sequential functions category is not cartesian closed, and their construction of sequential algorithms was not based on a comonad. The operational semantics implicitin their work was again coroutine-like and lazy, but with the restriction that computation should
proceed sequentially, with at most one argument being evaluated at a time. In our generalizationof their model we relax the sequentiality restriction so as to permit parallel computation.
The query model of parallel algorithms between deterministic concrete data structures, describedin [3], contains algorithms for non-sequential functions such as parallel-or. However, the model'sconstruction was rather complex and we were unable to formulate a suitable notion of composition
for algorithms. Instead, in [4] we presented a much more streamlined form of algorithm between
Scott domains and for the rst time we cast our construction in terms of a comonad. Of thecomonads introduced in this paper, T1 corresponds to the comonad used in [4]; T2 is closer in spirit
to the query model of [3], but we are able here to go considerably further.
Moggi has developed an abstract view of programming languages in which a notion of computation is modelled as a monad [12, 13]. Examples of notions of computation as monads include: computation with side-e ects, computation with exceptions, partial computations, andnon-deterministic computations. In this view, the meaning of a program is taken as a function
from values to computations, and an intuitive operational semantics is that a program from A to
B takes an input of type A and returns an output computation. This point of view is consistent
with an input-driven lazy operational semantics. In contrast, our \opposite" point of view based32

on comonads (which are, after all, monads on the opposite category) is consistent with a demanddriven lazy operational semantics. Moggi states in [12] that his view of programs corresponds tocall-by-value parameter passing, and he says that there is an alternative view of \programs asfunctions from computations to computations" corresponding to call-by-name. Our work showsthat there is also a third alternative: programs as functions from computations to values. Common
to these approaches is the realization that values should be distinguished from computations (andthe use of an endofunctor T ). Apart from that, the motivations and the operational intuitions
behind the monad approach and the comonad approach are di erent, and we feel that the two
approaches should be regarded as orthogonal or complementary. The extra structure and algebraiclaws embodied in a monad seem appropriate in Moggi's context. Equally, the extra structure andalgebraic laws embodied in a comonad seem appropriate in our context. We plan to explore to what
extent (and to what e ect) the two approaches can be combined. For instance, given a comonad T
and a monad P over the same category C one might obtain (assuming that T and P satisfy certain
properties) a category of (T; P )-algorithms, in which a morphism from A to B is a morphism in Cfrom TA to P B .
We plan to investigate notions of computation in further domain-theoretic settings. We are
already working on categories of algorithms on (generalized) concrete data structures [5]. It would
be interesting to see if the Berry-Curien sequential algorithms category could be embedded in the
Kleisli category of a suitable comonad over a sequential functions category. We intend to investigate
notions of computation on the category of dI-domains and stable functions [2], and on the categoryof qualitative domains and linear functions [7].

Acknowledgements

The diagrams in this paper were drawn using macros designed by John Reynolds.

33

References[1] M. Barr and C. Wells. Category Theory for Computing Science. Prentice-Hall International,
1990.
[2] G. Berry. Stable models of typed -calculi. In Proc. 5th Coll. on Automata, Languages andProgramming, number 62 in Lecture Notes in Computer Science, pages 72{89. Springer-Verlag,
July 1978.
[3] S. Brookes and S. Geva. Towards a theory of parallel algorithms on concrete data structures.
In Semantics for Concurrency, Leicester 1990, pages 116{136. Springer Verlag, 1990.
[4] S. Brookes and S. Geva. A cartesian closed category of parallel algorithms between Scottdomains. Technical Report CMU-CS-91-159, Carnegie Mellon University, School of Computer
Science, 1991. Submitted for publication.
[5] S. Brookes and S. Geva. Continuous functions and parallel algorithms on concrete data structures. Technical Report CMU-CS-91-160, Carnegie Mellon University, School of Computer
Science, 1991. To appear in the Proceedings of MFPS'91.
[6] P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming.
Research Notes in Theoretical Computer Science. Pitman, 1986.
[7] J.-Y. Girard. Proofs and Types. Cambridge University Press, 1989.
[8] C. Gunter and D. Scott. Semantic domains. In Handbook of Theoretical Computer Science,
Volume B: Formal Models and Semantics. MIT Press/Elsevier, 1990.
[9] C. B. Jay. Local adjunctions. Journal of Pure and Applied Logic, 53:227{238, 1988.
[10] G. Kahn and D. B. MacQueen. Coroutines and networks of parallel processes. In Information
Processing 1977, pages 993{998. North Holland, 1977.
[11] S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.
[12] E. Moggi. Computational lambda-calculus and monads. In Fourth Annual Symposium on
Logic in Computer Science. IEEE Computer Society Press, June 1989.
[13] E. Moggi. Notions of computation and monads. Information and Computation, 1991.
[14] R. A. G. Seely. Modeling computations: A 2-categorical framework. In Symposium on Logicin Computer Science. IEEE Computer Society Press, June 1987.

34