Kan Extensions!

.ghci

:set -i.

Adjunctions.hs

{-# LANGUAGE TypeOperators, MultiParamTypeClasses #-}

module Adjunctions where

class (Functor l, Functor r) => l ⊣ r where
  unit :: d -> r (l d)
  unit = leftAdjunct id
  counit :: l (r c) -> c
  counit = rightAdjunct id
  leftAdjunct :: (l d -> c) -> d -> r c
  leftAdjunct f = fmap f . unit
  rightAdjunct :: (d -> r c) -> l d -> c
  rightAdjunct f = counit . fmap f
  {-# MINIMAL leftAdjunct, rightAdjunct | unit, counit |
    leftAdjunct, counit | unit, rightAdjunct #-}

Codensity.hs

{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, DeriveFunctor #-}

module Codensity where
import Adjunctions
import Compose
import Identity
import MonoidalCategory2
import Nat
import Ran

newtype Codensity k a = Codensity (Ran k k a)
  deriving Functor

runCodensity (Codensity (Ran akk)) = akk
codensityToRan (Codensity ran) = ran

instance Functor k => Applicative (Codensity k) where
  pure = return
  mab <*> ma = mab >>= (`fmap` ma)

instance Functor k => Monad (Codensity k) where
  return a = Codensity (Ran (\ak -> ak a))
  (Codensity (Ran akk)) >>= abkk = Codensity (Ran bkk)
    where bkk bk = akk (\a -> (runCodensity . abkk $ a) bk)

class Abs_Ran k d where
  abs_Ran :: Ran k (Compose f d) ~> Compose f (Ran k d)

instance (Functor k, Abs_Ran k Id) => (Ran k Id) ⊣ k where
  unit = decompose . abs_Ran . (rotate_Ran ρ') . codensityToRan . return
  counit = runIdentity . counit_Ran . Compose

Comonad.hs

module Comonad where

class Functor w => Comonad w where
  extract :: w a -> a
  extend :: w a -> (w a -> b) -> w b

Compose.hs

{-# LANGUAGE MultiParamTypeClasses #-}

module Compose where
import Identity
import MonoidalCategory2

newtype Compose f g a = Compose { decompose :: (f (g a)) }

instance MonoidalCategory2 Compose Id where
  λ = runIdentity . decompose
  λ' = Compose . Id
  ρ = fmap runIdentity . decompose
  ρ' = Compose . fmap Id
  α = Compose . fmap Compose . decompose . decompose
  α' = Compose . Compose . fmap decompose . decompose

Coyoneda.hs

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeOperators #-}

module Coyoneda where
import Nat

data Coyoneda f a = forall x. Coyoneda (x -> a) (f x)
instance Functor (Coyoneda f) where
  fmap ab (Coyoneda xa fx) = Coyoneda (ab . xa) fx

fromCoyoneda :: Functor f => Coyoneda f ~> f
fromCoyoneda (Coyoneda xa fx) = xa <$> fx

toCoyoneda :: f ~> Coyoneda f
toCoyoneda fa = Coyoneda id fa

Density.hs

{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, DeriveFunctor #-}

module Density where
import Adjunctions
import Comonad
import Compose
import Identity
import Lan
import MonoidalCategory2
import Nat

newtype Density k a = Density (Lan k k a)
  deriving Functor

instance Functor k => Comonad (Density k) where
  extract (Density (Lan ka k)) = ka k
  extend (Density (Lan ka k)) kakb = Density (Lan kb k)
    where kb k' = kakb (Density (Lan ka k'))

class Abs_Lan k d where
  abs_Lan :: Compose f (Lan k d) ~> Lan k (Compose f d)

instance (Functor k, Abs_Lan k Id) => k ⊣ (Lan k Id) where
  unit = decompose . unit_Lan . Id
  counit = extract . Density . (rotate_Lan ρ) . abs_Lan . Compose

Identity.hs

{-# LANGUAGE DeriveFunctor #-}

module Identity where

newtype Id a = Id { runIdentity :: a }
  deriving Functor

Lan.hs

{-# LANGUAGE ExistentialQuantification, TypeOperators, RankNTypes #-}

module Lan where
import Adjunctions
import Compose
import Coyoneda
import Identity
import Nat

data Lan k d a = forall i. Lan (k i -> a) (d i)
instance Functor (Lan k d) where
  fmap ab (Lan ka d) = Lan (ab . ka) d
unit_Lan :: d ~> Compose (Lan k d) k
unit_Lan da = Compose (Lan id da)
rotate_Lan :: (d ~> d') -> Lan k d ~> Lan k d'
rotate_Lan nat (Lan ka d) = Lan ka (nat d)

lanToCoyoneda :: Lan Id d ~> Coyoneda d
lanToCoyoneda (Lan idia di) = Coyoneda (idia . Id) di
coyonedaToLan :: Coyoneda d ~> Lan Id d
coyonedaToLan (Coyoneda xa fx) = Lan (xa . runIdentity) fx

-- K ⊣ Lan_K Id
adjointToLan :: (l ⊣ r) => r ~> Lan l Id
adjointToLan = Lan counit . Id
lanToAdjoint :: (l ⊣ r) => Lan l Id ~> r
lanToAdjoint (Lan lia idi) = fmap lia . unit . runIdentity $ idi

MonoidalCategory2.hs

{-# LANGUAGE TypeOperators, MultiParamTypeClasses #-}

module MonoidalCategory2 where
import Nat

class Functor i => MonoidalCategory2 tensor i where
  λ :: Functor f => (i `tensor` f) ~> f
  λ' :: Functor f => f ~> (i `tensor` f)
  ρ :: Functor f => (f `tensor` i) ~> f
  ρ' :: Functor f => f ~> (f `tensor` i)
  α :: (Functor f, Functor g, Functor h) =>
    ((f `tensor` g) `tensor` h) ~> (f `tensor` (g `tensor` h))
  α' :: (Functor f, Functor g, Functor h) =>
    (f `tensor` (g `tensor` h)) ~> ((f `tensor` g) `tensor` h)

Nat.hs

{-# LANGUAGE RankNTypes, TypeOperators #-}

module Nat where

type f ~> g = forall a. f a -> g a

Ran.hs

{-# LANGUAGE RankNTypes, TypeOperators, DeriveFunctor #-}

module Ran where
import Adjunctions
import Compose
import Identity
import Nat
import Yoneda

newtype Ran k d a = Ran (forall i. (a -> k i) -> d i)
  deriving Functor
counit_Ran :: Compose (Ran k d) k ~> d
counit_Ran (Compose (Ran f)) = f id
rotate_Ran :: (d ~> d') -> Ran k d ~> Ran k d'
rotate_Ran nat (Ran akd) = Ran (nat . akd)

ranToYoneda :: Functor d => Ran Id d ~> Yoneda d
ranToYoneda (Ran aididi) = Yoneda (<$> aididi Id)
yonedaToRan :: Functor d => Yoneda d ~> Ran Id d
yonedaToRan yo = Ran (\aidi -> runIdentity . aidi <$> fromYoneda yo)

-- Ran_K Id ⊣ K
adjointToRan :: (l ⊣ r) => l ~> Ran r Id
adjointToRan l = Ran (\ari -> Id . counit . fmap ari $ l)
ranToAdjoint :: (l ⊣ r) => Ran r Id ~> l
ranToAdjoint (Ran arid) = runIdentity $ arid unit

Yoneda.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DeriveFunctor #-}

module Yoneda where
import Nat

newtype Yoneda f a = Yoneda { runYoneda :: forall x. (a -> x) -> f x }
  deriving Functor

fromYoneda :: Yoneda f ~> f
fromYoneda = ($id) . runYoneda

toYoneda :: Functor f => f ~> Yoneda f
toYoneda fa = Yoneda (`fmap` fa)