Okay guys, I'll try this.

The following was first established in by Kleisli in [*Every standard construction is induced by a pair of adjoint functors* (1965)](http://www.ams.org/journals/proc/1965-016-03/S0002-9939-1965-0177024-4/)

I am going to leave a bunch of puzzles so others can finish the construction.

Let's start with the boilerplate.

The `Category` typeclass is defined in [`Control.Category`](https://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Category.html) in base. It introduces `id` and `(.)`, which correspond to identity morphisms and morphism composition from category theory.

We diverge from the `Prelude` below. In traditional category theory, a *functor* maps morphisms in one Category into another. The following typeclass captures this.

This leads to the first puzzle:

**Puzzle 1**. What are the laws for CatFunctor? [Hint: They should be familiar...]

An *endofunctor* is a functor from a category to itself.

Haskell's `Functor` is a particular kind of endofunctor. It's on the category `(->)`, which is something called **Hask**.

This is operationally equivalent to the `Functor` in base. Here are the two instances:

So now we are ready for talking about adjunctions. In category theory, we say two functors \\(F: \mathcal{X} \to \mathcal{Y}\\) and \\(G: \mathcal{Y} \to \mathcal{X}\\) are adjoint whenever there is a family of bijections such that:

![](https://latex.codecogs.com/gif.latex?%5Cmathbf%7Bhom%7D_%7B%5Cmathcal%7BY%7D%7D%28FA%2CB%29%20%5Ccong%20%5Cmathbf%7Bhom%7D_%7B%5Cmathcal%7BX%7D%7D%28A%2CGB%29)

This is captured with this typeclass:

The usual Haskell adjunctions are just with endofunctors on `(->)`.

So now to the actualy adjoint constructions. From [`Control.Arrow`](https://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Arrow.html#g:1), there is the following *category* defined:

**Puzzle 2**. Fill out the category instance for `Kleisli m` below. You can always cheat if you want, but maybe don't share?

Finally, we can construct the adjunction. The *left* adjoint is free and doesn't depend on anything:

**Puzzle 3**. (the hard one) The right adjoint is **not** free.

1. Write the `newtype` declaration for it.

2. Write the instance `CatFunctor (Kleisli m) ??? (->)` for it

3. Finally, write the instance for `Monad m => CatAdjunction (->) (Kleisli m) LeftK ???`

------------------------------------------------

I am free to give hints to Puzzle 3. It might help after we finish it to see what this means for posets...

The following was first established in by Kleisli in [*Every standard construction is induced by a pair of adjoint functors* (1965)](http://www.ams.org/journals/proc/1965-016-03/S0002-9939-1965-0177024-4/)

I am going to leave a bunch of puzzles so others can finish the construction.

Let's start with the boilerplate.

{-# LANGUAGE ConstraintKinds #-}

{-# LANGUAGE FlexibleContexts #-}

{-# LANGUAGE FlexibleInstances #-}

{-# LANGUAGE FunctionalDependencies #-}

{-# LANGUAGE MonoLocalBinds #-}

{-# LANGUAGE MultiParamTypeClasses #-}

{-# LANGUAGE TypeOperators #-}

{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module CatAdjunctions where

import Control.Category

import Control.Monad ((<=<)) -- Hint!

import Prelude hiding ((.))

The `Category` typeclass is defined in [`Control.Category`](https://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Category.html) in base. It introduces `id` and `(.)`, which correspond to identity morphisms and morphism composition from category theory.

We diverge from the `Prelude` below. In traditional category theory, a *functor* maps morphisms in one Category into another. The following typeclass captures this.

class (Category x, Category y) => CatFunctor x f y where

catMap :: a `x` b -> f a `y` f b

This leads to the first puzzle:

**Puzzle 1**. What are the laws for CatFunctor? [Hint: They should be familiar...]

An *endofunctor* is a functor from a category to itself.

type EndoFunctor k f = CatFunctor k f k

Haskell's `Functor` is a particular kind of endofunctor. It's on the category `(->)`, which is something called **Hask**.

type HaskFunctor f = EndoFunctor (->) f

This is operationally equivalent to the `Functor` in base. Here are the two instances:

instance Functor f => CatFunctor (->) f (->) where

catMap = undefined

-- Needs UndecidableInstances and -fno-warn-orphans

instance EndoFunctor (->) f => Functor f where

fmap = undefined

So now we are ready for talking about adjunctions. In category theory, we say two functors \\(F: \mathcal{X} \to \mathcal{Y}\\) and \\(G: \mathcal{Y} \to \mathcal{X}\\) are adjoint whenever there is a family of bijections such that:

This is captured with this typeclass:

class ( CatFunctor x f y

, CatFunctor y g x

) => CatAdjunction x y f g where

catLeftAdjunct :: (f a `y` b) -> (a `x` g b)

catRightAdjunct :: (a `x` g b) -> (f a `y` b)

The usual Haskell adjunctions are just with endofunctors on `(->)`.

So now to the actualy adjoint constructions. From [`Control.Arrow`](https://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Arrow.html#g:1), there is the following *category* defined:

newtype Kleisli m a b = Kleisli { runKleisli :: a -> m b }

**Puzzle 2**. Fill out the category instance for `Kleisli m` below. You can always cheat if you want, but maybe don't share?

instance Monad m => Category (Kleisli m) where

id = undefined

(.) = undefined -- This should be familiar...

Finally, we can construct the adjunction. The *left* adjoint is free and doesn't depend on anything:

newtype LeftK a = LeftK { unLeftK :: a }

instance Applicative m => CatFunctor (->) LeftK (Kleisli m) where

catMap = Kleisli . (pure .) . haskCatMap

where

haskCatMap f (LeftK x) = LeftK (f x)

**Puzzle 3**. (the hard one) The right adjoint is **not** free.

1. Write the `newtype` declaration for it.

2. Write the instance `CatFunctor (Kleisli m) ??? (->)` for it

3. Finally, write the instance for `Monad m => CatAdjunction (->) (Kleisli m) LeftK ???`

------------------------------------------------

I am free to give hints to Puzzle 3. It might help after we finish it to see what this means for posets...