Freyd is Kleisli, for Arrows
Bart Jacobs1,2

Ichiro Hasuo2

Institute for Computing and Information Sciences, Radboud University Nijmegen
Postbus 9010, 6500GL Nijmegen, the Netherlands
http://www.cs.ru.nl/{B.Jacobs, I.Hasuo}{b.jacobs, ichiro}@cs.ru.nl

Abstract
Arrows have been introduced in functional programming as generalisations ofmonads. They also generalise comonads. Fundamental structures associated with(co)monads are Kleisli categories and categories of (Eilenberg-Moore) algebras.
Hence it makes sense to ask if there are analogous structures for Arrows. In thisshort note we shall take first steps in this direction, and identify for instance the Freyd
category that is commonly associated with an Arrow as a Kleisli category.
Keywords: Arrow, Freyd category, Kleisli category, Algebra

1. INTRODUCTION
Arrows have been introduced by Hughes [4] as generalisation of monads, in order to capture
a common interface for non-trivial programs such as parsers. See also [7, 5, 13, 1] for more
applications.
From a categorical point of view, Arrows have long been considered as an alternative formulationof the (older) concept of Freyd category, from [10]. Recently, an alternative categorical descriptionof Arrows has emerged [3], as a monoid in a category of bifunctors Cop × C → Sets. This
description is closer to the functional one, and enables a precise formulation of the one-to-one
relationship between Arrows and Freyd categories, see [3] for details.
This setting of Arrows-as-monoids forms the starting point for the investigations in this paper.
It extends the familiar description of monads-as-monoids (see [6, VII.3]) and comonads-asmonoids. Since Kleisli categories and categories of (Eilenberg-Moore) algebras are fundamental
constructions for monads and comonads, we ask ourselves the obvious question: are there
analogous constructions for Arrows?
In this note we shall give first answers, which are formulated at a high level of abstraction, touching
upon a 2-categorical description (like in [11, 9]). Concrete examples are missing at this stage—
apart from examples that come from (co)monads. What we do is formulate notions of algebra andKleisli category for an Arrow, and illustrate that they are reasonable.
In particular, the one-to-one correspondence from Arrows to Freyd categories [3] is identified
as the Kleisli construction for Arrows; hence the title “Freyd is Kleisli”. For this notion of Kleisli
construction we have two justifications: 1) for Arrows induced by (co)monads, it coincides with the(usual) Kleisli construction for (co)monads; 2) it is characterised as a suitable left 2-adjoint, whichis also the case for (co)monads [11]. In the course we extend the notion of Arrows to be definedon Freyd categories, which leads to some additional 2-categorical accounts.
It is straightforward to extend all the notions and results to enriched settings. That is, an Arrowis now a bifunctor Cop × C → V (instead of Cop × C → Sets) where V is a symmetric monoidal
closed category and C is V-enriched. It subsumes for example an Arrow C op × C → C when C is
1 Also part-time at Technical University Eindhoven, NL.

2 Part of this work was done during the authors’ stay at Research Center for Verification and Semantics, National Instituteof Advanced Industrial Science and Technology, Japan. They are grateful for the hospitality.

MSFP ’06

1Freyd is Kleisli, for Arrows

Cartesian closed. This extension is not purely of technical interest: most notions of computations
are found in enriched settings such as by cpo’s and not in Sets. However in this paper we stick to
the non-enriched setting for the sake of simplicity of presentation.
This paper is not self-contained. We shall assume familiarity with earlier work on Arrows and theircategorical semantics. We briefly recall notation and equations for Arrows in Section 2, together
with the main results of [3]: “Arrows as monoids” and “Arrows are Freyd categories”. In Section 3
the notion of Arrow-algebras is introduced and justified. Then we shall identify the construction ofa Freyd category associated with an Arrow as a Kleisli construction in Section 4. Only at this point
we start using a 2-categorical language. We conclude in Section 5.
2. ARROWS
As introduced in [4], an Arrow is in the notation of the programming language Haskell a type classof the form:
class Arrow A wherearr:: (X → Y ) → A X Y(>>>) :: A X Y → A Y Z → A X Z
first :: A X Y → A (X, Z) (Y , Z)
It describes an Arrow as a binary operation (X, Y ) 7→ A X Y —which we shall often write withbrackets as A(X, Y )—together with three operations arr, >>> and first. These operations should
satisfy the following equations.
(a >>> b) >>> c = a >>> (b >>> c),arr(g ◦ f ) = arr(f ) >>> arr(g),

(1)
(2)

arr id >>> a = a = a >>> arr id,
first(a) >>> arr(π1 ) = arr(π1 ) >>> a,

(3)
(4)

first(a) >>> arr(id × f ) = arr (id × f ) >>> first(a),first(a) >>> arr(α) = arr(α) >>> first(first(a)),
first(arr(f )) = arr(f × id)
first(a >>> b) = first(a) >>> first(b)

(5)
(6)
(7)
(8)

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. Also, arr(id × f ) is sometimes written as
second(arr(f )), where
second(a)= arr(γ) >>> first(a) >>> arr(γ),∼=

and γ : X × Y −→ Y × X is the well-known swap-map.
It is not hard to show that an Arrow is a bifunctor: for maps f : X 0 → X and g : Y → Y 0 one candefine:A(f, g)A(X, Y )arr(f ) >>> a >>> arr(g).
A(X 0 , Y 0 ) by a
As shown in [3], Arrows can be understood abstractly as bifunctors A : Cop × C → Sets, mapping
two types X (for input) and Y (for output) to the set/type A(X, Y ) of computations taking elementsof X to elements of Y . The map arr then appears as natural transformation Hom C (−, +) →A(−, +). Composition >>> can also be seen as a natural transformation A ⊗ A → A, for the
MSFP ’062Freyd is Kleisli, for Arrows

standard tensor product ⊗ of bifunctors / profunctors / distributors Cop × C → Sets, see [2]. In thisway one can understand the triple (A, arr, >>>) as a monoid in a category of bifunctors. Such a
monoid thus consists of a a functor A : Cop × C → Sets and natural transformations
>>>

A⊗A

A

arr

Hom

satisfying the familiar monoid laws. Naturality of arr and >>> means that for maps f : X 0 → X andg : Y → Y 0 in C one has:A(f, g)(arr(h))=

arr(g ◦ h ◦ f )A(f, g)(a >>> b)=

A(f, id)(a) >>> A(id, g)(b).

The latter leads to a useful description of the action A(f, g) as A(f, g) = arr(f ) >>> (−) >>> arr(g),because:A(f, g)(a) = A(f, g)(arr(id) >>> a)=

A(f, id)(arr(id)) >>> A(id, g)(a)=arr(f ) >>> A(id, g)(a >>> arr(id))=

arr(f ) >>> A(id, id)(a) >>> A(id, g)(arr(id))=

arr(f ) >>> a >>> arr(g).

As shown in [3], the map first is equivalent to a certain “internal strength” map A(X, Y ) →A(X, X × Y ) with suitable (di)naturality requirements. It will play only a minor role in this paper.
A strong monad (T, η, µ, st) on a category C with finite products induces an Arrow T : C op × C →Sets by (X, Y ) 7→ HomC (X, T Y ). For instance its operator first is given by firstZ (a) = st ◦ (a × Z).
Similarly, for a comonad (G, ε, δ) we write G for the Arrow given by (X, Y ) 7→ Hom C (GX, Y ).
And in case we have both a strong monad T and a comonad G, together with a distributive law
λ : GT ⇒ T G we write the associated Arrow as (G, T ). It is given by (X, Y ) 7→ Hom C (GX, T Y ).
The following definition gives the obvious way to associate a category of “computations” with an
Arrow.
Definition 1 For an Arrow A : Cop × C → Sets, with operations arr, >>> and first, we define anassociated category CA with objects X ∈ C and morphisms X → Y given by elements of the setA(X, Y ). Identities and composition are given by arr and >>> in the obvious manner.
We then have a functor JA : C → CA given by arr. This forms an instance of a Freyd category [8].
For example, the pre-monoidal structure  of CA comes from the operation first; the functor JA
preserves pre-monoidal structures on-the-nose.
ACA ) from Arrows to Freyd categories we shall call the KleisliThis mapping A 7→ (C →construction for Arrows. The justification for this name is one of the main points of this paper.
One way of doing this is as follows; the other 2-categorical one is later in Section 4.

J

For an Arrow induced by a (co)monad, the associated Freyd category C A coincides with the(co)Kleisli category for the (co)monad in a usual sense. For the Arrow (G, T ) induced by a monad
T , a comonad G and a distributive law GT ⇒ T G, the mapping yields what is called the bi-Kleisli
category used e.g. in [12].
A
The Kleisli construction A 7→ (C →CA ) turns out to be a bijective map, from Arrows to Freyd
categories. This observation is made in [3], turning the oft-heard (informal) statement “Arrows are
Freyd categories” [7] into a concrete one.

J

Theorem 2 (Theorem 5.4, [3]) For a locally small category C with finite products, there is a oneto-one correspondence between
MSFP ’063Freyd is Kleisli, for Arrows

1. Arrows A on C;
2. Locally small Freyd categories C → D.
Proof. The Kleisli construction for Arrows associates a Freyd category to an Arrow. Conversely,J
given a Freyd category C → D, we obtain an Arrow A on C by: A(X, Y ) = HomD (JX, JY ).

3. EILENBERG-MOORE ALGEBRAS FOR ARROWSIn this section we shall define the notion of Eilenberg-Moore algebras for Arrows. Its justification
is made in two ways: 1) for Arrows induced by (co)monads it coincides with a variant of the usual
notion of (co)algebras; 2) an Arrow-algebra is the same thing as a retraction of a Kleisli category,much like for monads.
Let us start by the situation for monads. We shall understand (Eilenberg-Moore) algebras (andcoalgebras) in 2-categorical style as natural transformations. This means that an algebra for amonad (T, η, µ) on a category C is a map ϕ : T ⇒ idC satisfying the familiar equations ϕ ◦ η = idand ϕ ◦ T ϕ = ϕ ◦ µ.
Since such a monad T is the same thing as a monoid in the category of endofunctors C → C—with monoidal structure given by functor composition and identity functor—we may write thesemonad equations as diagrams:
idC

η

T
ϕ

µ

T ⊗ T = T2
ϕ ⊗ ϕ = ϕ ◦ Tϕ

idC

idC ⊗ idC

When T is strong we might as well require a coherence condition with its strength. Namely, foreach X, Y ∈ C,st
T (X × Y )TX × Y
(9)

ϕ

ϕ×Y

X ×Y
Recalling that an Arrow is also a monoid—now in the category of bifunctors—we are led to thefollowing notion.
Definition 3 Let A : Cop × C → Sets be an Arrow. An algebra for this Arrow is a naturaltransformation χ : A ⇒ Hom such that:• It is compatible with arr and >>>. That is, the following diagrams commute.
Hom

arr

>>>

A
χ

A⊗A

(10)

χ⊗χ

Hom

∼
=

Hom ⊗ Hom

• It is compatible with first. That is, the following diagram commutes for each X, Y, Z ∈ C.
A(X, Y )firstZ

A(X × Z, Y × Z)

χHom(X, Y )χ
−×Z

Hom(X × Z, Y × Z)

An algebra of an Arrow is thus a (natural) mapping of computations to (pure) functions. One might
expect to have a single mapping χ : A(X, Y ) → Hom(X, Y ), but then it is not clear how to capturecommutation with composition >>>. Specifically, it is not clear how we define χ ⊗ χ in (10).
MSFP ’064Freyd is Kleisli, for Arrows

In elementary terms this means that an algebra χ satisfies the following three equations.
χ(arr(f ))

=

f

=

χ(a >>> b)

χ(b) ◦ χ(a)χ(first(a))=χ(a) × id.

Naturality is a consequence since:χ(A(f, g)(a))=χ(arr(f ) >>> a >>> arr(g))=χ(arr(g)) ◦ χ(a) ◦ χ(arr(f ))=g ◦ χ(a) ◦ f=

Hom(f, g)(χ(a)).

Here is a first basic result.
Proposition 4 For a strong monad T there is a bijective correspondence between strong-monadalgebras T ⇒ id and Arrow-algebras T ⇒ Hom for the corresponding Arrow T .
Later on in this section we shall see two similar results. For this first one we write out the proof infull detail, in order to show which parts are trivial and which are not. Especially the long calculation
below is a bit tricky in the order in which the equations have to be applied.
Proof. Given a monad algebra ϕ : T ⇒ id. We define ϕ : T ⇒ Hom on a ∈ Hom(X, T Y ) byϕ(X,Y ) (a) = ϕY ◦ a. We check that it satisfies the required properties (omitting subscripts forconvenience).
ϕ(arr(f ))ϕ(a >>> b)

=

ϕ◦η◦f

=

ϕ(firstZ (a))=ϕ ◦ st ◦ (a × Z)

f=

(ϕ × Z) ◦ (a × Z)=ϕ ◦ µ ◦ T (b) ◦ a=(ϕ ◦ a) × Z=

ϕ ◦ T (ϕ ◦ b) ◦ a=

ϕ(a) × Z=(ϕ ◦ b) ◦ (ϕ ◦ a)=ϕ(b) ◦ ϕ(a)ϕ(T (f, g)(a))= ϕ(T (g) ◦ a ◦ f )=ϕ ◦ T (g) ◦ a ◦ f=g◦ϕ◦a◦f=

Hom(f, g)(ϕ ◦ a)=

Hom(f, g)(ϕ(a)).

Conversely, given an Arrow-algebra χ : T ⇒ Hom we define χX : T X → X as χ(T X,X) (idT X ).
Then we get a T -algebra. The unit-law and naturality are easy, and done first.
χ◦η=

χ(id) ◦ χ(arr(η))=χ ◦ T (f )=

χ(id) ◦ χ(arr(T (f )))χ(arr(η) >>> id)=χ(arr(T (f )) >>> id)=χ(µ ◦ T (id) ◦ η ◦ η)=χ(µ ◦ T (id) ◦ η ◦ T (f ))

=

χ(η)

=

χ(T (f ))=χ(arr(id))=χ(µ ◦ T (η ◦ f ) ◦ id)

=

id

=

χ(id >>> arr(f ))=χ(arr(f )) ◦ χ(id)=f ◦ χ.

MSFP ’06

5Freyd is Kleisli, for Arrows

Compatibility (9) with strength is proved as follows.
χ×Y=χ(id) × Y(∗)=χ(st ◦ (id × id))=χ(st ◦ id)=

χ(id ◦ st)(†)=χ(id) ◦ st=

χ ◦ st.

Here the equality (∗) is because χ is compatible with first given by first(a) = st ◦ (a × id); (†) isbecause of the naturality of χ.
Verification of the multiplication law is more subtle.
χ ◦ T (χ)= χ(id) ◦ χ(arr(T (χ)))= χ(arr(T (χ)) >>> id)= χ(µ ◦ T (id) ◦ η ◦ T (χ))= χ(T (χ))= χ(µ ◦ T (η ◦ χ) ◦ id)= χ(arr(χ) >>> id)= χ(id) ◦ χ(arr(χ))= χ(id) ◦ χ(id)= χ(id >>> id)= χ(µ ◦ T (id) ◦ id)= χ(µ)= χ(µ ◦ T (id) ◦ η ◦ µ)= χ(arr(µ) >>> id)= χ(id) ◦ χ(arr(µ))= χ ◦ µ.

Finally we check that we really have a bijective correspondence:
ϕ

=

χ◦a

=

= ϕ(id)ϕ ◦ id=χ(id) ◦ χ(arr(a))

=

ϕ

=

χ(arr(a) >>> id)=χ(µ ◦ T (id) ◦ η ◦ a)

=

χ(a).

χ(a)



The definition of χ in this proof suggests that the Yoneda Lemma is applicable. We have chosen
to write out the proof directly, for clarity.
There is a dual result for comonads. This shows that Arrow-algebras form a common
generalisation of monad algebras and comonad coalgebras. The proof is similar to the one above,and left to the reader.
Proposition 5 For a comonad G there is a bijective correspondence between comonadcoalgebras id ⇒ G and Arrow-algebras G ⇒ Hom for the corresponding Arrow G.
We can even extend such results to bialgebras.
MSFP ’06

6Freyd is Kleisli, for Arrows

Proposition 6 Assume a strong monad T , a comonad G, and a distributive law λ : GT ⇒ T G
between them. Then there is a bijective correspondence between λ-bialgebras T ⇒ id ⇒ G andArrow-algebras (T, G) ⇒ Hom.
Proof. We shall only give the essentials, and leave details to the reader. Assume a λ-bialgebra
T =⇒ id =⇒ G, where by definition the following diagram commutes.
ϕ

ψ

ϕ

T

ψ

id

G
ϕG

ψT
GT

TG

λ

We obtain an Arrow-algebra (ϕ, ψ) : (T, G) ⇒ Hom by (ϕ, ψ)(a) = ϕ ◦ a ◦ ψ. It satisfies therequired equations.
In the reverse direction, assume an Arrow-algebra χ : (T, G) ⇒ Hom. We define a pair of maps
χ = (χ1 , χ2 ) as:χ1 = χ(T X,X) (εT X ) : T X −→ Xχ2=

χ(X,GX) (ηGX ):X −→ GX.

and then check that it yields an appropriate λ-bialgebra. Here we only show commutation of theabove diagram, i.e. that we have a compatible algebra-coalgebra pair.
χ1 ◦ λ ◦ χ2

= χ(ε) ◦ χ(arr(λ)) ◦ χ(η)= χ(η >>> arr(λ) >>> ε)= χ([µ ◦ T (η ◦ λ ◦ ε) ◦ λ ◦ G(η) ◦ δ] >>> ε)= χ([η ◦ λ] >>> ε)= χ(µ ◦ T (ε) ◦ λ ◦ G(η ◦ λ) ◦ δ)= χ(λ)= χ(µ ◦ T (η) ◦ λ ◦ G(ε) ◦ δ)= χ(ε >>> η)= χ(η) ◦ χ(ε)= χ 2 ◦ χ1 .

When John Power saw the notion of Arrow-algebra, he immediately conjectured the following“obvious” result.
Lemma 7 An algebra for an Arrow A on C is the same thing as a left inverse (or retraction)
K : CA → C of the “Kleisli inclusion” functor JA : C → CA (meaning that 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). The only thing worth checking is 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)).

Lemma 8MSFP ’067

Freyd is Kleisli, for Arrows

We claim that the previous lemma justifies our notion of Eilenberg-Moore algebras for Arrows,
because for monads we have an analogous characterisation.
For a monad T on a category C, there is a bijective correspondence between algebras T ⇒ idand retractions of the Kleisli inclusion J : C → CT .
Proof. Given an algebra ϕ : T ⇒ id we define a functor ϕ : CT → C by X 7→ X and f 7→ ϕ ◦ f .
This clearly yields a functor, and a retraction since:
ϕ(J(f )) = ϕ(η ◦ f ) = ϕ ◦ η ◦ f = f.
Conversely, given a retraction K : CT → C of J, we define K : T ⇒ id via K X = K(idT X : T X →X) : T X → X. This yields a natural transformation, and a monad-algebra:
K X ◦ T (K X )K X ◦ ηX

= KX ◦ KT X=

K(id) ◦ K(id)=K(id) ◦ KJ(η)=

K(µ ◦ T (id) ◦ id)=

K(µ ◦ T (id) ◦ η ◦ η)

=

K(µ)

=

K(η)

=

K(µ ◦ T (id) ◦ η ◦ µ)

=

id

=

K(id) ◦ KJ(µ)=

K X ◦ µ.



4. FREYD CATEGORIES ARE KLEISLI CATEGORIESFor monads and comonads, the Kleisli construction is characterised 2-categorically as a certain
left 2-adjoint [11]. In this section we show that the (bijective) mapping A 7→ (C → C A ) in the lastsection—from an Arrow to a Freyd category—allows for a similar 2-categorical characterisation.
Therefore the bijective mapping is justifiably called the Kleisli construction for Arrows. In its course
the notion of Arrows is extended to be defined on Freyd categories in general, instead of on
categories with finite products. We will also make some additional accounts on the 2-categoricalproperties of this extended notion of Arrows.
Let us recall the situation for monads. The Kleisli construction is described in the following 2adjunction, as the left 2-adjoint of the canonical “insertion” 2-functor Ins.

Cat

Ins
>
K`

Mnd(Cat∗ )(11)

Here the 2-category Mnd(Cat∗ ) is such that:2• An object is a pair (C, T ) of a category C and a monad T on it;• A 1-cell (H, σ) : (C, T ) → (D, S) is a pair of a functor H : C → D and a natural transformation
σ : HT ⇒ SH, which is compatible with monad structures of T and S.
• A 2-cell α : (H, σ) ⇒ (H 0 , σ 0 ), is a natural transformation α : H ⇒ H 0 which is 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 .
We shall do the same 2-categorical business for Arrows. Let us denote by FPCat the 2-categoryof categories with finite products. We may try to get a functor K` : Arr(FPCat) → FPCat for
2 The notation Mnd(Cat ) comes from [11]. The 2-category Cat is obtained from Cat by reversing 2-cells. The∗∗
constructor Mnd is actually a 2-functor which maps a 2-category C to the 2-category of monads on C.

MSFP ’068Freyd is Kleisli, for Arrows

a suitably defined Arr(FPCat), which maps (C, A) to CA . However, the category CA does notnecessarily have finite products: it has only a weaker structure of a Freyd category. This is thesame difficulty which occurs already when we try to get the 2-adjunction (11) for strong monads.
This problem is mended by considering Arrows on Freyd categories. Hence the 2-adjunction (11)for Arrows would look as follows.

Freyd

Ins
>
K`

(12)

Arr(Freyd)The definition of Arrows on Freyd categories is just the same as on categories with finite products,
J
except for the conditions on first. Recall that in a Freyd category C → K, K has a pre-monoidal
structure which we denote by .
Definition 9 (Arrows on Freyd categories) An Arrow on a Freyd category C → K is a monoid>>>arr
A ⊗ A → A ← Hom in the monoidal category [Kop × K, Sets] of bifunctors, equipped with: foreach X, Y, Z ∈ K,
firstX,Y,Z : A(X, Y ) → A(X  Z, Y  Z) ,J

which is natural in X, Y and dinatural in Z. The operations should satisfy the following equations.
first(a) >>> arr(J(π1 )) = arr(J(π1 )) >>> afirst(a) >>> arr(id  J(f )) = arr (id  J(f )) >>> first(a)first(a) >>> arr(α) = arr(α) >>> first(first(a))
first(arr(g)) = arr(g  id)
first(a >>> b) = first(a) >>> first(b)

(4’)
(5’)
(6’)
(7’)
(8’)

The conditions (4’)–(8’) correspond to (4)–(8) in the original definition. The conditions (1)–(3) aregone because they amount to saying that A is a monoid. The associativity isomorphisms α in(6’) are inherited from C as αK = J(αC ); this is because J preserves pre-monoidal structures.
Recalling the intuition that a morphism in C is a pure function while one in K is an effectful one,(5’) requires only pure functions commute with first(a).
For Arrows on categories with finite products, the operation first is equivalently described as an“internal strength” ist : A(X, Y ) → A(X, Y × X) subject to suitable coherence conditions. This isalso the case for Arrows on Freyd categories: however in the sequel we prefer to use first.
Let us continue by describing ingredients of the adjunction (12).
The 2-category Freyd of Freyd categories is defined in the following obvious way.
• 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 pre-monoidal structures, such that IF = HJ.
JI• A 2-cell (α, β) : (F, H) ⇒ (F 0 , H 0 ) : (C → K) → (D → L) is a pair of natural transformations
00
α : F ⇒ F and β : H ⇒ H such that Iα = βJ.
J

The 2-category Arr(Freyd) of Arrows on Freyd categories is as follows.
• An object is a pair (C → K, A) of a Freyd category an Arrow A on that.
JMSFP ’06

9Freyd is Kleisli, for Arrows• A 1-cell (F, H, σ) : (C → K, A) → (D → L, B) is a 1-cell (F, H) : (C → K) → (D → L) of
Freyd together with a natural transformation
J

I

J

H op × H

Kop × KI

Lop × L

σ

=⇒
A

B

Sets

,

which is compatible with arr, >>> and first, in the following sense.
– σ • arrA = arrB ◦ (H op × H) • Hom(H). Here Hom(H) is the following naturaltransformation induced by H’s action on morphisms.
Cop × C
HomC

H op × H

Dop × D

Hom(H)

=⇒

HomD

Sets


– σ • >>>A = >>>B ◦ (H op × H) • (σ ⊗ σ), where the natural transformation σ ⊗ σ isdefined in the following obvious manner.
(A ⊗ A)(X, Y )`(σ ⊗ σ)X,Y(B ⊗ B)(HX, HY )`P ∈C A(X, P ) × A(P, Y )Q∈D B(HX, Q) × B(Q, HY )

κ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 instanceof the functoriality of ⊗.
– With first: for each X, Y, Z in C,σA(X, Y )B(HX, HY )

A

first
A(X  Z, Y  Z)σ

B H(X  Z), H(Y  Z)∼=firstBB HX  HZ, HY  HZ

where the isomorphism is because H preserves pre-monoidal structures.
• 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.
JI

H op ×H 0

Kop × KHop

H op ×H 0

Lop × L

×β
σ

A

=⇒

Kop × K

B

σ0

A

Sets

Lop × Lβ op ×H 0

=

=⇒
Sets

(13)

B
.

Here note that a natural transformation β : H ⇒ H 0 : K → L induces its dual β op : H 0
H op : Kop → Lop , with the direction of ⇒ reversed.

op⇒

The 2-functor Ins : Freyd → Arr(Freyd) acts as follows.
• An object C → K is mapped to (C → K, HomK ). The bifunctor HomK is obviously an Arrow:its operation first comes from the pre-monoidal structure of K.
• A 1-cell (F, H) is mapped to (F, H, Hom(H)). Compatibility of Hom(H) with first is because
H preserves pre-monoidal structures.
JJ

MSFP ’06

10Freyd is Kleisli, for Arrows• 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 .
The 2-functor K` : Arr(Freyd) → Freyd is essentially the Kleisli construction for Arrows in
Definition 1. Namely,
A
A
KA is
KA , where K →• An object (C → K, A) is mapped to a Freyd category C → K →constructed like in Definition 1. The composition JA ◦ J is indeed a Freyd category: forexample it preserves central morphisms essentially due to the Arrow law (5’).
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 naturalityof β̃ amounts to the coherence condition (13).

J

J

J

J

Theorem 10 We have a 2-adjunction K` a Ins : Arr(Freyd) → Freyd as in Diagram (12).
(id, JA , ι)JAJJ
Proof. Its unit is given by (C →K, A)
KA , HomKA ) , where ι is a canonical(C → K →
natural transformation whose component is given by id : A(X, Y ) → Hom KA (X, Y ).
In relation to Arrows on categories with finite products—which form a 2-category Arr(FPCat) ina way similar to Arr(Freyd)—we have the following situation with the obvious horizontal insertion
2-functors.
Ins 0
Arr(FPCat)
Arr(Freyd)K` a Ins

Ins

Freyd

(14)

FPCat

Ins

In the rest of this section we elaborate further on this diagram. First, the correspondence result
from [3] is incorporated.
Theorem 11 The bijective correspondence in Theorem 2—between Freyd categories and Arrows
on categories with finite products—extends to an isomorphism between 2-categories Freyd andArr(FPCat) in an obvious way.
Freyd

Arr
∼
=
K`

Arr(FPCat)In Diagram (11) for Monads, the insertion functor Ins has a right 2-adjoint given by the obvious
forgetful functor. This is also the case for Arrows.
Proposition 12 Each of the “insertion” 2-functors in Diagram (14) has a right 2-adjoint. For thosenamed Ins it is given by the obvious forgetful functor; the right 2-adjoint of Ins 0 follows from theisomorphism in Theorem 11.

An intuition on an object (C → K, A) of Arr(Freyd) is that it has two different levels of extraJ
computational structures added to C. One is described by the Freyd category C → K, and on topof it we have the other one expressed as the Arrow A. By applying K` : Arr(Freyd) → Freydwe have these two structures combined and expressed as a composed Freyd category. In thissense, the 2-category Arr(Freyd) has extra expressive power—which is essentially redundant—
compared to Freyd. This point is put in precise, 2-categorical terms in the following two
propositions.
J

Proposition 13 Freyd is a full reflective 2-subcategory of Arr(Freyd), with Ins its embedding.

MSFP ’06

11Freyd is Kleisli, for Arrows

Proof. The 2-functor Ins : Freyd → Arr(Freyd) is full, faithful and injective on objects. In
particular, the fullness follows from the compatibility of 1-cells of Arr(Freyd) with arr.

Aside from the insertion functor Ins, there is another canonical 2-functor Freyd → Arr(Freyd)which we shall call Arr . On objects,
J

Ins :

C→K

Arr :

C→K

J

J

7→

(C → K, HomK ) ,7→

C → C, HomK (J−, J+)

id



.

Intuitively, Ins encodes the extra structure carried by J into a Freyd category; Arr does it into an
Arrow.
Proposition 14 We have the following 2-adjunctions.
Ins
>
K`
>
Arr

Freyd

Arr(Freyd)

Proof. Each object (C → K, A) of Arr(Freyd) induces the following two universal morphisms.
Here the canonical natural transformations ι and ι0 have the identity maps as their components.
J

id

C → C, A(J−, J+)0 (id, J, ι )J(C → K, A)(id, JA , ι)

They form the unit/counit of the 2-adjunctions.

J

J

A(C → K →KA , HomKA )Remark 15 We may aim at a similar 2-categorical characterisation of Eilenberg-Moore algebras
for Arrows. Here we shall show an attempt we have taken and how it fails.
The idea comes from the duality between the Eilenberg-Moore and Kleisli constructions formonads. The Eilenberg-Moore construction for monads is characterised as the following right2-adjoint [11].
Cat

Ins
⊥
EMAlg

Mnd(Cat)This is a dual of the 2-adjunction (11) for Kleisli in the following sense. A 1-cell (H, σ) : (C, T ) →(D, S) of Mnd(Cat) has its component σ : SH ⇒ HT , in the reversed direction from Mnd(Cat ∗ ).
We may try the same dualisation of the adjunction (12).
The problem lies in defining the dualised version of Ins. It should map a 1-cell (F, H) in Freyd to(F, H, σ), with some canonical natural transformation σ such thatCop × CH op × H
σ

Dop × D

⇐=
HomC

Sets

HomD

It is not clear how we can get σ in this direction.
5. CONCLUSIONS AND FUTURE WORK
Starting from the observation of Arrows-as-monoids—extending monads-as-monoids—we havemade a first step toward the notions of Kleisli categories and Eilenberg-Moore algebras for Arrows.
The definitions have been presented with reasonable justifications.
MSFP ’06

12Freyd is Kleisli, for Arrows

In particular, the Kleisli category for an Arrow turns out to be the Freyd category that corresponds
to the given Arrow one-to-one. This situation is put clearly in 2-categorical terms, accompaniedwith some additional observations.
The definition of Arrow-algebras in this paper we do not consider fully satisfactory. We might
expect an algebra carried by specific object(s). Concrete examples of what should be called
Arrow-algebras are to be found: those examples would also help us to get a more suitabledefinition.
In [8] Freyd categories are shown to be equivalent to the fibrational notion of κ-categories. The
relation between κ-categories and the current work is yet to be elaborated.
ACKNOWLEDGEMENTS
Thanks are due to Chris Heunen, John Power, Tarmo Uustalu, Hiroshi Watanabe and theanonymous referees for helpful discussions and comments.
REFERENCES[1] A. Alimarine, S. Smetsers, A. van Weelden, M. van Eekelen, and R. Plasmeijer. There andback again: arrows for invertible programming. In Proceedings of the 2005 ACM SIGPLAN
workshop on Haskell, pages 86–97. ACM Press, 2006.
[2] F. Borceux. Handbook of Categorical Algebra, volume 50, 51 and 52 of Encyclopedia of
Mathematics. Cambridge Univ. Press, 1994.
[3] C. Heunen and B. Jacobs. Arrows, like monads, are monoids. In Mathematical Foundationsof Program Semantics, Elect. Notes in Theor. Comp. Sci. 158, Elsevier, Amsterdam, 2006.
[4] J. Hughes. Generalising monads to arrows. Science of Comput. Progr., 37:67–111, 2000.
[5] P. Jansson and J. Jeuring. Polytypic data conversion programs. Science of Comput. Progr.,
43:35–75, 2002.
[6] S. Mac Lane. Categories for the Working Mathematician. Springer, Berlin, 1971.
[7] R. Paterson. A new notation for arrows. In International Conference on Functional
Programming (ICFP), volume 36(10), pages 229–240. ACM SIGPLAN Notices, 2001.
[8] J. Power and H. Thielecke. Environments, continuation semantics and indexed categories.
In M. Abadi and T. Ito, editors, Theoretical Aspects of Computer Software, number 1281 inLect. Notes Comp. Sci., pages 391–414. Springer, Berlin, 1997.
[9] J. Power and H. Watanabe. Combining a monad and a comonad. Theor. Comp. Sci., 280(1–2):137–162, 2002.
[10] E.P. Robinson and J. Power. Premonoidal categories and notions of computation. Math.
Struct. in Comp. Sci., 7(5):453–468, 1997.
[11] R. Street. The formal theory of monads. Journ. of Pure & Appl. Algebra, 2:149–169, 1972.
[12] T. Uustalu and V. Vene. The essence of dataflow programming. In 3rd Asian Symp. on
Programming Languages and Systems, APLAS’05, number 3780 in Lect. Notes Comp. Sci.,
pages 2–18. Springer, 2005.
[13] T. Uustalu and V. Vene. Signals and comonads. Journ. of Universal Comp. Sci., 11(7):1310–
1326, 2005.

MSFP ’06

13