```{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}
, Representation(..)
) where

import Data.Functor.Contravariant

--
-- > Op (f a) b ~ Hask a (g b)
--
-- > rightAdjunct unit = id
-- > leftAdjunct counit = id
class (Contravariant f, Contravariant g) => Adjunction f g | f -> g, g -> f where
leftAdjunct  :: (b -> f a) -> a -> g b
rightAdjunct :: (a -> g b) -> b -> f a
leftAdjunct f = contramap f . unit
rightAdjunct f = contramap f . counit

instance Adjunction (Op r) (Op r) where
unit a = Op (\k -> getOp k a)
counit = unit

-- | This gives rise to the Cont Bool monad
unit a = Predicate (\k -> getPredicate k a)
counit = unit

-- | A representation of a contravariant functor
data Representation f x = Representation
{ rep :: forall a. (a -> x) -> f a
, unrep :: forall a. f a -> (a -> x)
}

-- | Represent a contravariant functor that has a left adjoint
{ rep = flip leftAdjunct ()
, unrep = rightAdjunct . const
}

{ rep = flip rightAdjunct ()
, unrep = leftAdjunct . const
}

--
-- >  Hask (f a) b ~ Op a (g b)
--
-- > rightAdjunct unit = id
-- > leftAdjunct counit = id
class (Contravariant f, Contravariant g) => DualAdjunction f g | f -> g, g -> f where
unitOp :: g (f a) -> a
counitOp :: f (g a) -> a
leftAdjunctOp :: (f a -> b) -> g b -> a
rightAdjunctOp :: (g b -> a) -> f a -> b