{-# LANGUAGE Rank2Types, GADTs #-} {-# LANGUAGE CPP #-} #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Trustworthy #-} #endif ------------------------------------------------------------------------------------------- -- | -- Module : Data.Functor.KanExtension -- Copyright : 2008-2011 Edward Kmett -- License : BSD -- -- Maintainer : Edward Kmett -- Stability : experimental -- Portability : rank 2 types -- ------------------------------------------------------------------------------------------- module Data.Functor.KanExtension where import Data.Functor.Identity import Data.Functor.Adjunction import Data.Functor.Composition import Data.Functor.Apply import Control.Applicative newtype Ran g h a = Ran { runRan :: forall b. (a -> g b) -> h b } instance Functor (Ran g h) where fmap f m = Ran (\k -> runRan m (k . f)) -- | 'toRan' and 'fromRan' witness a higher kinded adjunction. from @(`'Compose'` g)@ to @'Ran' g@ toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b toRan s t = Ran (s . flip fmap t) fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b fromRan s = flip runRan id . s composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a composeRan r = Ran (\f -> runRan (runRan r (decompose . f)) id) decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) a decomposeRan r = Ran (\f -> Ran (\g -> runRan r (compose . fmap g . f))) adjointToRan :: Adjunction f g => f a -> Ran g Identity a adjointToRan f = Ran (\a -> Identity $ rightAdjunct a f) ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a ranToAdjoint r = runIdentity (runRan r unit) ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f a) ranToComposedAdjoint r = runRan r unit composedAdjointToRan :: (Adjunction f g, Functor h) => h (f a) -> Ran g h a composedAdjointToRan f = Ran (\a -> fmap (rightAdjunct a) f) data Lan g h a where Lan :: (g b -> a) -> h b -> Lan g h a -- 'fromLan' and 'toLan' witness a (higher kinded) adjunction between @'Lan' g@ and @(`Compose` g)@ toLan :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f b toLan s (Lan f v) = fmap f (s v) fromLan :: (forall a. Lan g h a -> f a) -> h b -> f (g b) fromLan s = s . Lan id instance Functor (Lan f g) where fmap f (Lan g h) = Lan (f . g) h instance (Functor g, Apply h) => Apply (Lan g h) where Lan kxf x <.> Lan kya y = Lan (\k -> kxf (fmap fst k) (kya (fmap snd k))) ((,) <$> x <.> y) instance (Functor g, Applicative h) => Applicative (Lan g h) where pure a = Lan (const a) (pure ()) Lan kxf x <*> Lan kya y = Lan (\k -> kxf (fmap fst k) (kya (fmap snd k))) (liftA2 (,) x y) adjointToLan :: Adjunction f g => g a -> Lan f Identity a adjointToLan = Lan counit . Identity lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a lanToAdjoint (Lan f v) = leftAdjunct f (runIdentity v) -- | 'lanToComposedAdjoint' and 'composedAdjointToLan' witness the natural isomorphism between @Lan f h@ and @Compose h g@ given @f -| g@ lanToComposedAdjoint :: (Functor h, Adjunction f g) => Lan f h a -> h (g a) lanToComposedAdjoint (Lan f v) = fmap (leftAdjunct f) v composedAdjointToLan :: Adjunction f g => h (g a) -> Lan f h a composedAdjointToLan = Lan counit -- | 'composeLan' and 'decomposeLan' witness the natural isomorphism from @Lan f (Lan g h)@ and @Lan (f `o` g) h@ composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h a composeLan (Lan f (Lan g h)) = Lan (f . fmap g . decompose) h decomposeLan :: Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) a decomposeLan (Lan f h) = Lan (f . compose) (Lan id h)