Coalgebraic Components
in a Many-Sorted Microcosm
Ichiro Hasuo1,4 , Chris Heunen2 , Bart Jacobs2 , and Ana Sokolova3
1

RIMS, Kyoto University, Japan
Radboud University Nijmegen, the Netherlands
3
University of Salzburg, Austria
4
PRESTO Research Promotion Program, Japan Science and Technology Agency
2

Abstract. The microcosm principle, advocated by Baez and Dolan andformalized for Lawvere theories lately by three of the authors, has been
applied to coalgebras in order to describe compositional behavior systematically. Here we further illustrate the usefulness of the approach byextending it to a many-sorted setting. Then we can show that the coalgebraic component calculi of Barbosa are examples, with compositionalityof behavior following from microcosm structure. The algebraic structure on these coalgebraic components corresponds to variants of Hughes’
notion of arrow, introduced to organize computations in functional programming.

1

Introduction

Arguably the most effective countermeasure against today’s growing complexityof computer systems is modularity: one should be able to derive the behavior of
the total system from that of its constituent parts. Parts that were developed andtested in isolation can then safely be composed into bigger systems. Likewise,
one would like to be able to prove statements about the compound system basedon proofs of substatements about the parts. Therefore, the theoretical models
should at the very least be such that their behavior is compositional.
This is easier said than done, especially in the presence of concurrency, thatis, when systems can be composed in parallel as well as in sequence. The microcosm principle [1, 12] brings some order to the situation. Roughly speaking,compositionality means that the behavior of a compound system is the composition of the components’ behaviors. The microcosm principle then observes
that the very definition of composition of behaviors depends on composition ofsystems, providing an intrinsic link between the two.
The present article gives a rigorous analysis of compositionality of components as sketched above. Considering models as coalgebras, we study Barbosa’s
calculi of components [2, 3] as coalgebras with specified input and output interfaces. Explicitly, a component is a coalgebra for the endofunctor
FI,J = (T (J × ))I : Set → Set,

(1)

2

where I is the set of possible input, and J that of output. The computational
effect of the component is modeled by a monad T , as is customary in functional programming [25]. The monad T can capture features such as finite nondeterminism (T = Pω ), possible non-termination or exceptions (T = 1 + ),probabilistic computation (T = D), global states (T = (S × )S ), or combinations of these.
To accommodate component calculi, the surrounding microcosm needs tobe many-sorted. After all, composing components sequentially requires that theoutput of the first and the input of the second match up. This is elaborated on
more precisely in §2. The contribution of the present article is twofold:– a rigorous development of a many-sorted microcosm principle, in §4;– an application of the many-sorted microcosm framework to component calculi, in §5.
It turns out that components as FI,J -coalgebras carry algebraic structurethat is a variant of Hughes’ notion of arrow [14, 19].5 Arrows, generalizing monads, have been used to model structured computations in semantics of functional
programming. In §5 we give a rigorous proof that components indeed carry sucharrow-like structure; however the calculation is overwhelming as it is. We shall
exploit the fact that a Kleisli category Kℓ(T ), where the calculation takes place,also carries the same arrow-like structure. This allows us to use the axiomatization of the (shared) structure as an “internal language.”2

Leading example: sequential composition

We shall exhibit, using the following example, the kind of phenomena in component calculi that we are interested in.
For simplicity let us assume that we have no effect in components (i.e. T =Id, FI,J = (J × )I ). Coalgebras for this functor are called Mealy machines, seee.g. [7]. A prominent operation in component calculi is sequential composition,or pipeline. It attaches two components with matching I/O interfaces, one after
another:

 >>>
I,J,K
I
J
I
J
K
, J dK
7−→
(2)
c
c d

Let X and Y be the state spaces of the components c and d, respectively. The
resulting component c >>>I,J,K d has the state space X × Y ;6 first c produces
output j ∈ J that is fed into the input port of d. More precisely, we can define
the coalgebra c >>>I,J,K d to be the adjoint transpose of the following function.
ĉ×d

X×ev

I × X × Y −→ J × X × (K × Y )J −→J K × X × Y(3)Here ĉ : I × X → J × X is the adjoint transpose of the coalgebra c, andevJ : J × (K × Y )J → K × Y is the obvious evaluation function.
5

Throughout the paper the word “arrow” always refers to Hughes’ notion. An “arrow”
in a category (as opposed to an object) will be always called a morphism.
6
We will use the infix notation for the operation >>>. The symbol >>> is taken fromthat for (Hughes’) arrows, whose relevance is explained in §5.

3

An important ingredient in the theory of coalgebra is F X
FZ“behavior-by-coinduction” [18]: when a state-based system is c=
final ∼
viewed as an F -coalgebra, then a final F -coalgebra (which very X beh(c) Z
often exists) consists of all the “behaviors” of systems of type
F . Moreover, the morphism induced by finality is the “behavior map”: it carries
a state of a system to its behavior. This view is also valid in the current example.
A final FI,J -coalgebra—where FI,J = (J × )I —is carried by the set ofstream functions I ω → J ω which are causal, meaning that the n-th letter of theoutput stream only depends on the first n letters of the input.7 It conforms to ourintuition: the “behavior” of such a component is what we see as an output stream
when we feed it with an input stream. Let us denote the final FI,J -coalgebra by∼=

ζI,J : ZI,J −→ FI,J (ZI,J ) ,that is, ZI,J = {t : I ω → J ω | t is causal} .

The structure map ζI,J is described in detail in [29].
Then there naturally arises a “sequential composition” operation that is different from (2): it acts on behaviors of components, simply composing two behaviors of matching types.
>>>I,J,K :

×
ZJ,K

ω t
I → J , J → Kω
ZI,J
ω s

−→
7−→

ω

ZI,K
t
I → J ω → Kω
ω s

(4)

The following observation—regarding the two operations (2) and (4)—is crucial for our behavioral view on component calculi. The “inner” operation (4),although it naturally arises by looking at stream functions, is in fact inducedby the “outer” operation (2). Specifically, it arises as the behavior map for the(outer) composition ζI,J >>>I,J,K ζJ,K of two final coalgebras.
FI,K (ZI,K )FI,K (ZI,J × ZJ,K )ζI,J >>> ζJ,K
final ζI,K
ZI,J × ZJ,K
ZI,K>>>I,J,K

0
i.e.

I

B ζI,J
B
J
B@ ζJ,KK

1

1
0
C >>>I,J,K
I
C
C 99K @ ζI,K A
A
K

(5)

Note here that, due to our definition (3), the coalgebra ζI,J >>>I,J,K ζJ,K has astate space ZI,J × ZJ,K .
As to the two operations (2) and(4), we can ask a further question:
are they compatible, in the sense thatthe the diagram on the right commute? One can think of this compatibility property as mathematical formulation of compositionality, a fundamental property in the theory of processes/components. The characterization of the inner operation by finality (5) isremarkably useful here; finality immediately yields a positive answer.
7

This is how they are formalized in [29]. Equivalent formulations are: as string functions I ∗ → J ∗ that are length-preserving and prefix-closed [26]; and as functions
I + → J where I + is the set of strings of length ≥ 1.

4

In fact, the microcosm principle is the mathematical structure that has been
behind the story. It refers to the phenomenon that the same algebraic structure
is carried by a category C and by an object X ∈ C, a prototypical example
being “a monoid object in a monoidal category” (see e.g. [24, §VII.3]). In [12] we
presented another example eminent in the process theory: parallel compositionof two coalgebras for the same signature functor, as well as parallel compositionof their behaviors. Our story so far is yet another example taken from component
calculi, with its new feature being that the algebraic structure is many-sorted.

3

FP-theory

3.1

Presenting algebraic structure as a category

Algebraic structure in this paper refers to the one in universal algebra (seee.g. [10]). We need it to be many-sorted in modeling component calculi. Algebraic structure consists of– a set S of sorts;– a set Σ of operations. Each operation σ ∈ Σ is equipped with its in-arity
inar(σ) given by a finite sequence of sorts denoted by S1 × · · · × Sm , and its
out-arity outar(σ) that is some sort S ∈ S;
– and a set E of equations.
A straightforward presentation of such is as a tuple (S, Σ, E) which is called an
algebraic specification (see e.g. [17]).
In this paper we prefer different, categorical presentation of algebraic structure. The idea is that algebraic structure can be presented by a category L with:– all the finite sequences of sorts S1 × · · · × Sm as its objects;σ– operations σ ∈ Σ as morphisms inar(σ) → outar(σ). Additionally, projections(such as π1 : S1 × S2 → S1 ) and diagonals (such as hid, idi : S → S × S)
are morphisms. So are (formal) products of two morphisms, equipping thecategory L with finite products. Besides we can compose morphisms in the
category L; that makes the morphisms in L precisely the terms composedusing the operations in Σ;– an equation as a commutative diagram. For example, when S is a singleton
and we have a binary operation m, its associativity

x, y, z ⊢ m(x, m(y, z)) = m(m(x, y), z)

amounts to

3

m×id

2
m

id×m

2

m

. (6)

1

See [17, §3.3] for the precise correspondence between an algebraic specification(S, Σ, E) and a category L. The correspondence is not bijective; to be precisesuch a category L represents the clone of an algebraic specification (see e.g. [10]).
Sketched in the above is the construction in one way, from (S, Σ, E) to L.

5

In a one-sorted setting—where arities (objects of L) are identified with natural numbers by taking their length—such a category L is called a Lawvere
theory (see e.g. [12, 15, 22]). In a many-sorted setting, such a category L—say a“many-sorted Lawvere theory”—is usually called a finite-product theory, or an
FP-theory, see e.g. [4, 5].
Definition 3.1 (FP-theory) An FP-theory is a category with finite products.
The idea of such categorical presentation of algebraic structure originatedin [22]. Significant about the approach is that one has a model as a functor.
Definition 3.2 (Set-theoretic model) Let L be an FP-theory. A (set-theoretic)model of L is a finite-product-preserving (FP-preserving) functor X : L → Set
into the category Set of sets and functions.
Later in Def. 4.1 we introduce the notion of category with L-structure—this is
the kind of models of our interest—based on this standard definition.
m
To illustrate Def. 3.2 in a one-sorted setting, think about an operation 2 → 1
which satisfies associativity (6). Let the image X(1) of 1 ∈ L be simply denoted
by X; then 2 = 1 × 1 ∈ L must be mapped to the set X 2 by FP-preservation.
By functoriality the morphism m is mapped to a morphism X(m) : X 2 → X
in Set, which we denote by JmKX . This yields a binary operation on the set X.
Moreover, the associativity diagram (6) in L is carried to a commutative diagramin Set; this expresses associativity of the interpretation JmKX .
When L arises from a many-sorted algebraic specification, it is not a single
set X that carries L-structure; we have a family of sets {X(S)}S∈S —one foreach sort S—as a carrier. By FP-preservation this extends to interpretation of
products of sorts: X(S1 × · · · × Sm ) ∼= X(S1 ) × · · · × X(Sm ).8 In this way anoperation is interpreted with its desired domain and codomain.
3.2

The FP-theory PLTh

We now present a specific FP-theory which will be our working example. We
list its sorts, operations and equations; these altogether induce an FP-theory in
the way that we sketched above. We denote the resulting FP-theory by PLTh.
Later in §5 we will see that this FP-theory represents Hughes’ notion of arrow,without its first operation. One can think of PLTh as a basic component calculus
modeling pipelines (PL for “pipeline”).
Assumption 3.3 Throughout the rest of the paper we fix a base category B to
be a Cartesian subcategory (i.e. closed under finite products) of Set. Its objects
8

To be precise, one should see the right-hand side as denoting a specific choice of a
product, say (· · · (XS1 × XS2 ) × · · · ) × XSm . Because Cartesian products in Set are
not strictly associative, one cannot force a functor X to be strictly FP-preserving.
This is why the displayed equation holds only up-to isomorphism.

6

I ∈ B are sets that can play a role of an interface. Its morphisms f : I → J—these are set-theoretic functions—represent “stateless” computations from I to
J that can be realized by components with a single state.
The FP-theory PLTh is generated by:– the sorts S = {(I, J) | I, J ∈ B}. Hence an object of PLTh can be written
as a formal product (I1 , J1 ) × · · · × (Im , Jm ). We denote the nullary product(i.e. the terminal object) by 1 ∈ PLTh;– the operations:>>>I,J,K : (I, J) × (J, K) −→ (I, K)
arr f : 1 −→ (I, J)

sequential composition
pure function

for each object I, J, K ∈ B and each morphism f : I → J in B. Sequential
composition is graphically understood as in (2). The component arr f , intuitively, has a singleton as its state space and realizes “stateless” processingIof data stream
arr f– the equations:• associativity:J;a : (I, J), b : (J, K), c : (K, L) ⊢ a >>> (b >>> c) = (a >>> b) >>> c(>>>-Assoc)
for each I, J, K, L ∈ B, omitting the obvious subscripts for >>>, i.e.
>>>I,J,K × (K, L)(I, J) × (J, K) × (K, L)(I, K) × (K, L)>>>I,K,L(I, J) × >>>J,K,L(I, J) × (J, L)(I, L)>>>I,J,L• preservation of composition: for each composable pair of morphisms f :I → J and g : J → K in B,∅ ⊢ arr (g ◦ f ) = arr f >>> arr g(arr-Func1)

where ∅ denotes the empty context. That is as a diagram,1

arr f × arr g(I, J) × (J, K)>>>I,J,K
arr (g ◦ f )(I, K)• preservation of identities: for each I, J ∈ B,
a : (I, J) ⊢ arr idI >>>I,I,J a = a = a >>>I,J,J arr idJ .

(arr-Func2)

For this FP-theory, the model of our interest is not a family of sets with thisstructure, but a family of categories, namely the category Coalg(FI,J ) for eachsort (I, J). Formalization of such an outer model carried by categories, together
with that of an inner model carried by final coalgebras, is the main topic of thenext section.

7

4

Microcosm model of an FP-theory

In this section we present our formalization of microcosm models for an FPtheory L. It is about nested models of L: the outer one (L-category) being afamily {C(S)}S∈S of categories; the inner one (L-object) being a family {XS ∈C(S)}S∈S of objects. Its relevance has been mentioned in §2; we shall use ourformalization to prove a general result (Thm. 4.7) that ensures compositionality.
In fact the formalization we present is essentially the one in our previous
work [12]. Due to the space limit we cannot afford sufficient illustration of ourseemingly complicated 2-categorical arguments. The reader is strongly suggested
to have [12, §3] as her companion; the thesis [11, Chap. 5] of one of the authors
has a more detailed account. What is new here, compared to [12], is the following.
– The algebraic structure of our interest is now many-sorted, generalizing Lfrom a Lawvere theory to an FP-theory.
– Now we can accommodate categories with “pseudo” algebraic structure in
our framework, such as monoidal categories as opposed to strict monoidal
categories. We cannot avoid this issue in the current paper, where we deal
with concrete models that satisfy equations only up-to isomorphisms.
4.1

Outer model: L-category

Take the functor FI,J = (T (J × ))I , for which coalgebras are components(see §1). We would like that the categories {Coalg(FI,J )}I,J∈B model PLTh,the algebraic structure for pipelines in §3.2. That is, we need functors
J>>>I,J,K K : Coalg(FI,J ) × Coalg(FJ,K ) → Coalg(FI,K ) for each I, J, K ∈ B,
Jarr f K: 1 → Coalg(FI,J )for each morphism f : I → J in B,
where 1 is a (chosen) terminal category, satisfying the three classes of equationsof PLTh in §3.2. One gets pretty close to the desired definition of “category
with L-structure” by replacing “sets” by “categories” in Def. 3.2. That is, by
having CAT—the 2-category of locally small categories, functors and naturaltransformations—in place of Set. In fact we did so in [12].
However here arises the problem of the right notion of “equality,” as it always
does when one moves up from n-categories to (n + 1)-categories. In a set theright notion of “equality” is the identity between elements; this is why a monoid
satisfies associativity up-to identity. In a category it is weakened into (coherent)
isomorphisms between objects;9 hence in a monoidal category multiplication isassociative only up-to isomorphism. The definition of L-categories must suitably
address this issue. Specifically, an equation—a commutative diagram in L—must
now be carried to a diagram which is “commutative up-to isomorphism,” i.e. a
9Equivalence of 0-cells is the right “equality” in a 2-category; biequivalence (seee.g. [27]) is the one in a 3-category; and so on.

8

3

id×m

2

=

m×id

2

m

m

1

in Set X 3

Jid×mKX

Jm×idKX

=

in L

X2

JmKX

X2
JmKX

X

x1 · (x2 · x3 ) = (x1 · x2 ) · x3

in CAT C3

Jid×mKC

Jm×idKC⇐=

diagram filled in with an iso-2-cell. Using the (one-sorted) example (6):

C2

∼
=

JmKC

C2
JmKC

C

∼

=
X1 ⊗ (X2 ⊗ X3 ) →(X1 ⊗ X2 ) ⊗ X3

We have worked on the clue obtained in [12, §3.3] and [11, §5.3.3]10 and cometo the following definition. In short, we get equations satisfied up-to isomorphism,by weakening a functor into a pseudo functor ; the latter preserves identities
and composition only up-to coherent isomorphisms (see e.g. [8]). The delicate
question here is what it means for a pseudo functor to be FP-preserving. The
conditions below are chosen so that Prop. 4.2 holds (see also Rem. 4.3 later).
Definition 4.1 (L-category) An L-category is a pseudo functor C : L →CAT that is FP-preserving in the following sense:11
1. the canonical map hCπ1 , Cπ2 i : C(A1 × A2 ) → C(A1 ) × C(A2 ) is an isomorphism for each A1 , A2 ∈ L;
2. the canonical map C(1) → 1 is an isomorphism;
3. it preserves identities up-to identity: C(id) = id;
4. it preserves pre- and post-composition of identities up-to identity: C(id ◦a) = C(a) = C(a ◦ id);
5. it preserves composition of the form πi ◦ a up-to identity: C(πi ◦ a) =C(πi ) ◦ C(a). Here πi : A1 × A2 → Ai is a projection.
We shall often denote C’s action C(a) on a morphism a by JaKC .
One consequence from the definition is that C also preserves composition of theform δ ◦ a, where δ : A → A × A is a diagonal. It is illustrated in [11, 12] how
pseudo functoriality induces isomorphisms up-to which equations are satisfied.
The definition is justified by the following fact. Its proof, as well as its generalization to other algebraic structure, is postponed to another venue.
Proposition 4.2 Let us denote the Lawvere theory for monoids by MonTh.
The 2-category MonCAT of monoidal categories, strong monoidal functors andmonoidal transformations is equivalent to the 2-category of MonTh-categories
with suitable 1- and 2-cells.
⊓⊔
In Def. 4.1 one can replace CAT by any 2-category with finite 2-products andobtain a more general notion of pseudo L-model. Such generality is not neededin this paper.
10Later we came to know that the idea is folklore at least for “monoidal” theories. It
is mentioned in [13] as Segalic presentation of monoidal categories.
11
To be precise, each of the conditions 3–5 means that the corresponding mediating
isomorphism (as part of the definition of a pseudo functor) is actually the identity.

9

Remark 4.3 A standard way to avoid the complication with pseudo algebraic
structure is by a coherence result [20, 24]. For example: every monoidal category
is equivalent to a strict one. This, however, only gives us a biequivalence (seee.g. [27]) between MonCAT and the 2-category of strict monoidal categories.
Although one readily sees that the latter is equivalent to the 2-category of strict
MonTh-categories, the two correspondence results combined only yield biequivalence. In contrast, Prop. 4.2 realizes equivalence between MonCAT and the2-category of MonTh-categories, by fine-tuning the latter notion.
Remark 4.4 In [21] a different approach for modeling pseudo algebraic structure is presented. There a “Lawvere theory” for monoidal categories is a 2category with all the coherent isomorphisms α, λ, ρ explicit as 2-cells. This allows
one to have a model as a (strict) 2-functor. In contrast, in our approach, monoids
and monoidal categories are specified by the same Lawvere theory MonTh without any 2-cells; the former is an FP-functor into Set and the latter a pseudo
FP-functor into CAT.
4.2

Inner model: L-object

Once we have an outer model C of L, we can define the notion of inner modelin C. It is a family of objects {XS ∈ C(S)}S∈S which carries L-structure in
the same way as a monoid object in a monoidal category carries structure as a
monoid [24, §VII.3]. Its relevance to component calculi is explained in §2 where
final coalgebras carry an inner model and realize composition of behaviors.
Definition 4.5 (L-object) Let C : L → CAT be an L-category. An L-object
in C is a lax natural transformation (see e.g. [8])

L

1
⇓X
C

CAT

which is FP-preserving in the sense that: it is strictly natural with regard toprojections and diagonals (see [12, Def. 3.4]). Here 1 : L → CAT denotes theconstant functor to a (chosen) terminal category 1.
An L-object is also called a microcosm model of L, emphasizing that it is amodel that resides in another model C.
The definition is abstract and it might be hard to grasp how it works. While thereader is referred to [11, 12] for its illustration, we shall point out its highlights.
An L-object X, as a lax natural transformain CAT
in L
XAtion, consists of the following data:
1

C(A)
JaK
Xa
C(B)

⇒

A
a
B

– its components XA : 1 → C(A), identified with1
objects XA ∈ C(A), for each A ∈ L;
XB
– mediating 2-cells Xa , as shown on the right, for each morphism a in L.

10

Generalizing the illustration in [11, 12] one immediately sees that
– X’s components are determined by those {XS }S∈S for sorts. The latterextend to an object S1 × · · · × Sm by:∼=C(S1 × · · · × Sm ) ∋ XS1 ×···×Sm 7−→ (XS1 , . . . , XSm ) ∈ C(S1 ) × · · · × C(Sm ) ;– an operation σ is interpreted on X by means of the mediating 2-cell Xσ ;– equations hold due to the coherence condition on the mediating 2-cells.
4.3

Categorical compositionality

Here we shall present a main technical result, namely the compositionality theorem (Thm. 4.7). It is a straightforward many-sorted adaptation of [12, Thm. 3.9],
to which we refer for its proof and more illustration.
Definition 4.6 (L-functor) Let C, D be L-categories. A lax L-functor F : C →D is a lax natural transformation L

C⇓F

CAT that is FP-preserving in theDsame sense as in Def. 4.5. Similarly, a strict L-functor is a strict natural transformation of the same type.
A lax/strict L-functor determines, as its components, a family of functors {FA :C(A) → D(A)}A∈L . Much like the case for an L-object, it is determined by thecomponents {FS : C(S) → D(S)}S∈S on sorts.
Theorem 4.7 (Compositionality) Let C be an L-category, and F : C → C be∼=a lax L-functor. Assume further that there is a final coalgebra ζA : ZA →FA (ZA )for each A ∈ L.
1. The family {Coalg(FA )}A∈L carries an L-category.
2. The family {ζA ∈ Coalg(FA )}A∈L carries a microcosm model of L.
3. The family {C(A)/ZA }A∈L of slice categories carries an L-category.
4. The family of functors {behA : Coalg(FA ) → C(A)/ZA }A∈L , where
FA X
behA : Coalg(FA ) −→ C(A)/ZA

is by coinduction

is a strict L-functor.

cX

FA (ZA )final ∼=
behA (c)ZA⊓⊔

An informal reading of the theorem is as follows. To get a “nice” interpretationof a component calculus L by F -coalgebras, it suffices to check that– the base category C models L, and– the functor F is “lax-compatible” with L.
These data interpret L on the category of coalgebras, yielding composition ofcomponents (the point 1.). Final coalgebras acquire canonical inner L-structure,yielding composition of behaviors (the point 2.). Finally, relating the two interpretations, compositionality is guaranteed (the point 4.).

11

5Taxonomy of FP-theories for component calculi

Up to now we have kept an FP-theory L as a parameter and have developed auniform framework that applies to any L. Now we start looking at: concrete models (components as coalgebras); and three concrete FP-theories PLTh, ArrTh
and MArrTh that express basic component calculi. The latter two are equippedwith different “parallel composition” operations.
Notably the algebraic structure expressed by ArrTh is that of (Hughes’)arrow [14], equivalently that of Freyd categories [23], the notions introduced formodeling structured computations in functional programming.
The main result in this section is that the categories {Coalg(FI,J )}I,J —modeling components with FI,J = (T (J × ))I —carry ArrTh-structure. If additionally the effect monad T is commutative, then {Coalg(FI,J )}I,J a forteriori carries stronger MArrTh-structure. These results parallel classic resultsin categorical semantics of functional programming, investigating (pre)monoidal
structure of a Kleisli category.
5.1

The FP-theories ArrTh, MArrTh

We shall add, to the FP-theory PLTh in §3.2, a suitable “parallel composition”
operation and equational axioms to obtain the FP-theory ArrTh. By imposing
stronger equational axioms we get the FP-theory MArrTh.
In ArrTh one has additional sideline operations!
I

firstI,J,K : (I, J) −→ (I × K, J × K) ,graphicallyafirstI,J,K

7−→

J

I

K

J

K

a

for each I, J, K ∈ B. The equations regarding these are:first a >>> arr π = arr π >>> a(ρ-Nat)first a >>> arr(id × f ) = arr(id × f ) >>> first a
first a >>> arr α = arr α >>> first(first a)(arr-Centr)(α-Nat)first(arr f ) = arr(f × id)
first(a >>> b) = first a >>> first b(arr-Premon)(first-Func)

It is easy to recover the omitted subscripts for arr, >>> and first. In the equations,f denotes a morphism in the base category B. In (ρ-Nat), if a has the type (I, J)∼=
then the π on the left is the projection π : J × 1 →J in B. In (α-Nat), α’s are∼=associativity isomorphisms like I × (J × K) → (I × J) × K in B.
Remark 5.1 In fact the equation (ρ-Nat) holds for any projection π : J ×
K → J without requiring K = 1; one can derive this general case from thespecial case and other equations. However, the special case has a clearer role inthe corresponding premonoidal structure (see §5.2). Namely, it is the naturality∼=
requirement of the right-unit isomorphism ρJ = arr πJ with πJ : J × 1 →J.

12In MArrTh, instead of the operations first, one has
kI,J,K,L : (I, J) × (K, L) −→ (I × K, J × L)

synchronous composition

for each I, J, K, L ∈ B. The equations are:(a k b) >>> (c k d) = (a >>> c) k (b >>> d)(k-Func1)

arr id k arr id = arr id
a k (b k c) >>> arr α = arr α >>> (a k b) k c(a k arr id1 ) >>> arr π = arr π >>> a(k-Func2)(α-Nat)(ρ-Nat)arr(f × g) = arr f k arr g(a k b) >>> arr γ = arr γ >>> (b k a)(arr-Mon)(γ-Nat)∼=Here α’s are associativity isomorphisms, and π’s are projections like J × 1 →J,as in ArrTh. The morphisms γ in (γ-Nat) are symmetry isomorphisms like∼=J ×I →I ×J in B. One readily derives, from (ρ-Nat) and (γ-Nat), the equation(arr id1 k a) >>> arr π ′ = arr π ′ >>> a(λ-Nat)∼=where π ′ ’s are (second) projections like 1 × I →I.
The reason that we have the first operation in ArrTh, instead of k as in
MArrTh, should be noted. The first operation in ArrTh yields the operation

secondI,J,K : (I, J) −→ (K × I, K × J) by second a = arr γ >>> first a >>> arr γ , where γ’s are symmetry isomorphisms. But the equa- KIaKtions in ArrTh do not derive second b >>> first a =  I b  first a >>> second b; that is, the two systems on the  a L  6=  J b JLright should not be identified. Indeed there are many
situations where these two systems are distinct. Assume that we have the global
state monad T = (S × )S as effect in FI,J . One can think of a global states ∈ S as residing in the ambience of components, unlike local/internal statesthat are inside components (i.e. coalgebras). When a component executes, itchanges the current global state as well as its internal state; hence the order of
execution of a and b does matter. In contrast, when one interprets MArrTh in{Coalg(FI,J )}I,J , the natural axiom (k-Func1) requires the above two systems
to be equal.
5.2

Set-theoretic models: arrows, Freyd categories

The FP-theories PLTh, ArrTh and MArrTh and their set-theoretic models
are, in fact, closely related with some notions that have been studied extensively
in semantics of functional programming. Here we elaborate on the relationship;
it will be exploited later in §5.3.
To start with, ArrTh is almost exactly a categorical presentation of theaxiomatization of Hughes’ arrow [14] (specifically the axiomatization in [19]),

13

the only gap being the one explained in Remark 5.1. The notion of arrow generalizes that of monad (modeling effects, i.e. structured output [25, 31]) andthat of comonad (modeling structured input [30]); the notion of arrow models“structured computations” in general. See e.g. [19, §2.3].
Definition 5.2 An arrow is a set-theoretic model (Def. 3.2) of ArrTh.
It had been folklore, and was proved in [19], that an arrow is the same thing
as a Freyd category. A Freyd category is a symmetric premonoidal category K
together with a Cartesian category B embedded via an identity-on-object strict
premonoidal functor B → K, subject to a condition on center morphisms. The
notion is introduced in [28], and it is named as such later in [23].
In this way one can look at ArrTh as an axiomatization of the notion of
Freyd category. There is a similar corresponding structure for the (stronger)
FP-theory MArrTh, which explains its name MArrTh.
Definition 5.3 Let B be a Cartesian (hence monoidal) category. A monoidal
Freyd category on B is a symmetric monoidal category K together with a strictly
monoidal, identity-on-object functor B → K.
Proposition 5.4 1. A set-theoretic model ArrTh → Set of ArrTh is thesame thing as a Freyd category.
2. A set-theoretic model MArrTh → Set of MArrTh is the same thing as a
monoidal Freyd category.
Proof. The first point is simply the correspondence result [19, Thm. 6.1] between
arrows and Freyd categories, put together with Def. 4.5. The proof of the second
point goes similar.
⊓⊔
Remark 5.5 To be precise, the correspondences in the previous proposition areequivalences of suitable categories. This is for the same reason as the category of
set-theoretic models of the Lawvere theory MonTh is equivalent to the category
Mon of monoids. These correspondences fail to be isomorphisms because of thepossible different choices of products in Set.
The notions of (monoidal) Freyd category were introduced in [28], prior toarrows, as axiomatizations of the structure possessed by a Kleisli category Kℓ(T )for a monad T . Here a Kleisli category is understood as a category of types andeffectful computations [25]. The results [28, Cor. 4.2 & 4.3]—showing that Kℓ(T )indeed induces a Freyd category—now read as follows, in view of Prop. 5.4. For
the notion of strong/commutative monad, see e.g. [16, §3].
Proposition 5.6 Let B be our base category (see Assumption 3.3).
1. A monad T on Set induces a model Kℓ(T ) : ArrTh → Set. Specifically,
its carrier set Kℓ(T )(I, J) for the sort (I, J) is the homset HomKℓ(T ) (I, J);
arr is interpreted by the Kleisli inclusion functor; >>> is by composition inKℓ(T ); and first is obtained using the canonical strength st of T . Recall thatevery monad on Set is strong.

14

2. Furthermore, if T is commutative then it induces a model Kℓ(T ) of MArrTh.
The operation k is interpreted using T ’s double strength.
⊓⊔
Thanks to the proposition we know that all the equations in ArrTh or in
MArrTh hold in Kℓ(T ), with the operations suitably interpreted. This fact
will be heavily exploited in the equational reasoning later in §5.3.
For PLTh—the parallel-free part of ArrTh and MArrTh—a set-theoretic
model is an arrow without first, or equivalently, a category K with an identity-onobject functor B → K. Yet another characterization of this structure, discoveredin [19], is as a monoid object in the monoidal category of bifunctors [Bop ×
B, Set] where the monoidal products are given by the so-called Day tensor [9].
Equivalently, it is a monad on B in the bicategory of profunctors (also called
distributors or bimodules, see e.g. [6, 8]).
5.3

PLTh, ArrTh and MArrTh as component calculi

We now show that our coalgebraic modeling of components indeed models thecalculi PLTh, ArrTh and MArrTh, according to the choice of an effect monadT . The result parallels Prop. 5.6.
Throughout the rest of the section we denote by LCC any one of PLTh,
ArrTh and MArrTh (CC for “component calculus”).
In view of Thm. 4.7, we only need to establish that: 1) the (constant) map(I, J) 7→ Set extends to an LCC -category; and 2) {FI,J : Set → Set}I,J extends
to a lax LCC -functor. Then Thm 4.7 ensures that the components (as coalgebras)
and their behaviors (as elements of final coalgebras) carry a microcosm modelof LCC , and that compositionality holds.
For 1), we interpret the operations in the following way. The guiding question is: what is the state space of the resulting component, when we apply an
operation to components as its arguments.
Definition 5.7 We denote by Set the LCC -category defined as follows. It maps
each sort (I, J) to Set ∈ CAT; and it interprets operations by
Jarr f K

1 −→ Set,∗ 7−→ 1

JfirstK

Set −→ Set,
X 7−→ X

J>>>K

Set × Set −→ Set,
(X, Y ) 7−→ X × Y

JkK

Set × Set −→ Set.
(X, Y ) 7−→ X × Y

We are using the same notation Set for models of three different FP-theories.
This will not cause confusion.
Lemma 5.8 The data in Def. 5.7 indeed determine FP-preserving pseudo functors. In particular, all the equations in PLTh, ArrTh and MArrTh are satisfied up-to coherent isomorphisms.
Proof. Easy. The equations hold only up-to isomorphisms because, for example,⊔
the associativity X × (Y × U ) ∼= (X × Y ) × U in Set is only an isomorphism. ⊓15

The requirement 2)—that {FI,J : Set → Set}I,J∈B extends to a lax LCC functor—puts additional demands on T . This is parallel to Prop. 5.6. Still theactual calculation is overwhelming. We notice that all the operations that appear
throughout the calculation can be described as morphisms in the Kleisli category
Kℓ(T ). Therefore, by Prop. 5.6, they are themselves subject to the equations in
LCC . This substantially simplifies the calculation.
Lemma 5.9 For the endofunctors FI,J = (T (J × ))I : Set → Set, the following hold.
1. The family {FI,J : Set → Set}I,J extends to a lax ArrTh-functor Set →Set. Therefore so it does to a lax PLTh-functor.
2. If T is commutative, {FI,J : Set → Set}I,J extends to a lax MArrThfunctor Set → Set.
Proof. What we need to do is: first to “interpret operations” on {FI,J }I,J ; second
to check if these interpreted operations “satisfy equations.”
More specifically, to make {FI,J }I,J into a lax LCC -functor, we need to havea mediating 2-cell corresponding to each operation (such as >>>). For example:
in LCCin CAT

Set × Set
J>>>K = ×
Set

FI,J × FJ,K⇓(I, J) × (J, K)>>>(I, K)

Set × Set
J>>>K = ×
F>>>
Set

(7)

FI,K

In the diagram, we have denoted the binary product in Set by the boldface
× : Set × Set → Set to distinguish it from the binary product × in CAT. The
needed 2-cell F>>> is nothing but a natural transformation
F>>> : FI,J X × FJ,K Y −→ FI,K (X × Y ) .

(8)

After that we have to show that these mediating 2-cells satisfy the coherence
condition. In the current setting where the domain category LCC is syntacticallygenerated by sorts, operations and equations, it amounts to checking if the mediating 2-cells “satisfy the equations.” Taking (>>>-Assoc) as an example, itmeans showing the following equality between 2-cells.

F>
>
>

FI,L

Set

2

×

Set

××id

=

Set

2

×

Set

Set3
××id

F>
>
> ×id

FI,K ×FK,L

⇓

Set

⇓

×

id×F>
>
>

FI,K ×FK,L

×
id××

FI,J ×FJ,K ×FK,L

Set2
×

F>
>
>

FI,L

⇐
α

×)
× ◦(id××

Set

2

Set3

Set3

⇓

×
id××
⇐
α

FI,J ×FJ,K ×FK,L

⇓

××id)
× ◦(×

Set3

(9)

Set
∼

=
Here α denotes the associativity isomorphism X × (Y × U ) →(X × Y ) × U .
See [11, Rem. 5.4.1] for more illustration. One readily sees that the equation (9)16boils down to commutativity of the following diagram in Set.
FI,J X × (FJ,K Y × FK,L U )α(FI,J X × FJ,K Y ) × FK,L U

id × F>>>

F>>> × id

FI,J X × FJ,L (Y × U )FI,K (X × Y ) × FK,L U

F>>>

F>>>

FI,L (X × (Y × U ))FI,L αFI,L ((X × Y ) × U )(10)

To summarize: we shall introduce a natural transformation Fσ , for each operation σ, like in (8); and check if they satisfy all the equations like in (10). While
the first task is straightforward, the second is painfully complicated as it is. We
shall only do the aforementioned examples in LCC for demonstration.
In the sequel, let us denote the set-theoretic model of LCC induced by the
Kleisli category (in Prop. 5.6) by Kℓ(T ). In particular, we have Kℓ(T )(I, J) =(T J)I . Hence the natural transformation F>>> in (8) is of the typeKℓ(T )(I, J × X) × Kℓ(T )(J, K × Y ) → Kℓ(T )(I, K × (X × Y )) .
We define it to be the following composition of morphisms in LCC , interpretedin Kℓ(T ).
`´
id×first(I, J × X) × (J, K × Y ) −→ (I, J × X) × J × X, (K × Y ) × X´ ( )>>>(arr α−1 )>>> `−→ I, (K × Y ) × X−→(I, K × (X × Y ))(11)

One can readily come up with such a morphism in LCC for each of the otheroperations.
Let us prove that F>>> thus defined satisfies (10). The morphisms in the
diagram (10) can be also written as morphisms in LCC , interpreted in Kℓ(T ).
Hence we shall do the equational reasoning in LCC , using the equational axioms
in §5.1. To reduce the number of parentheses, the terms are presented modulo
associativity (>>>-Assoc) of >>>. The letters c, d and e are variables of sorts(I, J × X), (J, K × Y ) and (K, L × U ), respectively.
(The path, first down, then to the right)= c >>> first d >>> arr α−1 >>> first e >>> arr α−1= c >>> first d >>> first first e >>> arr α−1 >>> arr α−1(α-Nat)−1= c >>> first d >>> first first e >>> arr (α◦ α−1 )
(arr-Func1)`´= c >>> first d >>> first first e >>> arr (L × α) ◦ α−1 ◦ (α−1 × U )(†)= c >>> first d >>> first first e >>> arr (α−1 × U ) >>> arr α−1 >>> arr (L × α)
(arr-Func1)−1−1= c >>> first`d >>> first first e >>> first (arr´ α ) >>> arr α >>> arr (L × α) (first-Premon)= c >>> first (d >>> first e) >>> arr α−1 >>> arr α−1 >>> arr(L × α)
(first-Func)= (The path, first to the right, then down)

Here the equality (†) is because of the “pentagon” coherence for α in Set. Naturality of F>>> in X, Y , as well as satisfaction of the other equations, can bederived by similar calculation.
⊓⊔
For obtaining a microcosm model we need final coalgebras. This depends on the“size” of the monad T ; all the examples of T listed in §1, except for T = D,satisfy the requirement.

17

Theorem 5.10 Assume that, for each I, J ∈ B, we have a final coalgebra ζI,J :∼=ZI,J →
FI,J (ZI,J ).
1. The family {Coalg(FI,J )}I,J forms an ArrTh-category, so a PLTh-category.
2. The family {ZI,J ∈ Set}I,J forms an ArrTh-object, hence a PLTh-object.
Compositionality holds in the sense of Thm. 4.7.4.
3. If T is commutative, then the above two are also an MArrTh-category andan MArrTh-object, respectively.
Proof. By Thm. 4.7, Lem. 5.8 and Lem. 5.9.

6⊓⊔Conclusions and Future Work

We have extended our previous formalization of the microcosm principle [12] toa many-sorted setting. This allowed to include Barbosa’s component calculi [2]as examples. We studied three concrete calculi that are variants of the axiomatization of arrows, demonstrating similarity between components and structured
computations.
As future work, we are interested in further extensions of the component calculi that allow modeling of further interesting examples like wiring and merging
components, queues, stacks, and folders of stacks with feedback, etc., as presented in [2]. The proof methods that we derived from the microcosm framework
will be useful in its course.
On the more abstract side, it is interesting to elevate the arguments in §5
further, to the bicategory DIST of distributors, with CAT embedded in it via
the Yoneda embedding. Such a higher level view on the matter might reveal
further microcosm instances in our proof methods.
Acknowledgments Thanks are due to Kazuyuki Asada, Masahito Hasegawa,Paul-André Melliès and John Power for helpful discussions and comments.

References
1. J.C. Baez and J. Dolan. Higher dimensional algebra III: n-categories and thealgebra of opetopes. Adv. Math, 135:145–206, 1998.
2. L.S. Barbosa. Towards a calculus of state-based software components. Journ. of
Universal Comp. Sci., 9(8):891–909, 2003.
3. L. Barbosa. Components as Coalgebras. PhD thesis, Univ. Minho, 2001.
4. M. Barr and C. Wells. Toposes, Triples and Theories. Springer, Berlin, 1985.
Available online.
5. M. Barr and C. Wells. Category Theory for Computing Science. Centre derecherches mathématiques, Université de Montréal, 3rd edn., 1999.
6. J. Bénabou. Distributors at work. Lecture notes by Thomas Streicher, 2000.
www.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf.gz.
7. M.M. Bonsangue, J.J.M.M. Rutten and A. Silva. Coalgebraic logic and synthesisof Mealy machines. In R.M. Amadio, editor, FoSSaCS, vol. 4962 of Lect. Notes
Comp. Sci., pp. 231–245. Springer, 2008.

18
8. F. Borceux. Handbook of Categorical Algebra, vol. 50, 51 and 52 of Encyclopediaof Mathematics. Cambridge Univ. Press, 1994.
9. B.J. Day. On closed categories of functors. In Reports of the Midwest Category
Seminar IV, vol. 137 of Lect. Notes Math., pp. 1–38. Springer-Verlag, 1970.
10. K. Denecke and S.L. Wismath. Universal Algebra and Applications in TheoreticalComputer Science. Chapman & Hall, 2002.
11. I. Hasuo. Tracing Anonymity with Coalgebras. PhD thesis, Radboud University
Nijmegen, 2008.
12. I. Hasuo, B. Jacobs and A. Sokolova. The microcosm principle and concurrency incoalgebra. In Foundations of Software Science and Computation Structures, vol.
4962 of Lect. Notes Comp. Sci., pp. 246–260. Springer-Verlag, 2008.
13. C. Hermida. A roadmap to the unification of weak categorical structures: transformations and equivalences among the various notions of pseudo-algebra, 2004.
maggie.cs.queensu.ca/chermida/papers/roadmap.pdf.
14. J. Hughes. Generalising monads to arrows. Science of Comput. Progr., 37(1–3):67–
111, 2000.
15. M. Hyland and J. Power. The category theoretic understanding of universal algebra: Lawvere theories and monads. Elect. Notes in Theor. Comp. Sci., 172:437–458,
2007.
16. B. Jacobs. Semantics of weakening and contraction. Ann. Pure & Appl. Logic,
69(1):73–106, 1994.
17. B. Jacobs. Categorical Logic and Type Theory. North Holland, Amsterdam, 1999.
18. B. Jacobs and J.J.M.M. Rutten. A tutorial on (co)algebras and (co)induction.
EATCS Bulletin, 62:222–259, 1997.
19. B. Jacobs, C. Heunen and I. Hasuo. Categorical semantics for arrows. Journ.
Funct. Progr., 2009. To appear.
20. A. Joyal and R. Street. Braided tensor categories. Adv. Math, 102:20–78, 1993.
21. S. Lack and J. Power. Lawvere 2-theories. Presented at CT2007, 2007.
www.mat.uc.pt/~categ/ct2007/slides/lack.pdf.
22. F.W. Lawvere. Functorial Semantics of Algebraic Theories and Some Algebraic
Problems in the Context of Functorial Semantics of Algebraic Theories. PhD thesis,
Columbia University, 1963. Reprints in Theory and Applications of Categories, 5(2004) 1–121.
23. P.B. Levy, A.J. Power and H. Thielecke. Modelling environments in call-by-value
programming languages. Inf. & Comp., 185(2):182–210, 2003.
24. S. Mac Lane. Categories for the Working Mathematician. Springer, Berlin, 2ndedn., 1998.
25. E. Moggi. Notions of computation and monads. Inf. & Comp., 93(1):55–92, 1991.
26. D. Pattinson. An introduction to the theory of coalgebras. Course notes for
NASSLLI, 2003.
www.indiana.edu/~nasslli.
27. A.J. Power. Why tricategories? Inf. & Comp., 120(2):251–262, 1995.
28. J. Power and E. Robinson. Premonoidal categories and notions of computation.
Math. Struct. in Comp. Sci., 7(5):453–468, 1997.
29. J.J.M.M. Rutten. Algebraic specification and coalgebraic synthesis of Mealy automata. Elect. Notes in Theor. Comp. Sci., 160:305–319, 2006.
30. T. Uustalu and V. Vene. Comonadic notions of computation. Elect. Notes in
Theor. Comp. Sci., 203(5):263–284, 2008.
31. P. Wadler. Monads for functional programming. In Marktoberdorf Summer Schoolon Program Design Calculi. Springer-Verlag, 1992.