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.


{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MonoLocalBinds         #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

import           Control.Category
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:

![](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:


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...