Adjunctions in Haskell

adjunction.hs

{-# LANGUAGE NoImplicitPrelude
           , MultiParamTypeClasses
           , FlexibleInstances
           , FunctionalDependencies
           , UndecidableInstances #-}



import           Prelude hiding (id, (.))
import qualified Prelude




---------------------
-- Category basics --
---------------------

-- Category
class Category cat where
    id :: cat a a
    (.) :: cat b c -> cat a b -> cat a c

-- Category-theoretical functors
class (Category cat, Category cat') => FunctorC f cat cat' where
    mapC :: cat a b -> cat' (f a) (f b)

-- Adjunctions in arbitrary categories. The base category (i.e. the one with the monad) comes last!
class ( FunctorC f cat' cat
      , FunctorC g cat cat'
      ) => Adjunction f g cat cat' | f g cat -> cat', f g cat' -> cat where

{-

The picture we need to have in mind is

            f
       ----------->
    cat'          cat
       <-----------
            g

i.e. the 'original' monad is cat' and the 'target' moand is cat.

-}

    unit   :: cat' a (g (f a))
    counit :: cat (f (g a)) a

    leftAdjunct  :: cat (f a) b -> cat' a (g b)
    rightAdjunct :: cat' a (g b) -> cat (f a) b

    leftAdjunct h = mapC h . unit
    rightAdjunct h = counit . mapC h

    unit = leftAdjunct id
    counit = rightAdjunct id




---------------
-- Instances --
---------------

-- Hask is a category
instance Category (->) where
    id  = Prelude.id
    (.) = (Prelude..)

-- Functors induce FunctorCs in Hask
instance Functor f => FunctorC f (->) (->) where
    mapC = fmap




-----------------------------------------
-- Adjunction between Hask and Hask^op --
-----------------------------------------

newtype Op a b = Op { getOp :: b -> a}

class ContraFunctor f where
    contrafmap :: (a -> b) -> f b -> f a

instance ContraFunctor (Op r) where
    -- contrafmap :: (a -> b) -> Op r b -> Op r a
    contrafmap f (Op g) = Op (g . f)

instance Category Op where
    id = Op Prelude.id
    Op f . Op g = Op (g Prelude.. f)

instance Functor f => FunctorC f Op Op where
    -- fmap :: Op a b -> Op (f a) (f b)
    mapC (Op g) = Op (fmap g)

instance ContraFunctor f => FunctorC f (->) Op where
    -- mapC :: (a -> b) -> Op (f a) (f b)
    mapC g = Op (contrafmap g)

instance ContraFunctor f => FunctorC f Op (->) where
    -- mapC :: Op a b -> f b -> f a
    mapC (Op g) = contrafmap g

instance Adjunction (Op r) (Op r) Op (->) where
    -- leftAdjunct :: Op (Op r a) b -> a -> Op r b
    leftAdjunct f = \a -> Op ( \b -> getOp ( getOp f b ) a )

    -- rightAdjunct :: (a -> Op r b) -> Op (Op r a) b
    rightAdjunct f = Op ( \b -> Op ( \a -> getOp (f a) b ) )

    -- unit :: a -> Op r (Op r a)  ~  a -> (a -> r) -> r
    unit   = \a -> Op ( \f -> getOp f a )

    -- counit :: Op (Op r (Op r a)) a
    counit = Op ( \a -> Op ( \f -> getOp f a ) )



--------------------------
-- FunctorC composition --
--------------------------

newtype O f g a = Compose { getCompose :: f (g a) }

instance ( FunctorC f cat cat', FunctorC g cat' cat'') => FunctorC (O g f) cat cat'' where

    -- mapC :: cat a b -> cat'' (O g f a) (O g f b)
    mapC (Compose f) = mapC (mapC f)


----------------------------------
-- Gives rise to the Cont monad --
----------------------------------



-----------------------------------
-- Kleisli arrows and adjunction --
-----------------------------------

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

f >=> g = \x -> f x >>= g
f <=< g = \x -> g x >>= f

instance Monad m => Category (Kleisli m) where
    id = Kleisli return
    Kleisli f . Kleisli g = Kleisli ( f <=< g )

instance Monad m => FunctorC m (Kleisli m) (->) where
    -- mapC :: Kleisli m a b -> (m a -> m b)
    mapC f x = x >>= runKleisli f

newtype Identity a = Identity { runIdentity :: a }

instance Monad m => FunctorC Identity (->) (Kleisli m) where
    -- mapC :: (a -> b) -> Kleisli Identity a b
    mapC f = Kleisli (return . Identity . f . runIdentity)

instance Monad m => Adjunction Identity m (Kleisli m) (->) where

    -- unit :: a -> m (Identity a)
    unit = return . Identity

    -- counit :: Kleisli m (Identity (m a)) a
    counit = Kleisli runIdentity