I thought I would share one of my favorite constructions in Haskell, namely that adjoint functors give rise to monads. Although it’s a trivial result in category theory how it manifests in Haskell is quite lovely.

A Functor in Haskell maps objects and morphism ( i.e. functions) in a subcategory of Hask to objects and morphisms of another category.

class Functor f where
fmap :: (a -> b) -> f a -> f b

And satisfies the functor laws:

fmap id = id
fmap (a . b) = (fmap a) . (fmap b)

In commutative diagrams we draw objects as points and morphisms as arrows. In a string diagrams we invert this and draw morphisms as points and objects as lines.

Functor composition is defined for $$F : \mathcal{A} \rightarrow \mathcal{B}$$, $$G : \mathcal{B} \rightarrow \mathcal{C}$$ as $$G \circ F : \mathcal{A} \rightarrow \mathcal{C}$$, and is drawn with parallel lines.

newtype FComp f g a = C { unC :: f (g a) }

instance (Functor f, Functor g) => Functor (FComp f g) where
fmap f (C x) = C (fmap (fmap f) x)

Generally the composition of functors $$F \circ G$$ is written simply as $$FG$$. Composition diagrammatically allows us to collapse adjacent segements in our string diagram.

The identity functor ( $$\text{Id}$$ ) is the functor that maps each morphism and object to itself.

newtype Id a = Identity { unId :: a }

instance Functor Id where
fmap f x = Identity (f (unId x))

Composition with the identity functor forms an identity relation:

$F \circ \text{Id}_B = F \\ \text{Id}_A \circ F = F$

As witnessed by the expressions:

left :: Functor f => FComp f Id a -> f a
left (C a) = fmap unId a

right :: Functor f => f a -> FComp f Id a
right a = C \$ fmap Identity a

We’ll follow the convention to omit the identity functor, and it is shown as a dotted line in subsequent string diagrams.

A natural transformation in our context will be a polymorphic function associated with two Haskell functor instances f and g with type signature (Functor f, Functor g) => forall a. f a -> g a. Which could be written with the following type synonym.

type Nat f g = forall a. f a -> g a

The identity natural transform mapping a functor $$F$$ to itself is written $$1_F$$ and in Haskell is just (id). The composition of natural transformations follows the associativity laws, shown below:

The final interchange law states that we can chase the natural transformations through the functors horizontally or compose natural transformation between functors vertically and still arrive at the same result.

$(\alpha \beta) \circ (\alpha' \beta') = (\alpha \alpha') \circ (\beta \beta')$

type NatComp f f' g g' = forall a. f' (f a) -> g' (g a)

vert :: (Functor f, Functor f', Functor g, Functor g') =>
Nat f' g' -> Nat f g -> NatComp f f' g g'
vert a b x = a (fmap b x)

horiz :: (Functor f, Functor f', Functor g, Functor g') =>
Nat f' g' -> Nat f g -> NatComp f f' g g'
horiz a b x = fmap b (a x)

By the interchange law horiz and vert must be interchangable under composition. For natural transformations a, b, a', b' in Haskell we have the equation:

(a . b) vert (a' . b') == (a horiz a') . (b horiz b')

A diagram example for a natural transformation $$\eta : 1_\mathcal{C} \rightarrow {FG}$$ between the identity functor and the composition functor of $$FG$$ would be drawn as:

An isomorphism $$F \cong G$$ implies that composition of functors is invertible in that $$F G = \text{Id}_C$$ and $$G F = \text{Id}_D$$. An adjoint $$F ⊣ G$$ between a pair of functors $$F : D \rightarrow C$$ and $$G : C \rightarrow D$$ is a weaker statement that there exists a pair of associated natural transformations $$(F, G, \epsilon, \eta)$$ with:

$\epsilon : FG \rightarrow 1_\mathcal{C} \\ \eta : 1_\mathcal{D} \rightarrow FG$

Such that the following triangle identities hold:

$(\epsilon F) \circ (F \eta) = 1_F \\ (G \epsilon) \circ (\eta G) = 1_G$

These are drawn below:

In terms of the categories $$C,D$$ an adjoint is in some sense a “half-isomorphism” or “almost inverse” but some structure is lost in one direction.

$$\eta$$ and $$\epsilon$$ are also referred to respectively as the unit and counit.

In Haskell we have the following typeclass which unfortunately requires a functional dependency in order for type inferencer to deduce which fmap is to be used:

class (Functor f, Functor g) => Adjoint f g | f -> g, g -> f where
eta     :: a -> g (f a)
epsilon :: f (g a) -> a

There are also two other natural transformations ($$\phi, \psi$$) which together with the adjoint functor pair form an adjunction. The adjunction can be defined in terms of the adjoint pair and this is most convenient definition in Haskell

$\psi \epsilon = 1_F \\ \phi \eta = 1_G$

phi :: Adjoint f g => (f a -> b) -> a -> g b
phi f = fmap f . eta

psi :: Adjoint f g => (a -> g b) -> f a -> b
psi f = epsilon . fmap f

Notably $$\phi$$ and $$\psi$$ form an isomorphism between the set of functions (a -> g b) and (f a -> b) which is the same relation as the above triangle identities. Alternatively $$\eta$$ and $$\epsilon$$ can be expressed in terms of $$\phi$$ and $$\psi$$.

phi eta = id
psi epsilon = id 

From the Haskell Prelude we have the canonical adjoint namely curry and uncurry:

$\text{curry} \quad ⊣ \quad \text{uncurry}$

instance Functor ((,) a) where
fmap f (x,y) = (x, f y)

instance Functor ((->) a) where
fmap f g = \x -> f (g x)

Which we can construction an Adjoint instance from these two functor instances:

instance Adjoint ((,) a) ((->) a) where
eta x y = (y, x)
epsilon (y, f) = f y

We can check that the triangle equalities hold for this definition by showing both $$(\epsilon F) \circ (F \eta)$$ and $$(G \epsilon) \circ (\eta G)$$ reduce to the identity natural transformation ( id ).

a0 :: (a -> (b -> c)) -> a -> (b -> c)
a0 f = \f -> fmap (epsilon . fmap f) . eta
a0 f = fmap ($$y, f) -> g f y) . eta a0 f = \x y -> f x y a1 :: ((a, b) -> c) -> (a,b) -> c a1 f = epsilon . fmap (fmap f . eta) a1 f = epsilon . fmap (\x y -> f (y, x)) a1 f = \(x, y) -> f (x, y) We know a Monad is an endofunctor \(T : C \rightarrow C$$ with two natural transformations $$(T, \mu, \eta)$$ with the usual laws:

$\mu \circ T \mu = \mu \circ \mu T \\ \mu \circ T \eta = \mu \circ \eta T = 1_T \\$

The geometric intuition is that the monad laws are reflected as topological properties of the string diagrams. Both $$\mu$$ and $$\eta$$ exhibit reflection symmetry and that we topologically straighten out $$\eta$$ to yield the identity functor.

In Haskell we can normally construct the Monad type class from an Endofunctor and ($$\mu, \eta$$) or join and return.

class (Functor t) => Monad t where
eta :: a -> (t a)
mu  :: (t (t a)) -> (t a)

(>>=) :: t a -> (a -> t b) -> t b
ma >>= f = mu . fmap f

return = eta
join = mu

What is not immediately apparent though is that every adjoint pair of functors gives rise to a monad $$(T, \mu, \eta)$$ over a category $$C$$ induced by the composition of the functors to give rise to a endofunctor and natural transformations in terms of the unit and counit of the underlying adjunction:

\begin{align} T &= G \circ F & : &C \rightarrow C \\ \mu &= G \epsilon & : &T^2 \rightarrow T \\ \end{align}

class Adjoint f g => Monad f g where
muM :: g (f (g (f a))) -> g (f a)
muM = fmap epsilon

etaM :: a -> g (f a)
etaM = eta

(>>=) :: g (f a) -> (a -> g (f b)) -> g (f b)
x >>= f = muM (fmap (fmap f) x)

The geometric intution for this is clear:

From the Monad we can then construct the Kleisli category in the usual way.

class (Adjoint f g, Category c) => Kleisli c f g where
idK :: c x (g (f x))
(<=<) :: c y (g (f z)) -> c x (g (f y)) -> c x (g (f z))

instance Monad f g => Kleisli (->) f g where
idK = eta
g <=< f = muM . fmap (fmap g) . f

instance Kleisli c f g => Monoid (c a (g (f a))) where
mempty  = idK
mappend = (<=<)

In retrospect this is trivial, but importantly leads us to the more important question: Can we recover an adjunction from a monad. The answer is Yes…