module Control.Functor.KanExtension
(
Ran(..)
, toRan, fromRan
, adjointToRan, ranToAdjoint
, ranToComposedAdjoint, composedAdjointToRan
, composeRan, decomposeRan
, Lan(..)
, toLan, fromLan
, adjointToLan, lanToAdjoint
, composeLan, decomposeLan
, lanToComposedAdjoint, composedAdjointToLan
) where
import Prelude hiding (abs)
import Control.Functor.Composition
import Control.Functor.Extras
import Control.Functor.Pointed ()
import Control.Functor.HigherOrder
import Control.Functor.Adjunction
import Control.Monad.Identity
newtype Ran g h a = Ran { runRan :: forall b. (a -> g b) -> h b }
toRan :: (Composition o, Functor k) => (k `o` g :~> h) -> k :~> Ran g h
toRan s t = Ran (s . compose . flip fmap t)
fromRan :: Composition o => (k :~> Ran g h) -> (k `o` g) :~> h
fromRan s = flip runRan id . s . decompose
instance HFunctor (Ran g) where
hfmap f (Ran m) = Ran (f . m)
ffmap f m = Ran (\k -> runRan m (k . f))
instance Functor (Ran g h) where
fmap f m = Ran (\k -> runRan m (k . f))
composeRan :: Composition o => Ran f (Ran g h) :~> Ran (f `o` g) h
composeRan r = Ran (\f -> runRan (runRan r (decompose . f)) id)
decomposeRan :: (Functor f, Composition o) => Ran (f `o` g) h :~> Ran f (Ran g h)
decomposeRan r = Ran (\f -> Ran (\g -> runRan r (compose . fmap g . f)))
adjointToRan :: Adjunction f g => f :~> Ran g Identity
adjointToRan f = Ran (\a -> Identity $ rightAdjunct a f)
ranToAdjoint :: Adjunction f g => Ran g Identity :~> f
ranToAdjoint r = runIdentity (runRan r unit)
ranToComposedAdjoint :: (Composition o, Adjunction f g) => Ran g h :~> (h `o` f)
ranToComposedAdjoint r = compose (runRan r unit)
composedAdjointToRan :: (Functor h, Composition o, Adjunction f g) => (h `o` f) :~> Ran g h
composedAdjointToRan f = Ran (\a -> fmap (rightAdjunct a) (decompose f))
data Lan g h a = forall b. Lan (g b -> a) (h b)
toLan :: (Composition o, Functor f) => (h :~> (f `o` g)) -> Lan g h :~> f
toLan s (Lan f v) = fmap f . decompose $ s v
fromLan :: Composition o => (Lan g h :~> f) -> h :~> (f `o` g)
fromLan s = compose . s . Lan id
instance Functor g => HFunctor (Lan g) where
ffmap f (Lan g h) = Lan (f . g) h
hfmap f (Lan g h) = Lan g (f h)
instance Functor (Lan f g) where
fmap f (Lan g h) = Lan (f . g) h
adjointToLan :: Adjunction f g => g :~> Lan f Identity
adjointToLan = Lan counit . Identity
lanToAdjoint :: Adjunction f g => Lan f Identity :~> g
lanToAdjoint (Lan f v) = leftAdjunct f (runIdentity v)
lanToComposedAdjoint :: (Functor h, Composition o, Adjunction f g) => Lan f h :~> (h `o` g)
lanToComposedAdjoint (Lan f v) = compose (fmap (leftAdjunct f) v)
composedAdjointToLan :: (Composition o, Adjunction f g) => (h `o` g) :~> Lan f h
composedAdjointToLan = Lan counit . decompose
composeLan :: (Functor f, Composition o) => Lan f (Lan g h) :~> Lan (f `o` g) h
composeLan (Lan f (Lan g h)) = Lan (f . fmap g . decompose) h
decomposeLan :: Composition o => Lan (f `o` g) h :~> Lan f (Lan g h)
decomposeLan (Lan f h) = Lan (f . compose) (Lan id h)