Under consideration for publication in J. Functional Programming

1

Categorical semantics for arrows
Bart Jacobs, Chris Heunen, Ichiro Hasuo
Institute for Computing and Information Sciences
Radboud University, Nijmegen, the Netherlands(e-mail: {b.jacobs,c.heunen,i.hasuo}@cs.ru.nl)

Abstract
Arrows are an extension of the well-established notion of a monad in functional programming languages. This article presents several examples and constructions, and develops
denotational semantics of arrows as monoids in categories of bifunctors Cop ×C → C. Observing similarities to monads – which are monoids in categories of endofunctors C → C– it then considers Eilenberg-Moore and Kleisli constructions for arrows. The latter yields
Freyd categories, mathematically formulating the folklore claim “arrows are Freyd categories”.

Contents
1 Introduction
2 Haskell examples
2.1 Monads
2.2 Arrows
2.3 Monads versus arrows
3 Arrow constructions and examples
4 Categorical formulation
4.1 Analysing arrow behaviour categorically
4.2 Monoidal structure in the ambient category
4.3 Internal strength
4.4 The categorical definition
5 Biarrows
6 Kleisli and Eilenberg-Moore constructions for arrows
6.1 Arrows are Freyd categories
6.2 Eilenberg-Moore algebras for arrows
6.3 Freyd is Kleisli, for arrows
7 Conclusion
A Coends
B Bicategorical characterisation
C 2-categorical details in the Kleisli construction for arrows
References

2
3
3
4
5
7
10
10
12
14
16
16
18
18
21
25
28
29
32
33
35

2

Jacobs, Heunen, Hasuo
1 Introduction

The motivation to introduce the concept of an arrow comes from functional programming (Hughes, 2000; Paterson, 2001). It is intended as a uniform interface tocertain types of computations, streamlining the infrastructure. This enables a highlevel of abstraction to uniformly capture for instance quantum computing (Vizzotto et al., 2006+). It also facilitates language extensions like secure information
flow (Li & Zdancewic, 2008): instead of building a domain-specific programming
language from the ground up, it can be defined within normal Haskell using thearrow interface. After all, arrows provide an abstract interface supporting familiar programming constructs like composition, conditional branches and iteration.
Haskell even incorporates convenient syntax to ease the use of such language extensions. The name “arrow” reflects the focus on the provided infrastructure, especiallycompositionality.1
Here is a more mathematical intuition. Monoids are probably the most fundamental mathematical structures used in computer science. The basic example(A, ; , skip) is given by a set A ∈ Set of programs or actions, with sequential composition ; as binary operation, and an empty statement skip as neutral element forcomposition. Such a monoid A does not capture input and output. We may liketo add it via parametrisation A(X, Y ), where X, Y are type variables. Since input
is contravariant and output covariant, we may consider such an indexed monoid
A(−, +) as a bifunctor Cop × C → Set for a suitable category C of types for input
and output. But of course, we still want it to have a monoid structure for composition. Hence we are led to consider monoids in the functor category Cop × C → Set.
Our first main result – stemming from (Heunen & Jacobs, 2006) – is that suchmonoids are in fact arrows as introduced by Hughes.
A special case of the above is when there is only output, but no input: these singly
indexed monoids are (categorical) monads. They correspond to the well-known
notion of a monad in Haskell (Moggi, 1989; Wadler, 1992). Arrows are thus similar
to monads in that they are monoids in suitable categories: namely in categories of
endofunctors C → C. Hence we are led to ask: what are the Eilenberg-Moore andKleisli constructions – two very basic constructions on monads – for arrows? Our
second main result – from (Jacobs & Hasuo, 2006) – is that the Kleisli construction
for arrows corresponds to Freyd categories (Robinson & Power, 1997), and moreoverthe correspondence is isomorphic. Thus, to the folklore claim “arrows are Freyd
categories” that we put in precise terms, we add the slogan “Freyd is Kleisli, forarrows”.
These main results are streamlined versions of (Heunen & Jacobs, 2006) and(Jacobs & Hasuo, 2006). The current article proceeds as follows. In Section 2 weintroduce the concepts of monads and arrows in Haskell more thoroughly, gradually
moving towards a more mathematical mindset instead of a functional programming
perspective. We also motivate why one can in fact achieve more with arrows than

1 In a categorical context, the name is a bit unfortunate, however. We consistenly use “arrow”

for the programming construct and “morphism” for the categorical notion.

Categorical semantics for arrows

3with monads, and give settings where this is useful. Section 3 investigates, still ina somewhat discursive style, combinations of arrows. It leads up to a deconstruction into elementary parts of the particular program that motivated Hughes to use
arrows in the first place (Swierstra & Duponcheel, 1996). The formal, categorical,
analysis of arrows takes place in Section 4, culminating in our first main result
mentioned above, Corollary 4.1. An example showing the elegance of this approachis discussed in Section 5, namely arrows facilitating bidirectional computation. Section 6 then considers algebra constructions for arrows, and contains the second
main result, Theorem 6.2. We conclude in section 7. Appendix A contains a proofof a result used in Section 4 but only sketched there. Next, Appendix B considers
a bicategorical characterisation of the notion of arrow that elegantly exemplifies its
naturality, but is somewhat out of the scope of the main line of this article. Finally,
Appendix C gives the missing details of Section 6.
2 Haskell examples
This section introduces arrows and their use in functional programming languages.
We briefly consider monads first in subsection 2.1, since this construction fromcategory theory historically paved the way for arrows (subsection 2.2). Subsection
2.3 then consider the advantages of arrows over monads.
2.1 Monads
A major reason for the initial reluctance to adopt functional programming languages
is the need to pass state data around explicitly. Monadic programming provides ananswer to this inconvenience (Moggi, 1989; Wadler, 1992). Through the use of amonad one can encapsulate the changes to the state data, the “side-effects”, without explicitly carrying states around. monads can efficiently structure functional
programs while improving genericity. This mechanism is even deemed importantenough to be incorporated into Haskell syntax (Peyton Jones, 2003). A monad in
Haskell is defined as a so-called type class:class

M onad M wherereturn:: X → M X(>>=):: M X → (X → M Y ) → M Y

To ensure the desired behaviour, the programmer herself should prove certain
monad laws about the operations return and >>= (pronounced bind ). These boil
down to the axioms that M be a monad, in the categorical sense. Using the formulation that is standard in the functional programming community, a categoricalmonad consist of a mapping X 7→ M (X) on types, together with “return” and“bind” functionsXrt/ M X,(X → M Y )bd/ (M X → M Y )satisfying
bd(f ) ◦ rt = f,bd(rt) = id,bd(f ) ◦ bd(g) = bd(bd(f ) ◦ g).

4

Jacobs, Heunen, Hasuo

In categorical style one defines M to be a functor, with multiplication maps µ =bd(idM X ) : M 2 X → M X satisfying suitable laws. The above equations are moreconvenient for equational reasoning. Often one writes u >>= f for bd(f )(u).
The most familiar monads are powerset, list, lift, state and distribution:SP
rt(x) = {x}bd(f )(a) = {f (x) | x ∈ a}(−)?
rt(x) = hxi
bd(f )(hx1 , . . . , xn i) = f (x1 ) · . . . · f (xn )⊥if v = ⊥1 + (−)
rt(x) = up(x)bd(f )(v) =f (x) if v= up(x)
(− × S)S rt(x) = λs . hx, si
bd(f )(h) = λs . f π1 h(s) π2 h(s)X
1 if x = yDrt(x) = λy .
bd(f )(ϕ) = λy .
ϕ(x) · f (x)(y)0 if x 6= yx
In the latter case we write D for the ‘subdistribution’ monad D(X) = {ϕ : X →P[0, 1] | supp(ϕ) is finite andx ϕ(x) ≤ 1}, where the support supp(ϕ) is the set ofx ∈ X with ϕ(x) > 0.
Monads are often considered with strength, i.e. come equipped with a suitable
natural transformation st : M (X) × Y → M (X × Y ). For later reference, we usethat in our present informal setting each functor M is strong, as its strength canbe described explicitly as:st(u, y) = M λx . hx, yi (u).
(1)
It satisfies the following basic equations.
M (f × g) ◦ st = st ◦ (M (f ) × g),
M (π1 ) ◦ st = π1 ,M (α−1 ) ◦ st = st ◦ (st × id) ◦ α−1 ,where we use
πi : X 1 × X 2 → X i ,∼=α : (X × Y ) × Z −→ X × (Y × Z),

for the familiar product maps fst, snd and assoc.
In other, non-set-theoretic settings one may have to require such strength maps
explicitly. The monad operations interact appropriately with the above strength
map, in the sense that the following equations hold.
st ◦ (rt × id) = rtst ◦ (bd(f ) × g) = bd(st ◦ f × g) ◦ st.

In effect, monads are thus functional combinators. They enable the combinationof functions very generally, without many assumptions on the precise functions to
combine. However, these restrictions are severe enough to exclude certain classes oflibraries from implementation with a monadic interface.

2.2 Arrows
Arrows are even more general functional combinators, and can be seen as a generalisation of monads (Hughes, 2000; Hughes, 2005). An arrow in Haskell is a type

Categorical semantics for arrows

5class of the form
class

Arrow A wherearr:: (X → Y ) → A X Y(>>>):: A X Y → A Y Z → A X Z
f irst:: A X Y → A (X, Z) (Y, Z)

where X, Z in Haskell denotes the Cartesian product type X × Y . Analogous tomonads, an arrow must furthermore satisfy the following arrow laws, the proof ofwhich is up to the programmer.
(a >>> b) >>> c = a >>> (b >>> c),(2)arr (g ◦ f ) = arr f >>> arr g,(3)

arr id >>> a = a = a >>> arr id,(4)

f irst a >>> arr π1 = arr π1 >>> a,(5)

f irst a >>> arr (id × f ) = arr (id × f ) >>> f irst a,(6)

f irst (f irst a) >>> arr α = arr α >>> f irst a,(7)

f irst (arr f ) = arr (f × id),(8)

f irst (a >>> b) = f irst a >>> f irst b,(9)

In fact, as Section 6.1 shows, less structure than Cartesian products suffices, eliminating the need for projections πi in the above arrow laws. Sometimes, arr(id × f )is written as second(arr(f )), where
second(a)= arr(γ) >>> f irst(a) >>> arr(γ),∼=

and γ : X × Y −→ Y × X is the well-known swap-map. The arrow laws (2)–(9)are sometimes given names (Paterson, 2003). Especially noteworthy are the names“exchange” for (6) and “extension” for (8).
Example of arrows will be given in Section 3.

2.3 Monads versus arrows
This article is concerned with a categorical understanding of this notion of arrow.
At this stage we shall reveal some of the structure involved, but are deliberately
a bit vague about the general setting in which we are working. In doing so wemove to a more mathematical notation, for instance writing A(X, Y ) for A X Y infunctional style.
It is not hard to show that an arrow is “bifunctorial” (Lemma 4.1). This meansthat for f : X 0 → X and g : Y → Y 0 one also has a map A(X, Y ) → A(X 0 , Y 0 ).
The maps arr : Y X → A(X, Y ) then form natural transformations (Lemma 4.2).
Even more, composition can also be seen as a natural transformation A ⊗ A → A,
for a suitable tensor product ⊗ of bifunctors (Proposition 4.2). In this way one
can describe the triple (A, arr, >>>) as a monoid in a category of bifunctors. Here
we shall not need these details yet. But in the remainder of this section we shallintroduce arrows as bifunctors of the form Cop × C → Set.

6

Jacobs, Heunen, Hasuo

Here is a first trivial example. Let (P, m, e) be a monoid, consisting of an associative operation m : P × P → P with two-sided unit e : P . It yields probably themost elementary example of an arrow, namely a constant one. We shall also write
it as P , formally as functor in P (X, Y ) = P , with operations:arr(f ) = e,a >>> b = m(a, b)

f irst(a) = a.

Standard examples of monoids P are the singleton type 1 (with trivial operations),
the type 2 = {0, 1} of truth values or Booleans (with either conjunctions >, ∧ or
disjunctions ⊥, ∨), or the type X ? of lists of an arbitrary type X (with the empty
list hi and concatenation ·).
Every monad (M, rt, bd) with a strength gives rise to an arrow M by
M (X, Y ) = M (Y )X ,(10)

with obvious operations (see e.g. Hughes, 2000) – strength is used to provide theoperation f irst.
Dual to a monad, a comonad is given by a mapping X 7→ N (X) with “coreturn”
and “cobind” operations crt : N X → X and cbd : (N X → Y ) −→ (N X → N Y )satisfying
crt ◦ cbd(f ) = f,cbd(crt) = id,

cbd(f ) ◦ cbd(g) = cbd(f ◦ cbd(g)).

It gives rise to an arrow by (X, Y ) 7→ Y N (X) – no strength is needed.
Comonads are less well-known, but are fundamental structures for handling contexts (among other things), in which the “counit” ε = crt : N X → X is used forweakening, and the “comultiplication” δ = cbd(idN X ) : N X → N 2 X for contraction (Jacobs, 1999). The following diagram presents the main comonads X 7→ · · ·for handling streams with discrete time input (Uustalu & Vene, 2005).
X? × X ocausality
no future(hα(0), . . . , α(n − 1)i, α(n)) o

XN × N

anti-causality
no past (α, n) 

/ XN

(11)

/ λm . α(n + m)

The intuition for a pair (α, n) ∈ X N ×N is that n represents the present stage in thestream α = hα(0), α(1), . . . , α(n − 1), α(n), α(n + 1), . . .i, where everything before
n is past input, and everything after n is future input. The two morphisms in theprevious diagram are homomorphisms of comonads, commuting with the relevantcomonad/context structure. There is a similar real-time analogue.
A strong monad M and a comonad N can also be combined to form arrows.
As illustrated for instance in (Uustalu & Vene, 2005; Heunen & Jacobs, 2006),
this happens via a so-called distributive law N M ⇒ M N that commutes with the(co)monad operations. Then one can define an arrow (M, N ) via(M, N )(X, Y ) = M (Y )N (X) .

(12)

It combines the previous two constructions with monads and comonads separately.
This mapping (X, Y ) 7→ M (Y )N (X) leads to an appealing picture of an arrow inwhich the monad M is used for structuring the outputs and the comonad N forCategorical semantics for arrows

7

the inputs. But arrows are more general than this. For instance, if we wish to do“non-deterministic dataflow” we may consider at first maps of the form
X N × N −→ P(Y ),(13)with the comonad on the left-hand side structuring the input of streams, and themonad on the right-hand-side producing non-deterministic output. However, thisrequires a distributive law of the form
P(X)N × N −→ P(X N × N).
While it is possible to construct such a function – for instance the power law
from (Jacobs, 2006) – it does not commute with the comonad structure. As aresult, composition is not associative.
The way out is to realise that co-Kleisli maps X N × N → Y correspond to maps
N
X → Y N via Currying. But then non-determinism can be introduced easily into
dataflow, namely by looking at maps
X N −→ P(Y N )(14)N

instead of maps (13). The corresponding assignment (X, Y ) 7→ P(Y N )(X ) indeed forms an arrow – with associative composition. It is however not of the form
(X, Y ) 7→ M (Y )N (X) . Arrows thus have more to offer than monad-comonad combinations. As an aside: it is not so clear how to combine the other comonads in (11)with non-determinism.

3 Arrow constructions and examples
This section continues in the discursive style of the previous one. It introduces
several elementary ways to combine arrows, and use these constructions to obtainsome well-known examples. The first construction is obvious, but useful. Its proof
is straightforward and left to the reader.
Lemma 3.1
Let (A1 , arr1 , >>>1 ) and (A2 , arr2 , >>>2 ) be arrows. Then so is their product A =A1 × A2 , described by
A(X, Y ) = A1 (X, Y ) × A2 (X, Y )with operations
arr(f ) = harr1 (f ), arr2 (f )i
ha1 , a2 i >>> hb1 , b2 i = ha1 >>>1 b1 , a2 >>>2 b2 if irst(ha, bi) = hf irst1 (a), f irst2 (b)i.
The next result now follows from the observation in the previous section thateach monoid forms a (constant) arrow. The result is mentioned explicitly because
it will be used later in this form, in Example 3.1.
Corollary 3.1

8Jacobs, Heunen, Hasuo

Let (A, arr, >>>) be an arrow, and (P, m, e) be a monoid. Then A0 = P × A, givenby
A0 (X, Y ) = P × A (X, Y ) = P × A(X, Y ) ,is again an arrow, with the following operations.
arr0 (f ) = he, arr(f )ihx, ai >>>0 hy, bi = hm(x, y), a >>> bi
f irst0 (hx, ai) = hx, f irst(a)i.
For the next result we consider functors F that preserve products. This meansthat the obvious maps
F (X × Y )hF (π1 ),F (π2 )i/ F (X) × F (Y )are isomorphisms. In that case we shall write β = βX,Y : F (X)×F (Y ) → F (X ×Y )for the inverse.
Lemma 3.2
Let (A, arr, >>>) be an arrow, and F be a product preserving functor. Defining
AF (X, Y ) = A(F (X), F (Y )),yields a new arrow AF with the following operations.
arr0 (f ) = arr(F (f ))a >>>0 b = a >>> b
f irst0 (a) = arr(hF (π1 ), F (π2 )i) >>> f irst(a) >>> arr(β).
ProofChecking the relevant equations is not hard. For instance:f irst0 (a >>> b)= arr(hF (π1 ), F (π2 )i) >>> f irst(a >>> b) >>> arr(β)
(9)

=

(4)

=

(3)

=

=

arr(hF (π1 ), F (π2 )i) >>> f irst(a) >>> f irst(b) >>> arr(β)
arr(hF (π1 ), F (π2 )i) >>> f irst(a) >>> arr(hF (π1 ), F (π2 )i ◦ β)>>>f irst(b) >>> arr(β)
arr(hF (π1 ), F (π2 )i) >>> f irst(a) >>> arr(β)>>>arr(hF (π1 ), F (π2 )i) >>> f irst(b) >>> arr(β)
f irst0 (a) >>>0 f irst0 (b).

Lemma 3.3
Let (A, arr, >>>) be an arrow and S an arbitrary type. The definition
AS× (X, Y ) = A(S × X, S × Y )again yields an arrow, with corresponding structure:arrS× (f ) = arr(idS × f )a >>>S× b = a >>> b
f irstS× (a) = arr(α−1 ) >>> f irst(a) >>> arr(α)

Categorical semantics for arrows

9

where α is the associativity isomorphism for products from Subsection 2.1.
This particular construction AS× occurs, in a slightly different formulation, already in (Hughes, 2000, §§9) where it is introduced via a ‘state functor’. A similar
construction (X, Y ) 7→ A(X, S)A(Y,S) is defined there for special arrows with suitable apply operations A(A(X, Y ) × X, Y ).
At this stage we can already see how one of the motivating examples for thenotion of arrow can be obtained from the previous constructions.
Example 3.1
In (Hughes, 2000, §§4.2) an arrow SD is introduced to describe a special parser
defined by (Swierstra & Duponcheel, 1996). This arrow can be described as
(S ? ×X)
SD(X, Y ) = (2 × S ? ) × 1 + S ? × Y.
(15)
We show that this arrow SD can be obtained by successive application of theconstructions in this section.
First, the set 2 × S ? – with 2 = {0, 1} – is used as monoid, not with the standard
structure, but with unit and composition given by:e = (1, hi)m((b, σ), (c, τ )) = (b ∧ c, σ · (if b = 1 then τ else hi)).
It is not hard to see that this yields a monoid. Corollary 3.1 then tells that (15)
(S ? ×X)
is an arrow if the rightmost part (X, Y ) 7→ 1 + S ? × Y
is. Using the liftmonad 1 + (−) we get an arrow (X, Y ) 7→ (1 + Y )X , as shown in subsection 2.3. By
applying Corollary 3.3 with set S ? we obtain the rightmost part, as required.
When we go into the details of these constructions we can also reconstruct theassociated operations of the arrow (15) as follows.
arr(f )= h (1, hi), λ(s, x) ∈ S ? × X . up(s, f (x)) ih(b, σ), f )i >>> h(c, τ ), gi= h (b ∧ c, σ · (if b = 1 then τ else hi)),⊥
if f (s, x) = ⊥λ(s, x) ∈ S ? × X .
g(t, y) if f (s, x) = up(t, y) i
f irst(h(b, σ), f i)
= h (b, σ),⊥
if f (s, x) = ⊥λ(s, (x, y)) ∈ S ? × (X × Y ) .
up(t, (z, y)) if f (s, x) = up(t, z) i.
These operations are precisely as described (in Haskell notation) in (Hughes, 2000,§§4.2).
Example 3.2
Quantum computing (Vizzotto et al., 2006+) can be modelled within a functional
programming language. The states of a quantum program are so-called density
matrices, that we can understand as elements of the monad application D(X)X to
some set X. These states evolve into each other by superoperators, which can be10Jacobs, Heunen, Hasuo

modelled as arrows (X, Y ) 7→ D(Y × Y )(X×X) . The previous lemmas also enable us
to show that this quantum computation arrow is indeed an arrow, by decomposing
it into elementary parts, without checking the arrow laws by hand.
First, recall that the mapping (X, Y ) 7→ D(Y )X yields an arrow, induced by the
distribution monad D. Next, notice that the diagonal functor X 7→ X ×X preserves
products, so that the mapping (X, Y ) 7→ (Y × Y )(X×X) yields an arrow, withf irst(a) = λ((x, z), (x0 , z 0 )) ∈ (X × Z) × (X × Z) . ((π1 a(x, x0 ), z), (π2 a(x, x0 ), z 0 ))for given a : X × X → Y × Y ,Thus, according to Lemma 3.2, the mapping (X, Y ) 7→ D(Y × Y )(X×X) is anarrow. If we follow through the construction, we obtain the following arrow operations.
arr(f )=rt ◦ (f × f )= λ(x, x0 ) . λ(y, y 0 ) .
a >>> b

1 if f (x) = y ∧ f (x0 ) = y 00 otherwise= bd(b) ◦ aX= λ(x, x0 ) . λ(z, z 0 ) .
a(x, x0 )(y, y 0 ) · b(y, y 0 )(z, z 0 )(y,y 0 )f irst(a)= D(hπ1 × π1 , π2 × π2 i) ◦ st ◦ (a × id) ◦ hπ1 × π1 , π2 × π2 i00
 a(x, x )(y, y ) if z1 = z20 0
0 0= λ((x, z1 ), (x , z1 )) . λ((y, z2 ), (y , z2 )) .
and z10 = z20 ,0otherwise.

These indeed coincide exactly with the ones given in (Vizzotto et al., 2006+).
4 Categorical formulation
In this section we shall move towards a categorical formulation of the notion ofarrow. We shall do so by first analysing the structure in a Haskell-like setting. We
denote by HT the category with Haskell types as objects. A morphism σ → τ inthis category is a Haskell function f = λx : σ . f (x) : τ taking input in σ to output
in τ . Composition of such maps is performed by substitution. Essentially, this is a
Cartesian closed category of types and terms, but for the fact that some functions do
not terminate, much like a lambda calculus. Of course there is much more structure(like general recursion) in Haskell than the types with type variables and terms, likein system F. Below we shall analyse the behaviour of Haskell arrows as bifunctors
on HT, leading to a more general definition of an arrow over any category C.
4.1 Analysing arrow behaviour categoricallyFirst and foremost, let us show that a Haskell arrow is indeed bifunctorial.
Lemma 4.1
The operation A(−, −) extends to a functor HTop × HT → Set by(X, Y ) 7→ {a : A(X, Y ) | a closed term},Categorical semantics for arrows

11

whose action A(f, g) : A(X, Y ) → A(X 0 , Y 0 ) on maps f : X 0 → X and g : Y → Y 0
is given by
A(f, g) = λa . arr(f ) >>> a >>> arr(g).
ProofUsing equations (2), (3) and (4) one easily derives the functorial properties for
identity, A(id, id) = id, and composition, A(f ◦ f 0 , g 0 ◦ g) = A(f 0 , g 0 ) ◦ A(f, g).
We now examine the arrow operations arr and f irst in the light of the bifunctoriality of A.
Lemma 4.2
The maps arr : HT(X, Y ) → A(X, Y ) form a natural transformation HT(−, +) ⇒A(−, +) from exponents to arrows, where HT(−, +) is the homset functor.
Similarly, the maps f irst : A(X, Y ) → A(X × Z, Y × Z) are natural in X and Y .
This may be formulated as: f irst yields a natural transformation hf irsti from A
Q
to the functor A× given by (X, Y ) 7→ Z A(X × Z, Y × Z). Of course, this functor
A× only makes sense in a small category with arbitrary (set-indexed) products Π.
ProofFor maps f : X 0 → X, g : Y → Y 0 in HT and h : HT(X, Y ) we haveA(f, g) ◦ arr (h) = arr(f ) >>> arr(h) >>> arr(g)(3)= arr(g ◦ h ◦ f ) = arr(g f (h)) = arr ◦ g f (h),andA× (f, g) ◦ hf irsti)(a) = hA(f × id, g × id) ◦ πZ iZ (hf irst(a)i)= hA(f × id, g × id)(f irst(a))i= harr(f × id) >>> f irst(a) >>> arr(g × id)i(8)

= hf irst(arr(f )) >>> f irst(a) >>> f irst(arr(g))i(9)= hf irst(arr(f ) >>> a >>> arr(g))i= hf irst(A(f, g)(a))i= hf irsti ◦ A(f, g) (a).
The next lemma shows that the maps >>> : A(X, P ) × A(P, Y ) → A(X, Y ) arenatural in X and Y , just like the maps arr and f irst in the previous lemma. In
the parameter P they are what is called dinatural (Mac Lane, 1971, Section IX.4).
This means that for each map f : P → Q the following diagram commutes.
A(X, P ) × A(P, Y )id×A(f,id)
hhh3
h
h
h
h
hhhh
A(X, P ) × A(Q, Y )
VVVV
VVVV
VV
A(id,f )×id V+
A(X, Q) × A(Q, Y )/ A(X, Y )
PPP
PPP
P
A(X, Y )
n
n
n
n
nnn
/ A(X, Y )
>>>

>>>

12

Jacobs, Heunen, Hasuo

Lemma 4.3
The maps >>> : A(X, P ) × A(P, Y ) → A(X, Y ) are natural in X and Y , anddinatural in P .
ProofNaturality is trivial. As for dinaturality, for a : A(X, P ) and b : A(Q, Y ), we have>>> ◦ (id × A(f, id)) (a, b) = a >>> A(f, id)(b)= a >>> arr(f ) >>> b= A(id, f )(a) >>> b

= >>> ◦ (A(id, f ) × id) (a, b).
Intuitively, dinaturality in P signifies that >>> is parametric in its middle argument type, and that this middle parameter is auxiliary; it could just have well been
another one, as long as it is the same across the second argument of the first factor,
and the first argument of the second.

4.2 Monoidal structure in the ambient category
Extending from the category HT of (Haskell) types and terms, we would like todefine an arrow over any suitable category C as a monoid in the functor category Cat(Cop × C, Set) of bifunctors that carries an internal strength. However,to do so we need to ensure that the ambient category, Cat(Cop × C, Set), hasmonoidal structure. The most elegant way to achieve this is to employ the notion of (parametrized) coends, see Appendix A. This approach generalises to theV-enriched situation, when an arrow is a suitable bifunctor Cop × C → V. Suchenrichment is necessary if we are to consider (instead of HT) a categorical modelof Haskell which is most probably Cpo-enriched. At this stage we shall present theconstruction for the reasonably concrete case where V = Set, mostly to give some
intuition about the monoidal structure.
Proposition 4.1
Let C be a small category. Then the category Cat(Cop × C, Set) of Set-valued
bifunctors has a monoidal structure with unit I and tensor product ⊗.
Proof
The naturality of HT(−, +) ⇒ A(−, +) observed in Lemma 4.2 suggests that the(internal) homfunctor could serve as the unit of the intended monoidal structure
on Cat(Cop × C, Set). Thus we define I : Cop × C → Set to be HomC ; explicitly,
I(X, Y ) = C(X, Y ) and I(f, g) = g f = λh . g ◦ h ◦ f . This requires C to be locallysmall.
The main idea now is to let the monoidal product of two bifunctors A, B : Cop ×
C → Set be the smallest type containing all bifunctors that behave dinaturally inthe middle parameter. More explicitly, composition >>> is a collection of morphisms
A(X, P ) × A(P, Y )>>>/ A(X, Y ),

Categorical semantics for arrows

13

which can be combined, using the (arbitrary set-indexed) coproduct in Set, into
one natural transformation with the following component at X, Y ∈ C.
`

 >>>

P ∈C A(X, P ) × A(P, Y )/ A(X, Y )This requires C to have a (small) set of objects. We take the dinaturality of Lemma
4.3 into account by defining the components of the monoidal product A ⊗ B as thecoequalizer c!
A(X, P )d1
a/ a A(X, P )_ _c _/ (A ⊗ B)(X, Y )
×C(P, Q)/×B(P, Y )d2
P ∈C
×B(P, Y )P,Q∈Cof (obvious cotuples of) the morphisms (in Set)
d1 = λ(a, f ) . A(id, f )(a) : A(X, P ) × C(P, Q) → A(X, Q),
d2 = λ(f, b) . B(f, id)(b) : C(P, Q) × B(Q, Y ) → B(P, Y ),for all P, Q ∈ C. The composition maps >>> then reappear as the components of
the unique A ⊗ A ⇒ A from the coequalizer.
RemarkThe situation sketched in the previous proposition and proof is that of profunctors,
which are also known as distributors or bimodules (Bénabou, 2000). Profunctors
and natural transformations form a bicategory Prof , which is a well-studied generalisation of the category of sets and relations. The monoidal structure of Prof (asdescribed above) is well-known. The basic idea is that composition of profunctors,
and hence the tensor product in the above proposition, can also be written in termsof standard functor composition using left Kan extension along the Yoneda embedding. See (Day, 1970) for the original account, or (Borceux, 1994, Section 7.8) fora modern record.
The previous lemma puts us in a position to make precise our intuition thatarrow laws (2)–(4) resemble monoid equations.
Proposition 4.2>>>
arr
An instantiation of the Haskell arrow class (A ⊗ A) −→ A ←− I satisfying (2)–(4) isa monoid in the category Cat(HTop × HT, Set) of bifunctors HTop × HT → Set.
Proof
>>>
arr
We have to check that the monoid equations hold for the span (A ⊗ A) −→ A ←− I.
Here we exhibit one of the equations, namely
ρ−1

/ A⊗A
A VVVVV / A ⊗ I
VVVV VV VVV>>>
VVVV 
V
A,
id⊗arr14

Jacobs, Heunen, Hasuo

which for a : A(X, Y ) becomes/ (a, id) a/ (a, arr(id))_
a >>> arr(id).

Hence commutation of this diagram amounts to arrow law (4), which states thata >>> arr(id) = a.
RemarkAlthough the proof of Proposition 4.1 requires a restriction to small categories, wewill often relax this to locally small categories. We are only after A⊗A anyway, andindeed, in the construction of A ⊗ A above we used a large coproduct for clarity,
where we could have formulated the composition operation >>> of A via collectionsof maps A(X, P ) × A(P, Y ) → A(X, Y ) that are natural in X, Y , dinatural in P
and satisfy the arrow equations (2)–(9).
In this way one could include domain theoretic models that are standardly usedfor Haskell semantics.
4.3 Internal strength
Now that we have seen that arrow laws (2)–(4) correspond to the monoid equations
on the semantical side, we investigate the remaining laws (5)–(9) concerning f irst
in more detail.
Recall that a monad T : C → C on a monoidal category C is called strong when
there is a natural transformation “strength” with components stX,Y : T (X) ⊗ Y →T (X ⊗ Y ) that satisfies suitable coherence conditions. This section shows that theavailability of the function f irst is equivalent to an analogous form of strength forbifunctors, that we call internal strength. Its emergence is motivated in Appendix B.
Definition 4.1
Let C be a category with finite products. The carrier A : Cop × C → Set of a
monoid (A, >>>, arr) in Cat(Cop × C, Set) is said to carry an internal strength
natural transformation with components istX,Y : A(X, Y ) → A(X, Y × X) if thesesatisfyist(arr(f )) = arr(hf, idi),
ist(a) >>> arr(π1 ) = a,

(16)
(17)

ist(a >>> b) = ist(a) >>> ist(arr(π1 ) >>> b) >>> arr(id × π2 ),(18)

ist(ist(a)) = ist(a) >>> arr(hid, π2 i).

(19)

Using the techniques of Appendix A this can again be extended to bifunctors
A : Cop × C → V for a category C with finite products and a suitable category V.
The following proposition shows that having internal strength is in fact equivalent
to having a f irst operation for arrows – as originally introduced by Hughes.
Proposition 4.3

Categorical semantics for arrows15

Let (A, >>>, arr) be an instantiation of the Haskell arrow class satisfying (2)-(4).
The maps f irst : A(X, Y ) → A(X × Z, Y × Z) satisfying equations (5)–(9) correspond to maps ist : A(X, Y ) → A(X, Y × X) which are natural in Y and dinaturalin X, and satisfy (16)–(19).
Proof
The proof of the equivalence of f irst and ist involves many basic calculations, ofwhich we only present a few exemplaric cases.
Given maps f irst satisfying (5)–(9), define internal strength on a : A(X, Y ) as
ist(a) = arr(∆) >>> f irst(a),where ∆ = hid, idi. One then checks naturality in Y , dinaturality in X, and (16)–(19). The (di)naturality equations can be formulated as:
ist(a) >>> arr(g × id) = ist(a >>> arr(g))
arr(f ) >>> ist(a) = ist(arr(f ) >>> a) >>> arr(id × f ).

(20)
(21)

By way of illustration we check equation (17):ist(a) >>> arr(π1 ) = arr(∆) >>> f irst(a) >>> arr(π1 )(5)= arr(∆) >>> arr(π1 ) >>> a(3)= arr(π1 ◦ ∆) >>> a= arr(id) >>> a
(4)

= a.

Conversely, given internal strength maps ist satisfying (16)–(19), define:f irst(a) = ist(arr(π1 ) >>> a) >>> arr(id × π2 ),where π1 : X × Z → X and id × π2 : Y × (X × Z) → Y × Z. This yields a naturaloperation, in the sense that:arr(f × id) >>> f irst(a) >>> arr(g × id) = f irst(f >>> a >>> g).
We shall prove equation (9) in detail, and leave the rest to the interested reader.
f irst(a) >>> f irst(b)=ist(arr(π1 ) >>> a) >>> arr(id × π2 ) >>> ist(arr(π1 ) >>> b)>>>arr(id × π2 )(dinat)

=

(3)

=

(18)

=
=

ist(arr(π1 ) >>> a) >>> ist(arr(id × π2 ) >>> arr(π1 ) >>> b)>>>arr(id × (id × π2 )) >>> arr(id × π2 )ist(arr(π1 ) >>> a) >>> ist(arr(π1 ) >>> b)>>>arr(id × π2 ) >>> arr(id × π2 )ist(arr(π1 ) >>> a >>> b) >>> arr(id × π2 )f irst (a >>> b).

The alternative formulation in terms of internal strength ist in the previous16

Jacobs, Heunen, Hasuo

Proposition is convenient because its (di)naturality is clearly described, and it has
only two parameters, whereas f irst has three.

4.4 The categorical definition
After the preparations of section 4.2 we know that an arrow A satisfying arrowlaws (2)–(4) is precisely a monoid in the category of bifunctors HTop × HT → Set.
Furthermore, section 4.3 showed that arrow laws (5)–(9) correspond precisely tothis monoid having internal strength. Since both notions have been defined moregenerally than just for the Haskell category HT, we can now lift these properties
into our main definition.
Definition 4.2
Let C be a small category with finite products. An arrow over C is a monoid in
Cat(Cop × C, Set) whose carrier has an internal strength.
In Appendix A we extend the definition of arrow to bifunctors Cop × C → V,
where C is V-enriched and both categories satisfy suitable size restrictions.
The combination of Propositions 4.2 and 4.3 justifies this categorical definitionby showing that in the small category HT of Haskell types and functions ourcategorical notion of arrows coincides with the conventional one. Let us record thisformally.
Corollary 4.1
An instantiation (A, >>>, arr, f irst) of the Haskell arrow class is an arrow over HT
in the sense of Definition 4.2.
Summarising, we have shown that arrows in a type theoretic setting coincide withmonoids in the category of bifunctors HTop × HT → Set with internal strength.
We then lifted this property to a definition of arrow on any suitable category ofbifunctors Cop × C → V, of which we described the case V = Set explicitly.

5 Biarrows
The aim of this section is to illustrate that our categorical semantics for Haskell
arrows is at the right level of abstraction. We consider the example of so-called biarrows, the semantics of which can now be elegantly expressed by simply restricting
the underlying category.
Biarrows were introduced in (Alimarine et al., 2005) as a language extension
facilitating bidirectional computations. For example, implementing a parser as abiarrow begets a pretty-printer “for free”. In Haskell terms, a biarrow is a further
restriction of the arrow class interface:class

Arrow B(↔)
inv=> BiArrow B where:: (X → Y ) → (Y → X) → B X Y:: B X Y → B Y X

Categorical semantics for arrows

17

satisfying (2), (5), (7), (9), and(f1 ↔ g2 ) >>> (g1 ↔ f2 ) = (f1 >>> g1 ) ↔ (f2 >>> g2 ),(3’)(id ↔ id) >>> f = f = f >>> (id ↔ id)(4’)

f irst(h) >>> (id × f ) ↔ (id × g) = (id × f ) ↔ (id × g) >>> f irst(h)(6’)

f irst(f ↔ g) = (f × id) ↔ (g × id)(8’)

inv(inv(f )) = f(22)

inv(f >>> g) = inv(g) >>> inv(f )(23)

inv(f ↔ g) = g ↔ f(24)

inv(f irst(f )) = f irst(inv(f ))(25)

We see that biarrows require a further operation inv on top of arr, >>> and f irst,
whose type should be inv : B(X, Y ) → B(Y, X). Since we defined an arrow as a bifunctor of the form B : Cop ×C → V, a natural transformation B(X, Y ) → B(Y, X)
is a problem because of the co- versus contravariance. The following definition enforces the required symmetry C = Cop .
Definition 5.1
For C a category, define a full subcategory C of Cop × C by the class of objects{(X, X) : X ∈ C}. We identify the objects of C and C, so that a morphism
X → Y in C is a pairs of morphisms X → Y and Y → X of C.
The category C is self-dual by construction. It has finite products if and only if
C has finite biproducts – which, for this situation, are finite products and coproducts that coincide.
Definition 5.2
A biarrow on C is defined to be an arrow B on C that is equipped with anatural transformation inv : B ⇒ B ∗ where B ∗ : Cop
 × C → Set is given byB ∗ (X, Y ) = B(Y, X) and h(g, f ), (h, k)i 7→ h(f, g), (k, h)i. The components invX,Y :B(X, Y ) → B(Y, X) are required to satisfy:
inv ◦ inv = id
inv ◦ >>> ◦ γ = >>> ◦ (inv × inv)

(26)
(27)

inv ◦ arr = arr ◦ γ(28)

inv ◦ f irst = f irst ◦ inv(29)

A biarrow B is called left-invertible on b ∈ B(X, Y ) if b >>> inv(b) = idX . It iscalled right-invertible on b if inv(b) >>> b = idY , and invertible if it is both left- andright-invertible.
Notice that the domain of the operation arr : C (X, Y ) → B(X, Y ) of a biarrow
B is C(X, Y ) × C(Y, X). Hence one can model the operation (↔) simply by theunit arr of the monoidal structure of a biarrow.
Let us conclude this section by studying under which conditions the examples ofSection 2.3 are (invertible) biarrows.

18

Jacobs, Heunen, Hasuo

Proposition 5.1
The arrow Cop
 × C → Set of pure functions, given by B(X, Y ) = C(X, Y ) ×
C(Y, X), is a biarrow. On morphisms it is given by:


X0 o

f
g

/ X, Y oh/ Y0 / λ(a, b) ∈ B(X, Y ) . (h ◦ a ◦ g, f ◦ b ◦ k)k

It is left-invertible on (the subcategories of C of) split monics, right-invertibleon split epis, and invertible on isomorphisms.
Proof
Use the “swap” map (a, b) 7→ (b, a) as the natural transformation inv. Since thisis in fact a natural isomorphism, (26)–(29) are trivially satisfied. Left-invertibility
on a morphism b ∈ B(X, Y ) means precisely that its components b1 : X → Y andb2 : Y → X satisfy b2 ◦ b1 = idX , proving the claim that b1 be split mono. The
claim on split epis is similar, and a morphism that is split mono as well as split epi
is necessarily an isomorphism.
In the style of Section 3, one may proceed to formulate a calculus of biarrows. In
this way one may structurally develop programs together with their “inverses”, asin (Alimarine et al., 2005).
6 Kleisli and Eilenberg-Moore constructions for arrows
In Section 4 we have observed that arrows are monoids in a category of bifunctors
Cop ×C → V, where C is V-enriched. This perspective bears a resemblance to monads. After all, monads are also monoids in a functor category, namely Cat(C, C).
Pursuing this analogy, this section investigates Eilenberg-Moore and Kleisli constructions for arrows.
We should warn the reader that this section requires a stronger stomach fortechnical/categorical details. For clarity of exposition, we focus on a non-enrichedsetting throughout this section, i.e. V = Set. Enriching the whole framework in a
monoidal closed category V (following Appendix A) is then straightforward. Concretely, this means that the results in this section will be needlessly restricted to
locally small categories.
6.1 Arrows are Freyd categories
Let us start by exhibiting an obvious way to associate a category of “(structured)computations” with an arrow. This construction will subsequently be shown to• give Freyd categories (Robinson & Power, 1997; Power & Thielecke, 1997);• provide a bijective correspondence between arrows and Freyd categories, adhering to the slogan “arrows are Freyd categories” (Heunen & Jacobs, 2006);• be the Kleisli construction for arrows, in a suitable 2-categorical sense, underthe motto “Freyd is Kleisli, for arrows” (Jacobs & Hasuo, 2006).
Definition 6.1 (The category CA )

Categorical semantics for arrows

19

Let A : Cop × C → Set be an arrow, with operations arr, >>> and f irst. Define acategory CA to have objects those of C, and morphisms X → Y given by elementsof the set A(X, Y ). Identities and composition are given by arr and >>> in theobvious manner.
Before proceeding to explain why this construction gives Freyd categories in
Theorem 6.1 below, let us briefly summarize what a Freyd category is. For that,
we need the notion of a premonoidal category, which can intuitively be thought ofas a monoidal category in which the tensor need not be a bifunctor, though it isfunctorial in each variable separately.
Definition 6.2
A binoidal category is a category D, with for every object X two functors (−) n X :D → D and X o (−) : D → D such that X n Y = X o Y . Hence we write
X  Y = X n Y = X o Y . A morphism f is called central if for each g, both
• (f n id) ◦ (id o g) = (id o g) ◦ (f n id), and• (id o f ) ◦ (g n id) = (g n id) ◦ (id o f ).
For such a central f it makes sense to write f  g or g  f for these composites.
Definition 6.3
A symmetric premonoidal category is a binoidal category D together with an object
I ∈ D and natural isomorphisms with central components α : (X  Y )  Z →X  (Y  Z), λ : I  X → X, ρ : X  I → X and γ : X  Y → Y  X that obey
the familiar coherence properties for monoidal categories.
The non-bifunctoriality reflects the order of side-effects when we think of D as acategory of ‘computations’. When we include a category C of ‘values’, we arrive at
the notion of a Freyd category (Robinson & Power, 1997; Power & Thielecke, 1997;
Levy et al., 2003).
Definition 6.4
A Freyd category consists of a symmetric premonoidal category D together witha category C with finite products, and an identity-on-objects functor J : C → D
which:2• carries Cartesian products in C to premonoidal products in D on-the-nose:J(X × Y ) = X  Y , J(α) = α, J(λ) = λ, etc.;• preserves central maps. Since every morphism in C is central, this just meansthat every morphism in D of the form J(g) is central.
A Freyd category C → D is called (locally) small if the category D is (locally)small.
2 Such a functor J satisfying the two conditions is called a strict premonoidal functor in Definition

8, (Power & Thielecke, 1997). In that paper the notion of Freyd category has not yet been given
its name; still it is a central notion there and appears e.g. in Theorem 14.

20

Jacobs, Heunen, Hasuo

Returning to the central construction of this section, the category CA of Definition 6.1, observe that there is an identity-on-objects functor JA : C → CA whose
action on morphisms is given by arr. This forms an instance of a Freyd category,JA
as Theorem 6.1 will prove. We shall call this mapping A 7→ (C →CA ) from arrows
to Freyd categories the Kleisli construction for arrows. Although this name will
be fully justified (2-categorically) in Section 6.3, we can observe now already somesimilarities to the Kleisli construction for monads. For an arrow A induced by a(co)monad, the associated Freyd category CA coincides with the (co)Kleisli category for the (co)monad in the usual sense. For the arrow (N, M ) of (12), induced byboth a monad M and a comonad N , the Kleisli construction yields what is called
the bi-Kleisli category used e.g. in (Uustalu & Vene, 2005).
J

A
The Kleisli construction A 7→ (C →CA ) turns out to be a bijective map from arrows to Freyd categories. This observation turns the oft-heard (informal) statement“arrows are Freyd categories”, into the following concrete theorem.

Theorem 6.1 (“Arrows are Freyd categories”)
For a locally small category C with finite products, there is a one-to-one correspondence between arrows A over C (in the sense of Definition 4.2) and locally small
Freyd categories C → D.
Proof
Suppose we are given an arrow A : Cop × C → Set with operations >>>, arr, andist. Putting D = CA entails that D is symmetric premonoidal by I = 1 ∈ D andX Y = X ×Y . The premonoidal tensor  extends to a functor (on morphisms) byvirtue of the provided ist (or equivalently f irst, see Proposition 4.3, and second),since every morphism a ∈ A(X, Y ) yields a  Z = f irstZ (a) : X  Z → Y  Z andZ  a = secondZ (a) : Z  X → Z  Y . The transformation of an arrow into a Freyd
category is completed by defining J : C → D to act as the identity on objects, andas arr on morphisms.
Conversely, suppose given a Freyd category J : C → D. Define A : Cop ×C → Set
by A(X, Y ) = D(X, Y ). This A is made into a monoid in Cat(Cop × C, Set) by theunit arr = J : C(X, Y ) → D(X, Y ), and for multiplication >>> the composition
A(X, P ) × A(P, Y ) → A(X, Y ) in D. Furthermore we can define internal strength
istX,Y : A(X, Y ) → A(X, Y × X)

by istX,Y (f ) = (f n X) ◦ J(hid, idi).

Naturality of ist in Y is obvious, dinaturality in X boils down to the fact that the
diagram
D(X, Y )8(−)◦J(g)ppp
p
p
p
ppp
0
D(X , Y )
NNN
NNNN
NN
D(X 0 , Y )istX,Y

istX 0 ,Y/ D(X, Y  X)
RRR(Y J(g))◦(−)
RRR
RRR
RR)
D(X, Y  X 0 )
ll5
lll
l
l
l
lll (−)◦J(g)/ D(X 0 , Y  X 0 )commutes for every morphism g : X → X 0 in C. The crux here is that it needCategorical semantics for arrows

21

only commute for morphisms g of C, i.e. morphisms of D of the form J(g) (cf.
equations (20) and (21)), which are central. Since one also readily checks (16)–(19),this proves that a Freyd category induces an arrow.
The proof of the previous theorem reminds one strongly of the situation formonads. In the well-known correspondence between• monoids in the category of functors C → C,
• monads M on C, and• identity-on-objects functors J : C → D that have a right adjoint,
the functor J arises from M by the Kleisli construction, while J induces a monad
M by the adjunction. The proof of the above theorem is a generalisation of thiscorrespondence (Heunen & Jacobs, 2006).

6.2 Eilenberg-Moore algebras for arrows
After considering Kleisli constructions for arrows in the previous subsection, we
now turn to the notion of Eilenberg-Moore algebras for arrows. We aim for two
properties of this new notion. First, for arrows induced by (co)monads it should
coincide with the usual notion of (co)algebra. Secondly, an arrow-algebra should bea retraction of a Kleisli category, much like for monads.
Let us start by the situation for monads. We shall understand (Eilenberg-Moore)(co)algebras in 2-categorical style as natural transformations. Explicitly, an algebra
for a monad (T, η, µ) on a category C is a map ϕ : T ⇒ idC satisfying the familiar
equations ϕ ◦ η = id and ϕ ◦ T ϕ = ϕ ◦ µ. Since such a monad T is the same thing as
a monoid in Cat(C, C), with monoidal structure given by functor composition andthe identity functor, these monad equations boil down to the following commuting
diagram.
/T o
idC LLLLLLL
LLLL ϕ
LLLL
L 
idC
η

µ

T ⊗ T = T2
ϕ⊗ϕ=ϕ◦T ϕ
idC ⊗ idC

When T is strong we might as well require coherence with its strength.
/ T ((·) × (∗))
T (·) × (∗)
PPP
PPP
ϕ
PP
ϕ×id PP'(·) × (∗)
ϕ(30)

The fact that an arrow is also a monoid – in a category of bifunctors – leads tothe following definition.
Definition 6.5
Let A : Cop × C → Set be an arrow. An algebra for A is a natural transformation
χ : A ⇒ Hom that is compatible with arr, >>> and hf irsti, in the sense that the22

Jacobs, Heunen, Hasuo

following diagrams commute for each Z ∈ C.
>>>
arr /
A⊗A
HomDD
Ao
DDDDD
DDDD χ
χ⊗χ
DDD
Hom ⊗ HomHom o ∼=

A

hf irsti

χ

/ A×
χ



Hom h(−)×Zi / Hom× ,

(31)

Z

where we used the functor A× from Lemma 4.2 and the analogous Hom× (X, Y ) =Hom(X × Z, Y × Z).

An algebra of an arrow is thus a (natural) mapping of computations to (pure)functions. One might have expected a single mapping χ : A(X, Y ) → Hom(X, Y ),but then it is unclear how to capture commutation with composition >>>. Specifically, defining χ ⊗ χ in (31) is problematic.
In elementary terms, an algebra χ must thus satisfy the equations
χ(arr(f )) = f,

χ(a >>> b) = χ(b) ◦ χ(a),χ(f irst(a)) = χ(a) × id.

Naturality then is a consequence:χ(A(f, g)(a)) = χ(arr(f ) >>> a >>> arr(g))= χ(arr(g)) ◦ χ(a) ◦ χ(arr(f ))= g ◦ χ(a) ◦ f= Hom(f, g)(χ(a)).
The rest of this subsection is devoted to results stemming from Definition 6.5.
The first one concerns arrows M induced by monads M as in (10). This subsection
contains two similar results. We write out the proof of this first one in full detail,to distinguish the trivial parts from the non-trivial ones. Especially the order inwhich to apply the equations in the verification of the multiplication law in the
proof below is delicate.

Proposition 6.1
For a strong monad M there is a bijective correspondence between strong-monadalgebras M ⇒ id and arrow-algebras M ⇒ Hom.

Proof
Given a monad algebra ϕ : M ⇒ id, define ϕ : M ⇒ Hom on a ∈ Hom(X, M Y )by ϕ(X,Y ) (a) = ϕY ◦ a. We check that it satisfies the required properties, omitting

Categorical semantics for arrows

23

subscripts for clarity.
ϕ(arr(f )) = ϕ ◦ η ◦ f

ϕ(f irstZ (a)) = ϕ ◦ st ◦ (a × Z)
= (ϕ × Z) ◦ (a × Z)

= f,
ϕ(a >>> b) = ϕ ◦ µ ◦ M (b) ◦ a= (ϕ ◦ a) × Z)

= ϕ ◦ M (ϕ ◦ b) ◦ a= ϕ(a) × Z,

= (ϕ ◦ b) ◦ (ϕ ◦ a)ϕ(M (f, g)(a)) = ϕ(M (g) ◦ a ◦ f )= ϕ(b) ◦ ϕ(a),= ϕ ◦ M (g) ◦ a ◦ f=g◦ϕ◦a◦f= Hom(f, g)(ϕ ◦ a)
= Hom(f, g)(ϕ(a)).

Conversely, given an arrow-algebra χ : M ⇒ Hom we define χX : M X → X
as χ(M X,X) (idM X ). This definition suggests that the Yoneda Lemma can also be
used. For clarity, we have chosen to write out the proof that we get an M -algebra
directly. The unit-law and naturality are easy:χ ◦ η = χ(id) ◦ χ(arr(η))χ ◦ M (f ) = χ(id) ◦ χ(arr(M (f )))= χ(arr(η) >>> id)= χ(arr(M (f )) >>> id)= χ(µ ◦ M (id) ◦ η ◦ η)= χ(µ ◦ M (id) ◦ η ◦ M (f ))= χ(η)= χ(M (f ))= χ(arr(id))= χ(µ ◦ M (η ◦ f ) ◦ id)= id,= χ(id >>> arr(f ))= χ(arr(f )) ◦ χ(id)= f ◦ χ.

Compatibility (30) with strength is proved as follows.
(∗)

χ × Y = χ(id) × Y = χ(st ◦ (id × id)) = χ(st ◦ id)(∗∗)= χ(id ◦ st) = χ(id) ◦ st = χ ◦ st.
The equality (∗) holds because χ is compatible with f irst, given by f irst(a) =st ◦ (a × id); (∗∗) uses the naturality of χ.
Verification of the multiplication law is more subtle.
χ ◦ M (χ) = χ(id) ◦ χ(arr(M (χ))) = χ(arr(M (χ)) >>> id)= χ(µ ◦ M (id) ◦ η ◦ M (χ)) = χ(M (χ)) = χ(µ ◦ M (η ◦ χ) ◦ id)= χ(arr(χ) >>> id) = χ(id) ◦ χ(arr(χ)) = χ(id) ◦ χ(id)= χ(id >>> id) = χ(µ ◦ M (id) ◦ id) = χ(µ)= χ(µ ◦ M (id) ◦ η ◦ µ) = χ(arr(µ) >>> id)= χ(id) ◦ χ(arr(µ)) = χ ◦ µ.

24

Jacobs, Heunen, Hasuo

The proof is completed by checking that the correspondence is indeed bijective:
χ(a) = χ ◦ a

ϕ = ϕ(id)= ϕ ◦ id= χ(id) ◦ χ(arr(a))=ϕ= χ(arr(a) >>> id)= χ(µ ◦ M (id) ◦ η ◦ a)
= χ(a).

There is a dual result for comonads. It shows that arrow-algebras form a common
generalisation of monad algebras and comonad coalgebras. The proof is similar tothe one above, and left to the reader.
Proposition 6.2
For a comonad N there is a bijective correspondence between comonad-coalgebras
id ⇒ N and arrow-algebras N ⇒ Hom.
The previous two propositions can be extended to bi-algebras.
Proposition 6.3
Let M be a strong monad, N a comonad, and λ : N M ⇒ M N a distributive
law between them. Then there is a bijective correspondence between λ-bi-algebras
M ⇒ id ⇒ N and arrow-algebras (M, N ) ⇒ Hom as in (12).
Proof
We shall only give the essentials, and leave details to the reader. Assuming a λϕψbialgebra M =⇒ id =⇒ N , the following diagram commutes by definition.
M

ϕ

/ id

/N
O
ϕN

ψM


NM

ψ

λ

/ MN

We obtain an arrow-algebra (ϕ, ψ) : (M, N ) ⇒ Hom by (ϕ, ψ)(a) = ϕ ◦ a ◦ ψ. It
satisfies the required equations.
Conversely, an arrow-algebra χ : (M, N ) ⇒ Hom induces a pair of maps χ =(χ1 , χ2 ) by
χ1 = χ(M X,X) (εM X ) : M X −→ X
χ2 = χ(X,N X) (ηN X ) : X −→ N X.
Of the verification that it yields an appropriate λ-bialgebra, we only show commutation of the above diagram, i.e. that we have a compatible algebra-coalgebrapair.
χ1 ◦ λ ◦ χ2 = χ(ε) ◦ χ(arr(λ)) ◦ χ(η) = χ(η >>> arr(λ) >>> ε)= χ([µ ◦ M (η ◦ λ ◦ ε) ◦ λ ◦ N (η) ◦ δ] >>> ε)= χ([η ◦ λ] >>> ε) = χ(µ ◦ M (ε) ◦ λ ◦ N (η ◦ λ) ◦ δ)= χ(λ) = χ(µ ◦ M (η) ◦ λ ◦ N (ε) ◦ δ)= χ(ε >>> η) = χ(η) ◦ χ(ε) = χ2 ◦ χ1 .

Categorical semantics for arrows

25

The next Lemma shows that arrow algebras are retractions of Kleisli categories.
Lemma 6.1
An algebra for an arrow A on C is precisely a left inverse K : CA → C of the“Kleisli inclusion” functor JA : C → CA . (A left inverse is sometimes also called a
retraction, and means KJ = id.)
Proof
Given an algebra χ : A ⇒ Hom we get a functor CA → C by X 7→ X and a 7→ χ(a).
It forms a retraction because χ(arr(f )) = f . Conversely, a retraction K : CA → C
yields an algebra K : A ⇒ Hom by a 7→ K(a). We check naturality:
K(A(f, g)(a)) = K(arr(f ) >>> a >>> arr(g))= K(arr(g)) ◦ K(a) ◦ K(arr(f ))= KJ(g) ◦ K(a) ◦ KJ(f )= g ◦ K(a) ◦ f= Hom(f, g)(K(a)).
The previous Lemma justifies the term Eilenberg-Moore algebra for arrows, since
the next Lemma gives an analogous characterisation for monads.
Lemma 6.2
For a monad M on a category C, there is a bijective correspondence between
algebras M ⇒ id and retractions of the Kleisli inclusion J : C → CM .
ProofGiven an algebra ϕ : M ⇒ id, define a functor ϕ : CM → C by X 7→ X andf 7→ ϕ ◦ f . This clearly yields a functor, and a moreover a retraction:
ϕ(J(f )) = ϕ(η ◦ f ) = ϕ ◦ η ◦ f = f.
Conversely, given a retraction K : CM → C of J, we define K : M ⇒ id via
K X = K(idM X : M X → X) : M X → X. This yields a natural transformation,
and a monad algebra:
K X ◦ ηX = K(id) ◦ KJ(η)

K X ◦ M (K X ) = K X ◦ K M X= K(µ ◦ M (id) ◦ η ◦ η)

= K(id) ◦ K(id)= K(η)= K(µ ◦ M (id) ◦ id)= id,= K(µ)= K(µ ◦ M (id) ◦ η ◦ µ)
= K(id) ◦ KJ(µ)= K X ◦ µ.
6.3 Freyd is Kleisli, for arrows

For monads and comonads, the Kleisli construction is characterised 2-categoricallyas a certain left 2-adjoint (Street, 1972). Theorem 6.2 will prove that the (bijective) mapping A 7→ (C → CA ) that we have been looking at allows a similar

26

Jacobs, Heunen, Hasuo

2-categorical characterisation. Therefore the bijective mapping is justifiably called
the Kleisli construction for arrows. This subsection will extend the notion of arrowon a category with finite products to arrows on Freyd categories in general, andstudies some additional (2-categorical) properties. It assumes a reasonable level offamiliarity with 2-categories; we refer to (Borceux, 1994a) for details.
Let us first recall the situation for monads. The Kleisli construction is the left
2-adjoint of the canonical “insertion” 2-functor Ins in the following 2-adjunction.3
Ins

Cat k

+ Mnd(Cat∗ )∗

>

(32)

K`

Here the 2-category Mnd(Cat∗ )∗ is such that:• An object is a pair (C, M ) of a category C and a monad M on it;• A 1-cell (H, σ) : (C, M ) → (D, M 0 ) is a pair of a functor H : C → D anda natural transformation σ : HM ⇒ M 0 H, which is compatible with monadstructures of M and M 0 .
C
M


C

H

EM

σ 



H

/D
M
/D

0

• A 2-cell α : (H, σ) ⇒ (H 0 , σ 0 ), is a natural transformation α : H ⇒ H 0 whichis compatible with σ and σ 0 in a suitable sense.
The functor Ins is a canonical one mapping an object C to (C, id). The functor K`of the Kleisli construction maps an object (C, T ) to the Kleisli category CT .
Let us go through similar 2-categorical motions for arrows. Denote by FPCat
the 2-category of categories with finite products. At first, one may try for a functor
K` : ArrFPCat → FPCat for a suitably defined 2-category ArrFPCat of arrows,4which maps (C, A) to CA . However, the category CA does not necessarily have finite
products; it has only the weaker structure of a Freyd category. The same difficulty
occurs already attempting to extend the 2-adjunction (32) to strong monads. The
problem is resolved by considering arrows on Freyd categories. The 2-adjunction

3 The notation Mnd(Cat∗ )∗ originates in (Street, 1972); see its Section 4. The operator ()∗
on 2-categories opposes 1-cells (but not 2-cells). The constructor Mnd is actually a 2-functor
which maps a 2-category C to the “2-category of monads” on C.
4 We use the notation Arr
FPCat rather than Arr(FPCat). The notion of monad is defined inany 2-category C hence the notation Mnd(C) makes sense; whereas the notion of arrow does
not come with such generality.
Moreover, two ∗’s in Mnd(Cat∗ )∗ are gone in the corresponding ArrFPCat . The two ∗’s were
there due to the choice of “lax” monad morphisms as 1-cells in Mnd(C) (which is convenient
for the Eilenberg-Moore construction); to have “oplax” monad morphisms instead as 1-cells weneeded two ∗’s. In defining the “category of arrows” ArrFPCat there is no room for such choice
between lax and oplax. For example, in the diagram (C 1) the 2-cell Hom(H) must be in thisdirection and not the other.

Categorical semantics for arrows

27(32) for arrows then looks as follows.
Ins

Freyd k

>

+ Arr

(33)

Freyd

K`

The definition of arrows on Freyd categories is exactly the same as on categories
with finite products, except for the conditions on f irst. Recall that in a FreydJ
category C → K, the category K has a premonoidal structure denoted by .
Definition 6.6 (Arrows on Freyd categories)
J

>>>

arr

An arrow on a Freyd category C → K is a monoid A ⊗ A → A ← Hom in themonoidal category [Kop × K, Set] of bifunctors, equipped with morphisms
f irstX,Y,Z : A(X, Y ) → A(X  Z, Y  Z) ,that are natural in X, Y and dinatural in Z, and satisfy the following equations.
f irst(a) >>> arr(J(π1 )) = arr(J(π1 )) >>> a(5’)

f irst(a) >>> arr(id  J(f )) = arr (id  J(f )) >>> f irst(a)(6’)

f irst(f irst(a)) >>> arr(α) = arr(α) >>> f irst(a)(7’)

f irst(arr(g)) = arr(g  id)(8’)

f irst(a >>> b) = f irst(a) >>> f irst(b)(9’)

The conditions (5’)–(9’) correspond to (5)–(9) in the original definition. The
equations (2)–(4) are already incorporated by the requirement that A be a monoid.
Because J preserves premonoidal structure, the associativity isomorphisms α in(7’) are inherited from C as αK = J(αC ). Recalling the intuition that a morphism
in C is a pure function while one in K is an effectful one, (6’) requires only purefunctions to commute with f irst(a).
For arrows on categories with finite products, Proposition 4.3 establishes theequivalence between the operations f irst and ist. This is also the case for arrows
on Freyd categories, but here we prefer f irst.
The ingredients of the adjunction (33) are defined straightforwardly, although
they become lenghty when spelled out, and there are some hidden subtleties in thedetails. We merely sketch the definitions here, and refer to Appendix C for thedetails.
The 2-categories Freyd and ArrFreyd are those of Freyd categories and arrows
J

on Freyd categories, respectively. The 2-functor Ins carries an object C → K to theJcanonical Hom-arrow (C → K, HomK ). The 2-functor K` in the converse direction
is essentially the Kleisli construction for arrows in Definition 6.1. Namely, an object
JA
JA
J
J
(C → K, A) is mapped to a Freyd category C → K →KA , where K →KA isconstructed like in Definition 6.1.
Now we are ready to prove the (informal) claim “Freyd is Kleisli, for arrows”.
Theorem 6.2 (“Freyd is Kleisli”)
There is a 2-adjunction K` a Ins : ArrFreyd → Freyd as in diagram (33).

28

Jacobs, Heunen, Hasuo

Proof(id,JA ,ι)

J

J

J

A
Its unit is given by (C → K, A) −→ (C → K →KA , HomKA ), where ι is the
canonical natural transformation with components id : A(X, Y ) → KA (X, Y ).

Arrows on categories with finite products also form a 2-category ArrFPCat , justlike ArrFreyd . The obvious horizontal insertion 2-functors produce the following
situation.
ArrFreyd o
U

Ins 0

ArrFPCatO

K` a Ins


Freyd o

Ins

(34)

FPCat

Ins

We conclude this section by elaborating this diagram. The following theorem gives
its relation to the correspondence result of Theorem 6.1.
Theorem 6.3
The bijective correspondence of Theorem 6.1 between Freyd categories and arrows
on categories with finite products extends to an isomorphism between 2-categories
Freyd and ArrFPCat in an obvious way.
Arr∼=

Freyd l-ArrFPCatK`J

An intuition on an object (C → K, A) of ArrFreyd is that it has two different
levels of extra computational structures added to C. One is described by the FreydJ
category C → K, and on top of it we have the other one expressed as the arrow
A. But in fact, the additional expressive power that comes from having two infrastructures is essentially redundant. This can be put in precise 2-categorical terms,
for the details of which we refer to (Jacobs & Hasuo, 2006).
7 Conclusion
Arrows are powerful tools in functional programming. They provide compositional
infrastructure, relieving the programmer of tedious bookkeeping, and in fact enable
more general interfaces than monadic programming.
The present article considered categorical denotational semantics for arrows. The
pivotal point is Definition 4.2, characterising an arrow as a monoid in the categoryof bifunctors Cop ×C → Set, that moreover has a structure called internal strength.
This monoidal structure of arrows has been illustrated by several important realworld examples. Two of them were discussed leading up to the categorical definition
in a way that does not require the arrow laws to be checked by hand. We have shownthat a third language extension (biarrows) can be formulated elegantly using theprovided semantics, indicating that they provide the right perspective and level ofabstraction.
Exploiting the similarity to monads then led to Kleisli and Eilenberg-Moore constructions for arrows. The definitions have been supported by results analogous tothat of (co)algebras for a (co)monad.

Categorical semantics for arrows

29

In fact, we have proven rigorously that the Kleisli construction for arrows corresponds precisely to a Freyd category. This turns the folklore claim that “arrows
are Freyd categories”, that has always remained informal, into a mathematically
precise statement. The arrows-as-monoids perspective, however, is not so delicate
as Freyd categories. Moreover it stresses the compositional infrastructure an arrowprovides.
Ultimately, as with any denotational semantics, this approach aids functional
programmers in reasoning about their programs. For example, it facilitates proving that the language extension induced by an arrow satisfies the desired domainspecific properties that initiated its design.
An interesting topic that has not yet been elaborated is recursion schemes forarrows (Erkök & Launchbury, 2002; Benton & Hyland, 2003), that might find amore thorough theoretical foundation in the present work.
Acknowledgement
We gratefully acknowledge John Power, who not only led us to the correspondence with Freyd categories, but also conjectured Lemma 6.1 immediately uponseeing Definition 6.5. We are also thankful for fruitful discussions with Thorsten
Altenkirch, Tarmo Uustalu, and Paul Blain Levy.

A Coends
This appendix briefly recalls the notion of (parametrised) coends (for more information, see Mac Lane 1971, Section IX.6). This is then applied, as promised in
section 4.4, to ensure that the category Cat(Cop × C, V) has monoidal structure
for suitable categories C and V. We specialise the category V later.
A coend of a bifunctor A : Cop × C → V consists of an object V ∈ V and a•universal dinatural cocone c : A =⇒ V . Explicitly, a dinatural cocone c consistsof morphisms cP : A(P, P ) → V for each P ∈ C such that, for each morphism
f : P → Q of C the following diagram commutes.
A(idP ,f )ddd2 A(P, P ) YYY cPd
YYYYYY
ddddddd
YY,
A(P, Q) ZZZZZZ
eeee2 VZZZZZ,
eeeeceQeeA(f,idQ )A(Q, Q)•

Moreover c is universal in the sense that for every dinatural cocone e : A =⇒ V 0
there is a unique mediating morphism g : V → V 0 as follows.
A(idP ,fh)hhhh4

hhh
hhhh
A(P, Q) VV
VVVV
VVVV
A(f,idQ ) VV*

A(P, P ) TZZZZZZZTTTT ZZZZZZZ ePZZZZZZZTTTZZZZZcP TTTT*__g _ _ _ _ _ZdZd_ZdZd_Zd-/1 V 0
4VjcQ jjjddddddd
jjjj
ddddddd
jdjdjdjddddddddd eQ
A(Q, Q)The object V , when it exists, is unique up to isomorphism. By abuse of language, it

30

Jacobs, Heunen, Hasuo

RP
is called the coend of A, and it is denoted by V =A(P, P ). The fact that coend
V does not depend on the ‘bound variable’ P makes the remark in section 4.1 thatthe parameter P is auxiliary more specific.
We described for each P, Q ∈ C a coend as an object in V. The following lemmashows that they cooperate so as to form a functor, even when parametrised, as
desired later.
Lemma A.1
Let V be a monoidal category, and suppose A, B : Cop × C → V are bifunctors
such that for each X, Y ∈ C, the functor
A(X, −) ⊗ B(−, Y ) : C × Cop → V
has a coend in V. Then these coends extend to a functor
Z P
A(−, P ) ⊗ B(P, −) : Cop × C → V.

(A 1)

(A 2)

Proof
This is a special case of Theorem IX.7.2 in (Mac Lane, 1971).
Given two bifunctors A, B : Cop ×C → V, we would like to define their monoidal
product A ⊗ B : Cop × C → V to be the coending bifunctor (A 2). For this we need
all the coends of (A 1) to exist. The naturality of arr in Lemma 4.2 suggests that
exponentiation should be the unit of the desired monoidal structure. This requiresthat C be V-enriched. This means that we assume objects C(X, Y ) ∈ V withsuitable identity and composition morphisms IX : IV → C(X, X) and CX,Y,Z :C(X, Y ) ⊗ C(Y, Z) → C(X, Z). Moreover, we consider V-bifunctors instead ofbifunctors, which means that we also have morphisms A(X,P ),(Q,Y ) : C(Q, X) ⊗C(P, Y ) → A(Q, Y )A(X,P ) in V analogous to application of the bifunctor A. For
more information, see (Borceux, 1994, Section 6.2; Kelly, 1982); another article witha lot of related information is (Cattani & Winskel, 2004). This requires V to haveexponents (with respect to its tensors) and thus to be monoidal closed.
Indeed, under these conditions, the above ideas combined with Lemma A.1 provide the desired monoidal structure, as the next proposition demonstrates. Its construction dates back to (Day, 1970).
Proposition A.1
Let V be a symmetric monoidal closed category, and C a V-enriched category.
Suppose that all the coends of the functor (A 1) exist. Then V-Cat(Cop × C, V)
is monoidal.
Proof
Due to the V-enrichedness of C and closedness of V we can define a V-bifunctor
I : Cop × C → V by
I(X, Y ) = C(X, Y ) ∈ V
whose action on morphisms, i.e. the morphism
I(X,Y ),(X 0 ,Y 0 ) : C(X 0 , X) ⊗ C(Y, Y 0 ) → C(X 0 , Y 0 )C(X,Y )Categorical semantics for arrows

31

in V, is the transpose of the iterated composition morphism
C(X 0 , X) ⊗ C(Y, Y 0 ) ⊗ C(X, Y ) ∼= C(X 0 , X) ⊗ C(X, Y ) ⊗ C(Y, Y 0 ) → C(X 0 , Y 0 ).
Next, notice that Lemma A.1 duly enriches over V (see Kelly, 1982, Section2.1), so that for V-bifunctors A, B : Cop × C → V we can define a V-bifunctor
A ⊗ B : Cop × C → V by
Z P
A⊗B =
A(−, P ) ⊗ B(P, −).
Recall that coend calculus is known to be associative up to isomorphism (Mac
Lane, 1971, Proposition 9.8). So to show that the above are indeed a monoidal
product and unit, it suffices to give natural isomorphisms λA : I ⊗ A ⇒ A andρA : A ⊗ I ⇒ A. We concentrate on ρ for the purposes of the proof. (In fact, this is
an instance of the enriched Yoneda lemma.)
For each P ∈ C we define a morphism eP : IV → A(X, Y )A(X,P )⊗I(P,Y ) as thetranspose of the following composite, where IV is the monoidal unit of V.
e0P

l l
l l
IV ⊗ A(X, P ) ⊗ I(P, Y )


l5
l l

A(X, Y ) iT
TTTT
V
TTev
TTTT
TTTT
A(X, P ) ⊗ A(X, Y )A(X,P )O∼=

A(X, P ) ⊗ IV ⊗ C(P, Y )id⊗A(X,P ),(X,Y )id⊗IX ⊗id

/ A(X, P ) ⊗ C(X, X) ⊗ C(P, Y )•These form a V-dinatural transformation e : A(X, −) ⊗ I(−, Y ) =⇒ A(X, Y ).
(The fact that the domain of eP is the monoidal unit in V is caused by the Venrichedness of the (di)natural transformation.) Since A ⊗ I is a coend, there is aunique morphism ρX,Y : (A ⊗ I)(X, Y ) → A(X, Y ) such that ρX,Y ◦ cP = eP , where•c : A(X, −) ⊗ I(−, Y ) =⇒ (A ⊗ I)(X, Y ) is the coending dinatural transformation.
Then ρ is a natural isomorphism. The natural transformation whose component
A(X,Y )
ρ−1
at X, Y is the transpose of the composite
X,Y : IV → (A ⊗ I)(X, Y )IV ⊗ A(X, Y ) ∼= A(X, Y ) ⊗ IV

id⊗IY

/ A(X, Y ) ⊗ C(Y, Y )cY/ / (A ⊗ I)(X, Y ).

is the inverse of ρX,Y , which shows that ρ is indeed a natural isomorphism, as
required.
To arrive at the monoidal structure of the previous proposition, we relied on theexistence of all the coends of (A 1). However, since we are only after a monoid inop× C, V), it suffices to require the existence only of coends of the form
RCat(CP
A(X, P ) × A(P, Y ) for all A : Cop × C → C and X, Y ∈ C. Recall that insection 4.4 we only needed C to be small. The previous observations lead to thefollowing extension of this requirement.
Definition A.1
A category C is said to support arrows in a symmetric monoidal closed category

32

Jacobs, Heunen, Hasuo

V if it is V-enriched,R and for each V-bifunctor A : Cop × C → V and each pairP
X, Y ∈ C the coendA(X, P ) ⊗ A(P, Y ) exists.
The previous machinery allows us to generalise our main definition, Definition 4.2.
Definition A.2
Let C be a category with finite products that supports arrows to V. An arrow over
C is a monoid in V-Cat(Cop × C, V) that carries an internal strength.
Notable special cases of the previous definition are V = C Cartesian closed, andV = Set. The latter case reduces the situation to profunctors, which we studied in
Section 4.4. The former one most closely resembles categorical semantics of Haskell,in that it concerns just one category of types and terms. But if C = V is to be
Cartesian closed, small and cocomplete, then it is forced to be a preorder (Freyd,
1964, Chapter 3, Exercise D). However, small complete internal categories do exist (Hyland, 1988), and can indeed be used as models for polymorphic type theory.
Working in such a universe is very similar to working in a polymorphic type theory
as we have done in Section 4.4. Separating size issues is one of the reasons we haveconsidered bifunctors to an enriching category V in this appendix.

B Bicategorical characterisation
Now that we have characterized arrows using categories enriched in a monoidal
closed category in Appendix A, we may as well go one step further and give a unified
characterisation of monads and arrows using categories enriched in a bicategory.
As a bicategory is a 2-category in which composition is only associative up toisomorphism, this allows for the category of profunctors – after all, compositionof profunctors depends on products in Set, that are not strictly associative. Thisapproach cleanly exhibits the mottomonad ∼ Functor
.
=
arrow
Profunctor
The definitions below clearly indicate that both arrows and monad are instances of
monoids; the only difference is that one has to take the right category to base themonoid on. Finally, this unified approach gives an intuitive basis of Theorem 6.2.
Definition B.1
Let V be a bicategory, and V ∈ V. By a monoid on V we mean a monoid in
the monoidal category V(V, V ), with the identity morphism and composition formonoidal structure.
To justify this terminology, observe that, an (ordinary) monoid in a monoidal
category C is a monoid in the corresponding one-object bicategory.
Definition B.2
Let C be a category enriched in V. A V-monad on C is a monoid on C in V-Cat.
A V-arrow on C is a monoid on C in V-Prof .

Categorical semantics for arrows

33

For C a category, a Set-monad on C is simply an (ordinary) monad. Unwinding
the definition, a Set-arrow A on C boils down to a monoid in Cat(Cop × C, Set).
Hence a Set-arrow of the previous definition closely resembles Definition 4.2 for thecase V = Set, since the only thing missing is the (internal) strength. Equivalently,
we can see A as an ‘index’, and speak of a category D with the same objects as C
and with homsets D(X, Y ) = A(X, Y ) instead, in which identity and composition
are given by the monoidal structure on A. Still another equivalent way of putting
this is an identity-on-objects functor J : C → D. Conversely, given a category D
and an identity-on-objects functor J : C → D we can reconstruct a Set-arrow A
on C by A(X, Y ) = D(X, Y ) and A(f, g) = Jg ◦ (−) ◦ Jf . This suggests that arrows
over C should resemble identity-on-objects functors C → D to a category D withthe same objects as C, with added conditions corresponding to internal strength.
To incorporate the internal strength restriction, consider the following definition.
Definition B.3
Let C be a category with finite products. Define a Cat(Cop , Set)-enriched category
self(C) by the same objects as C, and homobjects (self(C))(X, Y ) = C((−)×X, Y ).
For a category C with finite products, a Cat(Cop , Set)-monad on self(C) is an(ordinary) strong monad on C. Analogously, we can talk about Cat(Cop , Set)arrows on self(C) as ‘internally strong arrows over C’. These correspond to a Freyd
category J : C → D.

C 2-categorical details in the Kleisli construction for arrows
The 2-category Freyd of Freyd categories is defined in the following obvious way.
J

• An object is a Freyd category C → K.
JI

• A 1-cell (F, H) : (C → K) → (D → L) is a pair of a functor F : C → D
preserving finite products and a functor H : K → L preserving premonoidal
structures, such that IF = HJ.
JI• A 2-cell (α, β) : (F, H) ⇒ (F 0 , H 0 ) : (C → K) → (D → L) is a pair of naturaltransformations α : F ⇒ F 0 and β : H ⇒ H 0 such that Iα = βJ.
The 2-category ArrFreyd of arrows on Freyd categories is as follows.
J• An object is a pair (C → K, A) of a Freyd category an arrow A on that.
J

I

J• A 1-cell (F, H, σ) : (C → K, A) → (D → L, B) is a 1-cell (F, H) : (C →IK) → (D → L) of Freyd together with a natural transformation
H op ×H/ Lop × L
Kop × K
KKK
σ
tt
=⇒
KKK
tt
A K%
ytt B
,
Set
which is compatible with arr, >>> and f irst, in the following sense.

34

Jacobs, Heunen, Hasuo— σ • arrA = arrB ◦ (H op × H) • Hom(H). Here Hom(H) is the following
natural transformation induced by H’s action on morphisms.
op

H ×H/ Dop × D
Cop × CKKK Hom(H)KKK =⇒ sssss(C 1)
HomC K%yss HomDSet— σ • >>>A = >>>B ◦ (H op × H) • (σ ⊗ σ), where the natural transformationσ ⊗ σ is defined in the following obvious manner.
(σ⊗σ)X,Y(A ⊗ A)(X, Y ) _ _ _ _ _ _ _ _ _/ (B ⊗ B)(HX, HY )OO``
_ _ _ _/ Q∈D B(HX, Q) × B(Q, HY )P ∈C A(X, P ) × A(P, Y )
O
O
κP

κHP

A(X, P ) × A(P, Y )σX,P ×σP,Y/ B(HX, HP ) × B(HP, HY )Note that this construction of σ ⊗ σ : A ⊗ A ⇒ (B ⊗ B) ◦ (H op × H) is
not an instance of the functoriality of ⊗.
— With f irst: for each X, Y, Z in C,/ B(HX, HY )σA(X, Y )B

f irstAA(X  Z, Y  Z)σ
/ B H(X  Z), H(Y  Z)∼=

 f irst
/ B HX  HZ, HY  HZ

where the isomorphism is because H preserves premonoidal structures.
JI• A 2-cell (α, β) : (F, H, σ) ⇒ (F 0 , H 0 , σ 0 ) : (C → K, A) → (D → L, B) is a
2-cell (α, β) : (F, H) ⇒ (F 0 , H 0 ) of Freyd which is compatible with σ and σ 0
in the following sense.
H op ×H 0,

H op ×H 0, op
KS0  ×K2 Lt × L
JJ β ×H
JJ
tt
JJ
σ0
tt
J
t
=⇒
JJ
t
A
%
ztt B
.
Set
(C 2)
0
Here, note that a natural transformation β : H ⇒ H : K → L induces its
opdual β op : H 0 ⇒ H op : Kop → Lop , with the direction of ⇒ reversed.
K

op

op

 KS 
×β  op×K
K
2 Lt × L
JJ H
JJ
t
=
t
JJ
σ
tt
JJ =⇒
tt
A
J%
ztt B
Set

op

op

The 2-functor Ins : Freyd → ArrFreyd acts as follows.
J

J• An object C → K is mapped to (C → K, HomK ). The bifunctor HomK is
obviously an arrow: its operation f irst comes from the premonoidal structureof K.
• A 1-cell (F, H) is mapped to (F, H, Hom(H)). Compatibility of Hom(H) withf irst is because H preserves premonoidal structures.
• A 2-cell (α, β) : (F, H) ⇒ (F 0 , H 0 ) is mapped as it is. The compatibility of βwith Hom(H) and Hom(H 0 ) amounts to the naturality of β : H ⇒ H 0 .

Categorical semantics for arrows

35

The 2-functor K` : ArrFreyd → Freyd is essentially the Kleisli construction forarrows in Definition 6.1. Namely,
J

J

J

A
KA , where• An object (C → K, A) is mapped to a Freyd category C → K →JAK→
KA is constructed like in Definition 6.1. The composition JA ◦J is indeed
a Freyd category: for example it preserves central morphisms essentially due
to the arrow law (6’).
JI• A 1-cell (F, H, σ) : (C → K, A) → (D → L, B) induces a functor H̃ : KA →LB such that: H̃X = HX on objects and H̃f = σX,Y (f ) on morphisms.
• A 2-cell (α, β) is mapped to (α, β̃), where a component β̃X is given by arr(βX ).
The naturality of β̃ amounts to the coherence condition (C 2).

References
Alimarine, A., Smetsers, S., van Weelden, A., van Eekelen, M., & Plasmeijer, R. (2005).
There and back again: arrows for invertible programming. Pages 86–97 of: Proceedingsof the 2005 ACM SIGPLAN workshop on Haskell. ACM Press.
Bénabou, J. (2000). Distributors at work. Lecture notes written by Thomas Streicher.
Benton, N., & Hyland, M. (2003). Traced premonoidal categories. Theoretical informatics
and applications, 37(4), 273–299.
Borceux, F. (1994a). Handbook of categorical algebra. Encyclopedia of Mathematics andits applications, vol. 1. Cambridge University Press.
Borceux, F. (1994b). Handbook of categorical algebra. Encyclopedia of Mathematics andits applications, vol. 2. Cambridge University Press.
Cattani, G. L., & Winskel, G. 2004 (October). Profunctors, open maps and bisimulation.
Tech. rept. RS-04-22. BRICS, Aarhus, Denmark.
Day, B. J. (1970). Reports of the midwest category seminar. Lecture Notes in Mathematics,
vol. 137. Springer. Chap. On Closed Categories of Functors, pages 1–38.
Erkök, L., & Launchbury, J. (2002). A recursive do for haskell. Pages 29–37 of: Proceedingsof the 2002 ACM SIGPLAN workshop on Haskell. ACM Press.
Freyd, P. J. (1964). Abelian categories: An introduction to the theory of functor. New
York: Harper and Row.
Heunen, C., & Jacobs, B. (2006). Arrows, like monads, are monoids. Pages 219–236 of:
Brookes, S., & Mislove, M. (eds), Mathematical foundations of programming semantics,
twenty-second annual conference. Electronic Notes in Theoretical Computer Science,
vol. 158.
Hughes, J. (2000). Generalising monads to arrows. Science of computer programming, 37,
67–111.
Hughes, J. (2005). Advanced functional programming. Lecture Notes in Computer Science,
vol. 3622. Springer. Chap. Programming with Arrows, pages 73–129.
Hyland, J. M. E. (1988). A small complete category. Annals of pure & applied logic, 40,
135–165.
Jacobs, B. (1999). Categorical logic and type theory. North Holland.
Jacobs, B. (2006). Distributive laws for the coinductive solution of recursive equations.
Information and computation, 204(4), 561–587.
Jacobs, B., & Hasuo, I. (2006). Freyd is kleisli, for arrows. McBride, C., & Uustalu, T.
(eds), Workshop on mathematically structured functional programming (MSFP 2006).
Electronic Workshops in Computing (eWiC).

36

Jacobs, Heunen, Hasuo

Kelly, G. M. (1982). Basic concepts of enriched category theory. London MathematicalSociety Lecture Notes, vol. 64. Cambridge University Press.
Levy, P. B., Power, A. J., & Thielecke, H. (2003). Modelling environments in call-by-value
programming languages. Information and computation, 185, 182–210.
Li, P., & Zdancewic, S. (2008). Arrows for secure information flow. Tech. rept. MS-CIS08-02. University of Pennsylvania.
Mac Lane, S. (1971). Categories for the working mathematician. Springer.
Moggi, E. (1989). Computational lambda-calculus and monads. Logic in computer science.
Paterson, R. (2001). A new notation for arrows. Pages 229–240 of: International conference on functional programming. ACM Press.
Paterson, R. (2003). Arrows and computation. Pages 201–222 of: Gibbons, J., & de Moor,
O. (eds), The fun of programming. Palgrave.
Peyton Jones, S.L. (ed). (2003). Haskell 98 language and libraries: the revised report.
Cambridge University Press.
Power, J., & Thielecke, H. (1997). Environments, continuation semantics and indexedcategories. Pages 391–414 of: Abadi, M., & Ito, T. (eds), Theoretical aspects of computer
software. Lectures Notes in Computer Science, no. 1281. Springer, Berlin.
Robinson, E.P., & Power, J. (1997). Premonoidal categories and notions of computation.
Mathematical structures in computer science, 7(5), 453–468.
Street, R. (1972). The formal theory of monads. Journal of pure & applied algebra, 2,
149–169.
Swierstra, S. D., & Duponcheel, L. (1996). Deterministic, error-correcting combinatorparsers. Pages 184–207 of: Launchbury, J., Meijer, E., & Sheard, T. (eds), Advanced
functional programming. Lectures Notes in Computer Science, vol. 1129. Springer,
Berlin.
Uustalu, T., & Vene, V. (2005). Signals and comonads. Journal of universal computerscience, 11(7), 1310–1326”.
Vizzotto, J. K., Altenkirch, T., & Sabry, A. (2006+). Structuring quantum effects: Superoperators as arrows. to appear in mathematical structures in computer science, special
issue on quantum programming languages.
Wadler, P. (1992). Monads for functional programming. Program design calculi: Proceedings of the 1992 marktoberdorf international summer school. Springer-Verlag.