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