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.


{-# 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:

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