kan-extensions 3.4 → 3.5

raw patch · 16 files changed

+1135/−585 lines, 16 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +10/−0
• LICENSE +1/−1
• kan-extensions.cabal +10/−7
• src/Control/Comonad/Density.hs +50/−4
• src/Control/Monad/Co.hs +18/−5
• src/Control/Monad/Codensity.hs +125/−16
• src/Data/Functor/Contravariant/Yoneda/Reduction.hs +70/−0
• src/Data/Functor/Kan/Lan.hs +114/−0
• src/Data/Functor/Kan/Lift.hs +151/−0
• src/Data/Functor/Kan/Ran.hs +167/−0
• src/Data/Functor/Kan/Rift.hs +191/−0
• src/Data/Functor/KanExtension.hs +0/−96
• src/Data/Functor/KanLift.hs +0/−284
• src/Data/Functor/Yoneda.hs +8/−1
• src/Data/Functor/Yoneda/Contravariant.hs +0/−171
• src/Data/Functor/Yoneda/Reduction.hs +220/−0

@@ -1,3 +1,13 @@+3.5+---+* More combinators for `Rift`/`Lift`.+* Added combinators for working with representable functors rather than just adjoint functors.+* Split `Data.Functor.KanExtension` into `Data.Functor.Kan.Ran` and `Data.Functor.Kan.Lan`+* Split `Data.Functor.KanLift` into `Data.Functor.Kan.Rift` and `Data.Functor.Kan.Lift`+* Moved from `Data.Functor.Yoneda.Contravariant` to `Data.Functor.Yoneda.Reduction` adopting terminology from Todd Trimble.+* Added various missing isomorphisms.+* Greatly improved the Haddocks for this package stating laws and derivations where we can (especially for 'Rift' and 'Ran').+ 3.3 --- * Rift is now `Applicative`. Added `rap`.

@@ -1,4 +1,4 @@-Copyright 2011 Edward Kmett+Copyright 2008-2013 Edward Kmett  All rights reserved. 

@@ -1,6 +1,6 @@ name:          kan-extensions category:      Data Structures, Monads, Comonads, Functors-version:       3.4+version:       3.5 license:       BSD3 cabal-version: >= 1.6 license-file:  LICENSE@@ -9,9 +9,9 @@ stability:     provisional homepage:      http://github.com/ekmett/kan-extensions/ bug-reports:   http://github.com/ekmett/kan-extensions/issues-copyright:     Copyright (C) 2011-2013 Edward A. Kmett-synopsis:      Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads-description:   Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads+copyright:     Copyright (C) 2008-2013 Edward A. Kmett+synopsis:      Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads+description:   Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads build-type:    Simple  extra-source-files:@@ -62,10 +62,13 @@     Control.Comonad.Density     Control.Monad.Co     Control.Monad.Codensity-    Data.Functor.KanExtension-    Data.Functor.KanLift+    Data.Functor.Contravariant.Yoneda.Reduction+    Data.Functor.Kan.Lan+    Data.Functor.Kan.Lift+    Data.Functor.Kan.Ran+    Data.Functor.Kan.Rift     Data.Functor.Yoneda-    Data.Functor.Yoneda.Contravariant+    Data.Functor.Yoneda.Reduction    ghc-options: -Wall 

@@ -13,15 +13,19 @@ -- Stability   :  experimental -- Portability :  non-portable (GADTs, MPTCs) ----- The density comonad for a functor. aka the comonad generated by a functor--- The ''density'' term dates back to Dubuc''s 1974 thesis. The term--- ''monad genererated by a functor'' dates back to 1972 in Street''s+-- The 'Density' 'Comonad' for a 'Functor' (aka the 'Comonad generated by a 'Functor')+-- The 'Density' term dates back to Dubuc''s 1974 thesis. The term+-- '''Monad' genererated by a 'Functor''' dates back to 1972 in Street''s -- ''Formal Theory of Monads''.+--+-- The left Kan extension of a 'Functor' along itself (@'Lan' f f@) forms a 'Comonad'. This is+-- that 'Comonad'. ---------------------------------------------------------------------------- module Control.Comonad.Density   ( Density(..)   , liftDensity   , densityToAdjunction, adjunctionToDensity+  , densityToLan, lanToDensity   ) where  import Control.Applicative@@ -30,38 +34,80 @@ import Data.Functor.Apply import Data.Functor.Adjunction import Data.Functor.Extend+import Data.Functor.Kan.Lan  data Density k a where   Density :: (k b -> a) -> k b -> Density k a  instance Functor (Density f) where   fmap f (Density g h) = Density (f . g) h+  {-# INLINE fmap #-}  instance Extend (Density f) where   duplicated (Density f ws) = Density (Density f) ws+  {-# INLINE duplicated #-}  instance Comonad (Density f) where   duplicate (Density f ws) = Density (Density f) ws+  {-# INLINE duplicate #-}   extract (Density f a) = f a+  {-# INLINE extract #-}  instance ComonadTrans Density where   lower (Density f c) = extend f c+  {-# INLINE lower #-}  instance Apply f => Apply (Density f) where   Density kxf x <.> Density kya y =     Density (\k -> kxf (fmap fst k) (kya (fmap snd k))) ((,) <$> x <.> y)+  {-# INLINE (<.>) #-}  instance Applicative f => Applicative (Density f) where   pure a = Density (const a) (pure ())+  {-# INLINE pure #-}   Density kxf x <*> Density kya y =     Density (\k -> kxf (fmap fst k) (kya (fmap snd k))) (liftA2 (,) x y)+  {-# INLINE (<*>) #-} --- | The natural isomorphism between a comonad w and the comonad generated by w (forwards).+-- | The natural transformation from a @'Comonad' w@ to the 'Comonad' generated by @w@ (forwards).+--+-- This is merely a right-inverse (section) of 'lower', rather than a full inverse.+--+-- @+-- 'lower' . 'liftDensity' ≡ 'id'+-- @ liftDensity :: Comonad w => w a -> Density w a liftDensity = Density extract+{-# INLINE liftDensity #-} +-- | The Density 'Comonad' of a left adjoint is isomorphic to the 'Comonad' formed by that 'Adjunction'.+--+-- This isomorphism is witnessed by 'densityToAdjunction' and 'adjunctionToDensity'.+--+-- @+-- 'densityToAdjunction' . 'adjunctionToDensity' ≡ 'id'+-- 'adjunctionToDensity' . 'densityToAdjunction' ≡ 'id'+-- @ densityToAdjunction :: Adjunction f g => Density f a -> f (g a) densityToAdjunction (Density f v) = fmap (leftAdjunct f) v+{-# INLINE densityToAdjunction #-}  adjunctionToDensity :: Adjunction f g => f (g a) -> Density f a adjunctionToDensity = Density counit+{-# INLINE adjunctionToDensity #-}++-- | The 'Density' 'Comonad' of a 'Functor' @f@ is obtained by taking the left Kan extension+-- ('Lan') of @f@ along itself. This isomorphism is witnessed by 'lanToDensity' and 'densityToLan'+--+-- @+-- 'lanToDensity' . 'densityToLan' ≡ 'id'+-- 'densityToLan' . 'lanToDensity' ≡ 'id'+-- @+lanToDensity :: Lan f f a -> Density f a+lanToDensity (Lan f v) = Density f v+{-# INLINE lanToDensity #-}++densityToLan :: Density f a -> Lan f f a+densityToLan (Density f v) = Lan f v+{-# INLINE densityToLan #-}+

@@ -23,12 +23,25 @@ -- -- <http://comonad.com/reader/2011/monads-from-comonads/> ----- 'Co' and 'CoT' just special cases of the general notion of a--- Right Kan lift.+-- 'Co' can be viewed as a right Kan lift along a 'Comonad'. ----- TODO: We could consider unifying the definition of 'CoT' and 'Rift', but--- 'Rift' f f also forms a Codensity-like 'Monad', so there is a reasonable--- case for keeping them separate.+-- In general you can \"sandwich\" a monad in between two halves of an adjunction.+-- That is to say, if you have an adjunction @F -| G : C -> D @ then not only does @GF@+-- form a monad, but @GMF@ forms a monad for @M@ a monad in @D@. Therefore if we+-- have an adjunction @F -| G : Hask -> Hask^op@ then we can lift a 'Comonad' in @Hask@+-- which is a 'Monad' in @Hask^op@ to a 'Monad' in 'Hask'.+--+-- For any @r@, the 'Contravariant' functor / presheaf @(-> r)@ :: Hask^op -> Hask is adjoint to the \"same\"+-- 'Contravariant' functor @(-> r) :: Hask -> Hask^op@. So we can sandwhich a+-- Monad in Hask^op in the middle to obtain @w (a -> r-) -> r+@, and then take a coend over+-- @r@ to obtain @forall r. w (a -> r) -> r@. This gives rise to 'Co'. If we observe that+-- we didn't care what the choices we made for @r@ were to finish this construction, we can+-- upgrade to @forall r. w (a -> m r) -> m r@ in a manner similar to how @ContT@ is constructed+-- yielding 'CoT'.+--+-- We could consider unifying the definition of 'Co' and 'Rift', but+-- there are many other arguments for which 'Rift' can form a 'Monad', and this+-- wouldn't give rise to 'CoT'. ---------------------------------------------------------------------------- module Control.Monad.Co   (

@@ -1,5 +1,8 @@-{-# LANGUAGE Rank2Types, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-} {-# LANGUAGE CPP #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-} #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Trustworthy #-} #endif@@ -10,7 +13,7 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Control.Monad.Codensity--- Copyright   :  (C) 2008-2011 Edward Kmett+-- Copyright   :  (C) 2008-2013 Edward Kmett -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  Edward Kmett <ekmett@gmail.com>@@ -21,58 +24,86 @@ module Control.Monad.Codensity   ( Codensity(..)   , lowerCodensity-  , codensityToAdjunction-  , adjunctionToCodensity+  , codensityToAdjunction, adjunctionToCodensity+  , codensityToRan, ranToCodensity+  , codensityToComposedRep, composedRepToCodensity   , improve   ) where  import Control.Applicative+import Control.Concurrent.Speculation+import Control.Concurrent.Speculation.Class+import Control.Monad (ap, MonadPlus(..))+import Control.Monad.Free+import Control.Monad.IO.Class import Control.Monad.Reader.Class import Control.Monad.State.Class-import Control.Monad.Free.Class-import Control.Monad.Free-import Control.Monad (ap, MonadPlus(..))+import Control.Monad.Trans.Class import Data.Functor.Adjunction import Data.Functor.Apply+import Data.Functor.Kan.Ran import Data.Functor.Plus-import Control.Monad.Trans.Class-import Control.Monad.IO.Class-import Control.Concurrent.Speculation-import Control.Concurrent.Speculation.Class+import Data.Functor.Representable+import Data.Key -newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }+-- |+-- @'Codensity' f@ is the Monad generated by taking the right Kan extension+-- of any 'Functor' @f@ along itself (@Ran f f@).+--+-- This can often be more \"efficient\" to construct than @f@ itself using+-- repeated applications of @(>>=)@.+--+-- See \"Asymptotic Improvement of Computations over Free Monads\" by Janis+-- Voightländer for more information about this type.+--+-- <http://www.iai.uni-bonn.de/~jv/mpc08.pdf>+newtype Codensity m a = Codensity+  { runCodensity :: forall b. (a -> m b) -> m b+  }  instance MonadSpec (Codensity m) where   specByM f g a = Codensity $ \k -> specBy f g k a+  {-# INLINE specByM #-} #if !(MIN_VERSION_speculation(1,5,0))   specByM' f g a = Codensity $ \k -> specBy' f g k a+  {-# INLINE specByM' #-} #endif  instance Functor (Codensity k) where   fmap f (Codensity m) = Codensity (\k -> m (k . f))+  {-# INLINE fmap #-}  instance Apply (Codensity f) where   (<.>) = ap+  {-# INLINE (<.>) #-}  instance Applicative (Codensity f) where   pure x = Codensity (\k -> k x)+  {-# INLINE pure #-}   (<*>) = ap+  {-# INLINE (<*>) #-}  instance Monad (Codensity f) where   return x = Codensity (\k -> k x)+  {-# INLINE return #-}   m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))+  {-# INLINE (>>=) #-}  instance MonadIO m => MonadIO (Codensity m) where-  liftIO = lift . liftIO +  liftIO = lift . liftIO+  {-# INLINE liftIO #-}  instance MonadTrans Codensity where   lift m = Codensity (m >>=)+  {-# INLINE lift #-}  instance Alt v => Alt (Codensity v) where   Codensity m <!> Codensity n = Codensity (\k -> m k <!> n k)+  {-# INLINE (<!>) #-}  instance Plus v => Plus (Codensity v) where   zero = Codensity (const zero)+  {-# INLINE zero #-}  {- instance Plus v => Alternative (Codensity v) where@@ -85,32 +116,110 @@ -}  instance Alternative v => Alternative (Codensity v) where-  empty                         = Codensity (\_ -> empty)+  empty = Codensity (\_ -> empty)+  {-# INLINE empty #-}   Codensity m <|> Codensity n = Codensity (\k -> m k <|> n k)+  {-# INLINE (<|>) #-}  instance MonadPlus v => MonadPlus (Codensity v) where-  mzero                             = Codensity (\_ -> mzero)+  mzero = Codensity (\_ -> mzero)+  {-# INLINE mzero #-}   Codensity m `mplus` Codensity n = Codensity (\k -> m k `mplus` n k)+  {-# INLINE mplus #-} +-- |+-- This serves as the *left*-inverse (retraction) of 'lift'.+--+--+-- @+-- 'lowerCodensity . lift' ≡ 'id'+-- @+--+-- In general this is not a full 2-sided inverse, merely a retraction, as+-- @'Codensity' m@ is often considerably "larger" than @m@.+--+-- e.g. @'Codensity' ((->) s)) a ~ forall r. (a -> s -> r) -> s -> r@+-- could support a full complement of @'MonadState' s@ actions, while @(->) s@+-- is limited to @'MonadReader' s@ actions. lowerCodensity :: Monad m => Codensity m a -> m a lowerCodensity a = runCodensity a return+{-# INLINE lowerCodensity #-} +-- | The 'Codensity' monad of a right adjoint is isomorphic to the+-- monad obtained from the 'Adjunction'.+--+-- @+-- 'codensityToAdjunction' . 'adjunctionToCodensity' ≡ 'id'+-- 'adjunctionToCodensity' . 'codensityToAdjunction' ≡ 'id'+-- @ codensityToAdjunction :: Adjunction f g => Codensity g a -> g (f a) codensityToAdjunction r = runCodensity r unit+{-# INLINE codensityToAdjunction #-}  adjunctionToCodensity :: Adjunction f g => g (f a) -> Codensity g a adjunctionToCodensity f = Codensity (\a -> fmap (rightAdjunct a) f)+{-# INLINE adjunctionToCodensity #-} +-- | The 'Codensity' monad of a representable 'Functor' is isomorphic to the+-- monad obtained from the 'Adjunction' for which that 'Functor' is the right+-- adjoint.+--+-- @+-- 'codensityToComposedRep' . 'composedRepToCodensity' ≡ 'id'+-- 'composedRepToCodensity' . 'codensityToComposedRep' ≡ 'id'+-- @+--+-- @+-- codensityToComposedRep = 'ranToComposedRep' . 'codensityToRan'+-- @++codensityToComposedRep :: Representable u => Codensity u a -> u (Key u, a)+codensityToComposedRep (Codensity f) = f (\a -> tabulate $ \e -> (e, a))+{-# INLINE codensityToComposedRep #-}++-- |+--+-- @+-- 'composedRepToCodensity' = 'ranToCodensity' . 'composedRepToRan'+-- @+composedRepToCodensity :: (Representable u, Functor h) => u (Key u, a) -> Codensity u a+composedRepToCodensity hfa = Codensity $ \k -> fmap (\(e, a) -> index (k a) e) hfa+{-# INLINE composedRepToCodensity #-}++-- | The 'Codensity' 'Monad' of a 'Functor' @g@ is the right Kan extension ('Ran')+-- of @g@ along itself.+--+-- @+-- 'codensityToRan' . 'ranToCodensity' ≡ 'id'+-- 'ranToCodensity' . 'codensityToRan' ≡ 'id'+-- @+codensityToRan :: Codensity g a -> Ran g g a+codensityToRan (Codensity m) = Ran m+{-# INLINE codensityToRan #-}++ranToCodensity :: Ran g g a -> Codensity g a+ranToCodensity (Ran m) = Codensity m+{-# INLINE ranToCodensity #-}+ instance (Functor f, MonadFree f m) => MonadFree f (Codensity m) where   wrap t = Codensity (\h -> wrap (fmap (\p -> runCodensity p h) t))+  {-# INLINE wrap #-}  instance MonadReader r m => MonadState r (Codensity m) where   get = Codensity (ask >>=)+  {-# INLINE get #-}   put s = Codensity (\k -> local (const s) (k ()))+  {-# INLINE put #-}  -- | Right associate all binds in a computation that generates a free monad+-- -- This can improve the asymptotic efficiency of the result, while preserving -- semantics.+--+-- See \"Asymptotic Improvement of Computations over Free Monads\" by Janis+-- Voightländer for more information about this combinator.+--+-- <http://www.iai.uni-bonn.de/~jv/mpc08.pdf> improve :: Functor f => (forall m. MonadFree f m => m a) -> Free f a improve m = lowerCodensity m-+{-# INLINE improve #-}

@@ -0,0 +1,70 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UndecidableInstances #-}+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702+{-# LANGUAGE Trustworthy #-}+#endif+-----------------------------------------------------------------------------+-- |+-- Copyright   :  (C) 2013 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  provisional+-- Portability :  GADTs, TFs, MPTCs+--+-- Yoneda Reduction of presheafs+--+-- <http://ncatlab.org/nlab/show/Yoneda+reduction>+--+----------------------------------------------------------------------------+module Data.Functor.Contravariant.Yoneda.Reduction+  ( Yoneda(..)+  , liftYoneda+  , lowerYoneda+  ) where++import Control.Arrow+import Data.Functor.Contravariant+import Data.Functor.Contravariant.Adjunction+import Data.Functor.Contravariant.Representable++type instance Value (Yoneda f) = Value f++-- | A 'Contravariant' functor (aka presheaf) suitable for Yoneda reduction.+data Yoneda f a where+  Yoneda :: (a -> b) -> f b -> Yoneda f a++instance Contravariant (Yoneda f) where+  contramap f (Yoneda g m) = Yoneda (g.f) m+  {-# INLINE contramap #-}++instance Valued f => Valued (Yoneda f) where+  contramapWithValue beav (Yoneda ac fc) = Yoneda (left ac . beav) (contramapWithValue id fc)+  {-# INLINE contramapWithValue #-}++instance Coindexed f => Coindexed (Yoneda f) where+  coindex (Yoneda ab fb) a = coindex fb (ab a)+  {-# INLINE coindex #-}++instance Representable f => Representable (Yoneda f) where+  contrarep = liftYoneda . contrarep+  {-# INLINE contrarep #-}++instance Adjunction f g => Adjunction (Yoneda f) (Yoneda g) where+  leftAdjunct f = liftYoneda . leftAdjunct (lowerYoneda . f)+  {-# INLINE leftAdjunct #-}+  rightAdjunct f = liftYoneda . rightAdjunct (lowerYoneda . f)+  {-# INLINE rightAdjunct #-}++-- | Yoneda "expansion" of a presheaf+liftYoneda :: f a -> Yoneda f a+liftYoneda = Yoneda id+{-# INLINE liftYoneda #-}++-- | Yoneda reduction on a presheaf+lowerYoneda :: Contravariant f => Yoneda f a -> f a+lowerYoneda (Yoneda f m) = contramap f m+{-# INLINE lowerYoneda #-}

@@ -0,0 +1,114 @@+{-# LANGUAGE Rank2Types, GADTs #-}+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702+{-# LANGUAGE Trustworthy #-}+#endif+-------------------------------------------------------------------------------------------+-- |+-- Copyright 	: 2008-2013 Edward Kmett+-- License	: BSD+--+-- Maintainer	: Edward Kmett <ekmett@gmail.com>+-- Stability	: experimental+-- Portability	: rank 2 types+--+-- Left Kan Extensions+-------------------------------------------------------------------------------------------+module Data.Functor.Kan.Lan+  (+  -- * Left Kan Extensions+    Lan(..)+  , toLan, fromLan+  , glan+  , composeLan, decomposeLan+  , adjointToLan, lanToAdjoint+  , composedAdjointToLan, lanToComposedAdjoint+  ) where++import Control.Applicative+import Data.Functor.Adjunction+import Data.Functor.Apply+import Data.Functor.Composition+import Data.Functor.Identity++-- | The left Kan extension of a 'Functor' @h@ along a 'Functor' @g@.+data Lan g h a where+  Lan :: (g b -> a) -> h b -> Lan g h a++instance Functor (Lan f g) where+  fmap f (Lan g h) = Lan (f . g) h+  {-# INLINE fmap #-}++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)+  {-# INLINE (<.>) #-}++instance (Functor g, Applicative h) => Applicative (Lan g h) where+  pure a = Lan (const a) (pure ())+  {-# INLINE pure #-}+  Lan kxf x <*> Lan kya y =+    Lan (\k -> kxf (fmap fst k) (kya (fmap snd k))) (liftA2 (,) x y)+  {-# INLINE (<*>) #-}++-- | The universal property of a left Kan extension.+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)+{-# INLINE toLan #-}++-- | 'fromLan' and 'toLan' witness a (higher kinded) adjunction between @'Lan' g@ and @(`Compose` g)@+--+-- @+-- 'toLan' . 'fromLan' ≡ 'id'+-- 'fromLan' . 'toLan' ≡ 'id'+-- @+fromLan :: (forall a. Lan g h a -> f a) -> h b -> f (g b)+fromLan s = s . glan+{-# INLINE fromLan #-}++-- |+--+-- @+-- 'adjointToLan' . 'lanToAdjoint' ≡ 'id'+-- 'lanToAdjoint' . 'adjointToLan' ≡ 'id'+-- @+adjointToLan :: Adjunction f g => g a -> Lan f Identity a+adjointToLan = Lan counit . Identity+{-# INLINE adjointToLan #-}++lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a+lanToAdjoint (Lan f v) = leftAdjunct f (runIdentity v)+{-# INLINE lanToAdjoint #-}++-- | 'lanToComposedAdjoint' and 'composedAdjointToLan' witness the natural isomorphism between @Lan f h@ and @Compose h g@ given @f -| g@+--+-- @+-- 'composedAdjointToLan' . 'lanToComposedAdjoint' ≡ 'id'+-- 'lanToComposedAdjoint' . 'composedAdjointToLan' ≡ 'id'+-- @+lanToComposedAdjoint :: (Functor h, Adjunction f g) => Lan f h a -> h (g a)+lanToComposedAdjoint (Lan f v) = fmap (leftAdjunct f) v+{-# INLINE lanToComposedAdjoint #-}++composedAdjointToLan :: Adjunction f g => h (g a) -> Lan f h a+composedAdjointToLan = Lan counit+{-# INLINE composedAdjointToLan #-}++-- | 'composeLan' and 'decomposeLan' witness the natural isomorphism from @Lan f (Lan g h)@ and @Lan (f `o` g) h@+--+-- @+-- 'composeLan' . 'decomposeLan' ≡ 'id'+-- 'decomposeLan' . 'composeLan' ≡ 'id'+-- @+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+{-# INLINE composeLan #-}++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)+{-# INLINE decomposeLan #-}++-- | This is the natural transformation that defines a Left Kan extension.+glan :: h a -> Lan g h (g a)+glan = Lan id+{-# INLINE glan #-}

@@ -0,0 +1,151 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE GADTs #-}++#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702+{-# LANGUAGE Trustworthy #-}+#endif+-------------------------------------------------------------------------------------------+-- |+-- Copyright 	: 2013 Edward Kmett and Dan Doel+-- License	: BSD+--+-- Maintainer	: Edward Kmett <ekmett@gmail.com>+-- Stability	: experimental+-- Portability	: rank N types+--+-- Left Kan lifts for functors over Hask, wherever they exist.+--+-- <http://ncatlab.org/nlab/show/Kan+lift>+-------------------------------------------------------------------------------------------+module Data.Functor.Kan.Lift+  (+  -- * Left Kan lifts+    Lift(..)+  , toLift, fromLift, glift+  , composeLift, decomposeLift+  , adjointToLift, liftToAdjoint+  , liftToComposedAdjoint, composedAdjointToLift+  , repToLift, liftToRep+  , liftToComposedRep, composedRepToLift+  ) where++import Data.Copointed+import Data.Functor.Adjunction+import Data.Functor.Composition+import Data.Functor.Compose+import Data.Functor.Identity+import Data.Functor.Representable+import Data.Key++-- * Left Kan Lift++-- |+-- > f => g . Lift g f+-- > (forall z. f => g . z) -> Lift g f => z -- couniversal+--+-- Here we use the universal property directly as how we extract from our definition of 'Lift'.+newtype Lift g f a = Lift { runLift :: forall z. Functor z => (forall x. f x -> g (z x)) -> z a }++instance Functor (Lift g h) where+  fmap f (Lift g) = Lift (fmap f . g)+  {-# INLINE fmap #-}++instance (Functor g, g ~ h) => Copointed (Lift g h) where+  copoint x = runIdentity (runLift x (fmap Identity))+  {-# INLINE copoint #-}++-- |+--+-- @f => g ('Lift' g f a)@+glift :: Adjunction l g => k a -> g (Lift g k a)+glift = leftAdjunct (\lka -> Lift (\k2gz -> rightAdjunct k2gz lka))+{-# INLINE glift #-}++-- | The universal property of 'Lift'+toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z b+toLift = flip runLift+{-# INLINE toLift #-}++-- | When the adjunction exists+--+-- @+-- 'fromLift' . 'toLift' ≡ 'id'+-- 'toLift' . 'fromLift' ≡ 'id'+-- @+fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b)+fromLift f = fmap f . glift+{-# INLINE fromLift #-}++-- |+--+-- @+-- 'composeLift' . 'decomposeLift' = 'id'+-- 'decomposeLift' . 'composeLift' = 'id'+-- @+composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h a+composeLift (Lift m) = Lift $ \h -> m $ decompose . toLift (fmap Compose . decompose . h)+{-# INLINE composeLift #-}++decomposeLift :: (Composition compose, Adjunction l g) => Lift (compose g f) h a -> Lift f (Lift g h) a+decomposeLift (Lift m) = Lift $ \h -> m (compose . fmap h . glift)+{-# INLINE decomposeLift #-}++-- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.+--+-- @+-- 'adjointToLift' . 'liftToAdjoint' ≡ 'id'+-- 'liftToAdjoint' . 'adjointToLift' ≡ 'id'+-- @+adjointToLift :: Adjunction f u => f a -> Lift u Identity a+adjointToLift fa = Lift $ \k -> rightAdjunct (k . Identity) fa+{-# INLINE adjointToLift #-}+++-- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.+liftToAdjoint :: Adjunction f u => Lift u Identity a -> f a+liftToAdjoint = toLift (unit . runIdentity)+{-# INLINE liftToAdjoint #-}++-- |+--+-- @+-- 'repToLift' . 'liftToRep' ≡ 'id'+-- 'liftToRep' . 'repToLift' ≡ 'id'+-- @+repToLift :: Representable u => Key u -> a -> Lift u Identity a+repToLift e a = Lift $ \k -> index (k (Identity a)) e+{-# INLINE repToLift #-}++liftToRep :: Representable u => Lift u Identity a -> (Key u, a)+liftToRep (Lift m) = m $ \(Identity a) -> tabulate $ \e -> (e, a)+{-# INLINE liftToRep #-}++-- | @Lift u h a@ is isomorphic to the post-composition of the left adjoint of @u@ onto @h@ if such a left adjoint exists.+--+-- @+-- 'liftToComposedAdjoint' . 'composedAdjointToLift' ≡ 'id'+-- 'composedAdjointToLift' . 'liftToComposedAdjoint' ≡ 'id'+-- @+liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a)+liftToComposedAdjoint (Lift m) = decompose $ m (leftAdjunct Compose)+{-# INLINE liftToComposedAdjoint #-}++-- | @Lift u h a@ is isomorphic to the post-composition of the left adjoint of @u@ onto @h@ if such a left adjoint exists.+composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h a+composedAdjointToLift = rightAdjunct glift+{-# INLINE composedAdjointToLift #-}++-- |+--+-- @+-- 'liftToComposedRep' . 'composedRepToLift' ≡ 'id'+-- 'composedRepToLift' . 'liftToComposedRep' ≡ 'id'+-- @+liftToComposedRep :: (Functor h, Representable u) => Lift u h a -> (Key u, h a)+liftToComposedRep (Lift m) = decompose $ m $ \h -> tabulate $ \e -> Compose (e, h)+{-# INLINE liftToComposedRep #-}++composedRepToLift :: Representable u => Key u -> h a -> Lift u h a+composedRepToLift e ha = Lift $ \h2uz -> index (h2uz ha) e+{-# INLINE composedRepToLift #-}

@@ -0,0 +1,167 @@+{-# LANGUAGE Rank2Types, GADTs #-}+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702+{-# LANGUAGE Trustworthy #-}+#endif+-------------------------------------------------------------------------------------------+-- |+-- Copyright 	: 2008-2013 Edward Kmett+-- License	: BSD+--+-- Maintainer	: Edward Kmett <ekmett@gmail.com>+-- Stability	: experimental+-- Portability	: rank 2 types+--+-- * Right Kan Extensions+-------------------------------------------------------------------------------------------+module Data.Functor.Kan.Ran+  (+    Ran(..)+  , toRan, fromRan+  , gran+  , composeRan, decomposeRan+  , adjointToRan, ranToAdjoint+  , composedAdjointToRan, ranToComposedAdjoint+  , repToRan, ranToRep+  , composedRepToRan, ranToComposedRep+  ) where++import Data.Functor.Adjunction+import Data.Functor.Composition+import Data.Functor.Identity+import Data.Functor.Representable+import Data.Key++-- | The right Kan extension of a 'Functor' h along a 'Functor' g.+--+-- We can define a right Kan extension in several ways. The definition here is obtained by reading off+-- the definition in of a right Kan extension in terms of an End, but we can derive an equivalent definition+-- from the universal property.+--+-- Given a 'Functor' @h : C -> D@ and a 'Functor' @g : C -> C'@, we want to find extend @h@ /back/ along @g@+-- to give @Ran g h : C' -> C@, such that the natural transformation @'gran' :: Ran g h (g a) -> h a@ exists.+--+-- In some sense this is trying to approximate the inverse of @g@ by using one of+-- its adjoints, because if the adjoint and the inverse both exist, they match!+--+-- > Hask -h-> Hask+-- >   |       ++-- >   g      /+-- >   |    Ran g h+-- >   v    /+-- > Hask -'+--+-- The Right Kan extension is unique (up to isomorphism) by taking this as its universal property.+--+-- That is to say given any @K : C' -> C@ such that we have a natural transformation from @k.g@ to @h@+-- @(forall x. k (g x) -> h x)@ there exists a canonical natural transformation from @k@ to @Ran g h@.+-- @(forall x. k x -> Ran g h x)@.+--+-- We could literally read this off as a valid Rank-3 definition for 'Ran':+--+-- @+-- data Ran' g h a = forall z. 'Functor' z => Ran' (forall x. z (g x) -> h x) (z a)+-- @+--+-- This definition is isomorphic the simpler Rank-2 definition we use below as witnessed by the+--+-- @+-- ranIso1 :: Ran g f x -> Ran' g f x+-- ranIso1 (Ran e) = Ran' e id+--+-- ranIso2 :: Ran' g f x -> Ran g f x+-- ranIso2 (Ran' h z) = Ran $ \k -> h (k <$> z)+-- @+--+-- @+-- ranIso2 (ranIso1 (Ran e)) ≡ -- by definition+-- ranIso2 (Ran' e id) ≡       -- by definition+-- Ran $ \k -> e (k <$> id)    -- by definition+-- Ran $ \k -> e (k . id)      -- f . id = f+-- Ran $ \k -> e k             -- eta reduction+-- Ran e+-- @+--+-- The other direction is left as an exercise for the reader.+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))+  {-# INLINE fmap #-}++-- | The universal property of a right Kan extension.+toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b+toRan s t = Ran (s . flip fmap t)+{-# INLINE toRan #-}++-- | 'toRan' and 'fromRan' witness a higher kinded adjunction. from @(`'Compose'` g)@ to @'Ran' g@+--+-- @+-- 'toRan' . 'fromRan' ≡ 'id'+-- 'fromRan' . 'toRan' ≡ 'id'+-- @+fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b+fromRan s = flip runRan id . s+{-# INLINE fromRan #-}++-- |+-- @+-- 'composeRan' . 'decomposeRan' ≡ 'id'+-- 'decomposeRan' . 'composeRan' ≡ 'id'+-- @+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)+{-# INLINE composeRan #-}++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)))+{-# INLINE decomposeRan #-}++-- |+--+-- @+-- 'adjointToRan' . 'ranToAdjoint' ≡ 'id'+-- 'ranToAdjoint' . 'adjointToRan' ≡ 'id'+-- @+adjointToRan :: Adjunction f g => f a -> Ran g Identity a+adjointToRan f = Ran (\a -> Identity $ rightAdjunct a f)+{-# INLINE adjointToRan #-}++ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a+ranToAdjoint r = runIdentity (runRan r unit)+{-# INLINE ranToAdjoint #-}++-- |+--+-- @+-- 'composedAdjointToRan' . 'ranToComposedAdjoint' ≡ 'id'+-- 'ranToComposedAdjoint' . 'composedAdjointToRan' ≡ 'id'+-- @+ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f a)+ranToComposedAdjoint r = runRan r unit+{-# INLINE ranToComposedAdjoint #-}++composedAdjointToRan :: (Adjunction f g, Functor h) => h (f a) -> Ran g h a+composedAdjointToRan f = Ran (\a -> fmap (rightAdjunct a) f)+{-# INLINE composedAdjointToRan #-}++-- | This is the natural transformation that defines a Right Kan extension.+gran :: Ran g h (g a) -> h a+gran (Ran f) = f id+{-# INLINE gran #-}++repToRan :: Representable u => Key u -> a -> Ran u Identity a+repToRan e a = Ran $ \k -> Identity $ index (k a) e+{-# INLINE repToRan #-}++ranToRep :: Representable u => Ran u Identity a -> (Key u, a)+ranToRep (Ran f) = runIdentity $ f (\a -> tabulate $ \e -> (e, a))+{-# INLINE ranToRep #-}++ranToComposedRep :: Representable u => Ran u h a -> h (Key u, a)+ranToComposedRep (Ran f) = f (\a -> tabulate $ \e -> (e, a))+{-# INLINE ranToComposedRep #-}++composedRepToRan :: (Representable u, Functor h) => h (Key u, a) -> Ran u h a+composedRepToRan hfa = Ran $ \k -> fmap (\(e, a) -> index (k a) e) hfa+{-# INLINE composedRepToRan #-}

@@ -0,0 +1,191 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE GADTs #-}++#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702+{-# LANGUAGE Trustworthy #-}+#endif+-------------------------------------------------------------------------------------------+-- |+-- Copyright 	: 2013 Edward Kmett and Dan Doel+-- License	: BSD+--+-- Maintainer	: Edward Kmett <ekmett@gmail.com>+-- Stability	: experimental+-- Portability	: rank N types+--+-- Right and Left Kan lifts for functors over Hask, where they exist.+--+-- <http://ncatlab.org/nlab/show/Kan+lift>+-------------------------------------------------------------------------------------------+module Data.Functor.Kan.Rift+  (+  -- * Right Kan lifts+    Rift(..)+  , toRift, fromRift, grift+  , composeRift, decomposeRift+  , adjointToRift, riftToAdjoint+  , composedAdjointToRift, riftToComposedAdjoint+  , rap+  ) where++import Control.Applicative+import Data.Functor.Adjunction+import Data.Functor.Composition+import Data.Functor.Identity+import Data.Pointed++-- * Right Kan Lift++-- |+--+-- @g . 'Rift' g f => f@+--+-- This could alternately be defined directly from the (co)universal propertly+-- in which case, we'd get 'toRift' = 'UniversalRift', but then the usage would+-- suffer.+--+-- @+-- data 'UniversalRift' g f a = forall z. 'Functor' z =>+--      'UniversalRift' (forall x. g (z x) -> f x) (z a)+-- @+--+-- We can witness the isomorphism between Rift and UniversalRift using:+--+-- @+-- riftIso1 :: Functor g => UniversalRift g f a -> Rift g f a+-- riftIso1 (UniversalRift h z) = Rift $ \g -> h $ fmap (\k -> k <$> z) g+-- @+--+-- @+-- riftIso2 :: Rift g f a -> UniversalRift g f a+-- riftIso2 (Rift e) = UniversalRift e id+-- @+--+-- @+-- riftIso1 (riftIso2 (Rift h)) =+-- riftIso1 (UniversalRift h id) =          -- by definition+-- Rift $ \g -> h $ fmap (\k -> k <$> id) g -- by definition+-- Rift $ \g -> h $ fmap id g               -- <$> = (.) and (.id)+-- Rift $ \g -> h g                         -- by functor law+-- Rift h                                   -- eta reduction+-- @+--+-- The other direction is left as an exercise for the reader.+--+-- There are several monads that we can form from @Rift@.+--+-- When @g@ is corepresentable (e.g. is a right adjoint) then there exists @x@ such that @g ~ (->) x@, then it follows that+--+-- @+-- Rift g g a ~+-- forall r. (x -> a -> r) -> x -> r ~+-- forall r. (a -> x -> r) -> x -> r ~+-- forall r. (a -> g r) -> g r ~+-- Codensity g r+-- @+--+-- When @f@ is a left adjoint, so that @f -| g@ then+--+-- @+-- Rift f f a ~+-- forall r. f (a -> r) -> f r ~+-- forall r. (a -> r) -> g (f r) ~+-- forall r. (a -> r) -> Adjoint f g r ~+-- Yoneda (Adjoint f g r)+-- @+--+-- An alternative way to view that is to note that whenever @f@ is a left adjoint then @f -| 'Rift' f 'Identity'@, and since @'Rift' f f@ is isomorphic to @'Rift' f 'Identity' (f a)@, this is the 'Monad' formed by the adjunction.+--+-- @'Rift' w f ~ 'Control.Monad.Co.CoT' w f@ can be a 'Monad' for any 'Comonad' @w@.+--+-- @'Rift' 'Identity' m@ can be a 'Monad' for any 'Monad' @m@, as it is isomorphic to @'Yoneda' m@.++newtype Rift g h a =+  Rift { runRift :: forall r. g (a -> r) -> h r }++instance Functor g => Functor (Rift g h) where+  fmap f (Rift g) = Rift (g . fmap (.f))+  {-# INLINE fmap #-}++instance (Functor g, g ~ h) => Pointed (Rift g h) where+  point a = Rift (fmap ($a))+  {-# INLINE point #-}++instance (Functor g, g ~ h) => Applicative (Rift g h) where+  pure a = Rift (fmap ($a))+  {-# INLINE pure #-}+  Rift mf <*> Rift ma = Rift (ma . mf . fmap (.))+  {-# INLINE (<*>) #-}++-- | Indexed applicative composition of right Kan lifts.+rap :: Functor f => Rift f g (a -> b) -> Rift g h a -> Rift f h b+rap (Rift mf) (Rift ma) = Rift (ma . mf . fmap (.))+{-# INLINE rap #-}++grift :: Adjunction f u => f (Rift f k a) -> k a+grift = rightAdjunct (\r -> leftAdjunct (runRift r) id)+{-# INLINE grift #-}++-- | The universal property of 'Rift'+toRift :: (Functor g, Functor k) => (forall x. g (k x) -> h x) -> k a -> Rift g h a+toRift h z = Rift $ \g -> h $ fmap (<$> z) g+{-# INLINE toRift #-}++-- |+-- When @f -| u@, then @f -| Rift f Identity@ and+--+-- @+-- 'toRift' . 'fromRift' ≡ 'id'+-- 'fromRift' . 'toRift' ≡ 'id'+-- @+fromRift :: Adjunction f u => (forall a. k a -> Rift f h a) -> f (k b) -> h b+fromRift f = grift . fmap f+{-# INLINE fromRift #-}++-- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.+--+-- @+-- 'adjointToRift' . 'riftToAdjoint' ≡ 'id'+-- 'riftToAdjoint' . 'adjointToRift' ≡ 'id'+-- @+adjointToRift :: Adjunction f u => u a -> Rift f Identity a+adjointToRift ua = Rift (Identity . rightAdjunct (<$> ua))+{-# INLINE adjointToRift #-}++-- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.+riftToAdjoint :: Adjunction f u => Rift f Identity a -> u a+riftToAdjoint (Rift m) = leftAdjunct (runIdentity . m) id+{-# INLINE riftToAdjoint #-}++-- |+--+-- @+-- 'composeRift' . 'decomposeRift' ≡ 'id'+-- 'decomposeRift' . 'composeRift' ≡ 'id'+-- @+composeRift :: (Composition compose, Adjunction g u) => Rift f (Rift g h) a -> Rift (compose g f) h a+composeRift (Rift f) = Rift (grift . fmap f . decompose)+{-# INLINE composeRift #-}++decomposeRift :: (Composition compose, Functor f, Functor g) => Rift (compose g f) h a -> Rift f (Rift g h) a+decomposeRift (Rift f) = Rift $ \far -> Rift (f . compose . fmap (\rs -> fmap (rs.) far))+{-# INLINE decomposeRift #-}+++-- | @Rift f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.+--+-- @+-- 'riftToComposedAdjoint' . 'composedAdjointToRift' ≡ 'id'+-- 'composedAdjointToRift' . 'riftToComposedAdjoint' ≡ 'id'+-- @++riftToComposedAdjoint :: Adjunction f u => Rift f h a -> u (h a)+riftToComposedAdjoint (Rift m) = leftAdjunct m id+{-# INLINE riftToComposedAdjoint #-}++-- | @Rift f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.+composedAdjointToRift :: (Functor h, Adjunction f u) => u (h a) -> Rift f h a+composedAdjointToRift uha = Rift $ rightAdjunct (\b -> fmap b <$> uha)+{-# INLINE composedAdjointToRift #-}+

@@ -1,96 +0,0 @@-{-# 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 <ekmett@gmail.com>--- 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)-

@@ -1,284 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE GADTs #-}--#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Trustworthy #-}-#endif----------------------------------------------------------------------------------------------- |--- Copyright 	: 2013 Edward Kmett and Dan Doel--- License	: BSD------ Maintainer	: Edward Kmett <ekmett@gmail.com>--- Stability	: experimental--- Portability	: rank N types------ Right and Left Kan lifts for functors over Hask, where they exist.------ <http://ncatlab.org/nlab/show/Kan+lift>---------------------------------------------------------------------------------------------module Data.Functor.KanLift-  (-  -- * Right Kan lifts-    Rift(..)-  , toRift, fromRift, grift-  , composeRift, decomposeRift-  , adjointToRift, riftToAdjoint-  , composedAdjointToRift, riftToComposedAdjoint-  , rap-  -- * Left Kan lifts-  , Lift(..)-  , toLift, fromLift, glift-  , composeLift, decomposeLift-  , adjointToLift, liftToAdjoint-  , liftToComposedAdjoint, composedAdjointToLift-  ) where--import Control.Applicative-import Data.Copointed-import Data.Functor.Adjunction-import Data.Functor.Composition-import Data.Functor.Compose-import Data.Functor.Identity-import Data.Pointed---- * Right Kan Lift---- |------ @g . 'Rift' g f => f@------ This could alternately be defined directly from the (co)universal propertly--- in which case, we'd get 'toRift' = 'UniversalRift', but then the usage would--- suffer.------ @--- data 'UniversalRift' g f a = forall z. 'Functor' z =>---      'UniversalRift' (forall x. g (z x) -> f x) (z a)--- @------ We can witness the isomorphism between Rift and UniversalRift using:------ @--- riftIso1 :: Functor g => UniversalRift g f a -> Rift g f a--- riftIso1 (UniversalRift h z) = Rift $ \g -> h $ fmap (\k -> k <$> z) g--- @------ @--- riftIso2 :: Rift g f a -> UniversalRift g f a--- riftIso2 (Rift e) = UniversalRift e id--- @------ @--- riftIso1 (riftIso2 (Rift h)) =--- riftIso1 (UniversalRift h id) =          -- by definition--- Rift $ \g -> h $ fmap (\k -> k <$> id) g -- by definition--- Rift $ \g -> h $ fmap id g               -- <$> = (.) and (.id)--- Rift $ \g -> h g                         -- by functor law--- Rift h                                   -- eta reduction--- @------ The other direction is left as an exercise for the reader.------ There are several monads that we can form from @Rift@.------ When @g@ is corepresentable (e.g. is a right adjoint) then there exists @x@ such that @g ~ (->) x@, then it follows that------ @--- Rift g g a ~--- forall r. (x -> a -> r) -> x -> r ~--- forall r. (a -> x -> r) -> x -> r ~--- forall r. (a -> g r) -> g r ~--- Codensity g r--- @------ When @f@ is a left adjoint, so that @f -| g@ then------ @--- Rift f f a ~--- forall r. f (a -> r) -> f r ~--- forall r. (a -> r) -> g (f r) ~--- forall r. (a -> r) -> Adjoint f g r ~--- Yoneda (Adjoint f g r)--- @------ An alternative way to view that is to note that whenever @f@ is a left adjoint then @f -| 'Rift' f 'Identity'@, and since @'Rift' f f@ is isomorphic to @'Rift' f 'Identity' (f a)@, this is the 'Monad' formed by the adjunction.------ @'Rift' w f ~ 'Control.Monad.Co.CoT' w f@ can be a 'Monad' for any 'Comonad' @w@.------ @'Rift' 'Identity' m@ can be a 'Monad' for any 'Monad' @m@, as it is isomorphic to @'Yoneda' m@.--newtype Rift g h a =-  Rift { runRift :: forall r. g (a -> r) -> h r }--instance Functor g => Functor (Rift g h) where-  fmap f (Rift g) = Rift (g . fmap (.f))-  {-# INLINE fmap #-}--instance (Functor g, g ~ h) => Pointed (Rift g h) where-  point a = Rift (fmap ($a))-  {-# INLINE point #-}--instance (Functor g, g ~ h) => Applicative (Rift g h) where-  pure a = Rift (fmap ($a))-  {-# INLINE pure #-}-  Rift mf <*> Rift ma = Rift (ma . mf . fmap (.))-  {-# INLINE (<*>) #-}---- | Indexed applicative composition of right Kan lifts.-rap :: Functor f => Rift f g (a -> b) -> Rift g h a -> Rift f h b-rap (Rift mf) (Rift ma) = Rift (ma . mf . fmap (.))-{-# INLINE rap #-}--grift :: Adjunction f u => f (Rift f k a) -> k a-grift = rightAdjunct (\r -> leftAdjunct (runRift r) id)-{-# INLINE grift #-}---- | The universal property of 'Rift'-toRift :: (Functor g, Functor k) => (forall x. g (k x) -> h x) -> k a -> Rift g h a-toRift h z = Rift $ \g -> h $ fmap (<$> z) g-{-# INLINE toRift #-}---- |--- When @f -| u@, then @f -| Rift f Identity@ and------ @--- 'toRift' . 'fromRift' ≡ 'id'--- 'fromRift' . 'toRift' ≡ 'id'--- @-fromRift :: Adjunction f u => (forall a. k a -> Rift f h a) -> f (k b) -> h b-fromRift f = grift . fmap f-{-# INLINE fromRift #-}---- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.------ @--- 'adjointToRift' . 'riftToAdjoint' ≡ 'id'--- 'riftToAdjoint' . 'adjointToRift' ≡ 'id'--- @-adjointToRift :: Adjunction f u => u a -> Rift f Identity a-adjointToRift ua = Rift (Identity . rightAdjunct (<$> ua))-{-# INLINE adjointToRift #-}---- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.-riftToAdjoint :: Adjunction f u => Rift f Identity a -> u a-riftToAdjoint (Rift m) = leftAdjunct (runIdentity . m) id-{-# INLINE riftToAdjoint #-}---- |------ @--- 'composeRift' . 'decomposeRift' ≡ 'id'--- 'decomposeRift' . 'composeRift' ≡ 'id'--- @-composeRift :: (Composition compose, Adjunction g u) => Rift f (Rift g h) a -> Rift (compose g f) h a-composeRift (Rift f) = Rift (grift . fmap f . decompose)-{-# INLINE composeRift #-}--decomposeRift :: (Composition compose, Functor f, Functor g) => Rift (compose g f) h a -> Rift f (Rift g h) a-decomposeRift (Rift f) = Rift $ \far -> Rift (f . compose . fmap (\rs -> fmap (rs.) far))-{-# INLINE decomposeRift #-}----- |--- | @Rift f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.------ @--- 'riftToComposedAdjoint' . 'composedAdjointToRift' ≡ 'id'--- 'composedAdjointToRift' . 'riftToComposedAdjoint' ≡ 'id'--- @--riftToComposedAdjoint :: Adjunction f u => Rift f h a -> u (h a)-riftToComposedAdjoint (Rift m) = leftAdjunct m id-{-# INLINE riftToComposedAdjoint #-}---- | @Rift f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.-composedAdjointToRift :: (Functor h, Adjunction f u) => u (h a) -> Rift f h a-composedAdjointToRift uha = Rift $ rightAdjunct (\b -> fmap b <$> uha)-{-# INLINE composedAdjointToRift #-}---- * Left Kan Lift---- |--- > f => g . Lift g f--- > (forall z. f => g . z) -> Lift g f => z -- couniversal------ Here we use the universal property directly as how we extract from our definition of 'Lift'.-newtype Lift g f a = Lift { runLift :: forall z. Functor z => (forall x. f x -> g (z x)) -> z a }--instance Functor (Lift g h) where-  fmap f (Lift g) = Lift (fmap f . g)-  {-# INLINE fmap #-}--instance (Functor g, g ~ h) => Copointed (Lift g h) where-  copoint x = runIdentity (runLift x (fmap Identity))-  {-# INLINE copoint #-}---- |------ @f => g ('Lift' g f a)@-glift :: Adjunction l g => k a -> g (Lift g k a)-glift = leftAdjunct (\lka -> Lift (\k2gz -> rightAdjunct k2gz lka))-{-# INLINE glift #-}---- | The universal property of 'Lift'-toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z b-toLift = flip runLift-{-# INLINE toLift #-}---- toLift decompose :: Compose f => Lift g (compose g f) a -> f a---- | When the adjunction exists------ @--- 'fromLift' . 'toLift' ≡ 'id'--- 'toLift' . 'fromLift' ≡ 'id'--- @-fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b)-fromLift f = fmap f . glift-{-# INLINE fromLift #-}---- |------ @--- 'composeLift' . 'decomposeLift' = 'id'--- 'decomposeLift' . 'composeLift' = 'id'--- @-composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h a-composeLift (Lift m) = Lift $ \h -> m $ decompose . toLift (fmap Compose . decompose . h)-{-# INLINE composeLift #-}--decomposeLift :: (Composition compose, Adjunction l g) => Lift (compose g f) h a -> Lift f (Lift g h) a-decomposeLift (Lift m) = Lift $ \h -> m (compose . fmap h . glift)-{-# INLINE decomposeLift #-}---- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.------ @--- 'adjointToLift' . 'liftToAdjoint' ≡ 'id'--- 'liftToAdjoint' . 'adjointToLift' ≡ 'id'--- @-adjointToLift :: Adjunction f u => f a -> Lift u Identity a-adjointToLift fa = Lift $ \k -> rightAdjunct (k . Identity) fa-{-# INLINE adjointToLift #-}---- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.-liftToAdjoint :: Adjunction f u => Lift u Identity a -> f a-liftToAdjoint = toLift (unit . runIdentity)-{-# INLINE liftToAdjoint #-}---- | @Lift u h a@ is isomorphic to the post-composition of the left adjoint of @u@ onto @h@ if such a left adjoint exists.------ @--- 'liftToComposedAdjoint' . 'composedAdjointToLift' ≡ 'id'--- 'composedAdjointToLift' . 'liftToComposedAdjoint' ≡ 'id'--- @-liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a)-liftToComposedAdjoint (Lift m) = decompose $ m (leftAdjunct Compose)-{-# INLINE liftToComposedAdjoint #-}---- | @Lift u h a@ is isomorphic to the post-composition of the left adjoint of @u@ onto @h@ if such a left adjoint exists.-composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h a-composedAdjointToLift = rightAdjunct glift-{-# INLINE composedAdjointToLift #-}

@@ -5,13 +5,20 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Functor.Yoneda--- Copyright   :  (C) 2011 Edward Kmett+-- Copyright   :  (C) 2011-2013 Edward Kmett -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  Edward Kmett <ekmett@gmail.com> -- Stability   :  provisional -- Portability :  MPTCs, fundeps --+-- The co-Yoneda lemma states that+--+-- @f a@ is isomorphic to @(forall r. (a -> r) -> f a)@+--+-- This is described in a rather intuitive fashion by Dan Piponi in+--+-- <http://blog.sigfpe.com/2006/11/yoneda-lemma.html> ----------------------------------------------------------------------------  module Data.Functor.Yoneda

@@ -1,171 +0,0 @@-{-# LANGUAGE CPP, GADTs, FlexibleContexts, MultiParamTypeClasses, UndecidableInstances, TypeFamilies #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Trustworthy #-}-#endif--------------------------------------------------------------------------------- |--- Module      :  Data.Functor.Yoneda.Contravariant--- Copyright   :  (C) 2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  GADTs, MPTCs, fundeps---------------------------------------------------------------------------------module Data.Functor.Yoneda.Contravariant-  ( Yoneda(..)-  , liftYoneda-  , lowerYoneda-  , lowerM-  ) where--import Control.Applicative-import Control.Monad (MonadPlus(..), liftM)-import Control.Monad.Fix-import Control.Monad.Trans.Class-import Control.Comonad-import Control.Comonad.Trans.Class-import Data.Distributive-import Data.Function (on)-import Data.Functor.Bind-import Data.Functor.Extend-import Data.Functor.Plus-import Data.Functor.Adjunction-import Data.Functor.Representable-import Data.Key-import Data.Foldable-import Data.Traversable-import Data.Semigroup.Foldable-import Data.Semigroup.Traversable-import Prelude hiding (sequence, lookup, zipWith)-import Text.Read hiding (lift)---- | The contravariant Yoneda lemma applied to a covariant functor-data Yoneda f a where-  Yoneda :: (b -> a) -> f b -> Yoneda f a--liftYoneda :: f a -> Yoneda f a -liftYoneda = Yoneda id--lowerYoneda :: Functor f => Yoneda f a -> f a-lowerYoneda (Yoneda f m) = fmap f m--lowerM :: Monad f => Yoneda f a -> f a -lowerM (Yoneda f m) = liftM f m--instance Functor (Yoneda f) where-  fmap f (Yoneda g v) = Yoneda (f . g) v--type instance Key (Yoneda f) = Key f--instance Keyed f => Keyed (Yoneda f) where-  mapWithKey f (Yoneda k a) = Yoneda id $ mapWithKey (\x -> f x . k) a--instance Apply f => Apply (Yoneda f) where-  m <.> n = liftYoneda $ lowerYoneda m <.> lowerYoneda n--instance Applicative f => Applicative (Yoneda f) where-  pure = liftYoneda . pure-  m <*> n = liftYoneda $ lowerYoneda m <*> lowerYoneda n--instance Zip f => Zip (Yoneda f) where-  zipWith f m n = liftYoneda $ zipWith f (lowerYoneda m) (lowerYoneda n)--instance ZipWithKey f => ZipWithKey (Yoneda f) where-  zipWithKey f m n = liftYoneda $ zipWithKey f (lowerYoneda m) (lowerYoneda n)--instance Alternative f => Alternative (Yoneda f) where-  empty = liftYoneda empty -  m <|> n = liftYoneda $ lowerYoneda m <|> lowerYoneda n--instance Alt f => Alt (Yoneda f) where-  m <!> n = liftYoneda $ lowerYoneda m <!> lowerYoneda n--instance Plus f => Plus (Yoneda f) where-  zero = liftYoneda zero--instance Bind m => Bind (Yoneda m) where-  Yoneda f v >>- k = liftYoneda (v >>- lowerYoneda . k . f)--instance Monad m => Monad (Yoneda m) where-  return = Yoneda id . return-  Yoneda f v >>= k = lift (v >>= lowerM . k . f)--instance MonadTrans Yoneda where-  lift = Yoneda id--instance MonadFix f => MonadFix (Yoneda f) where-  mfix f = lift $ mfix (lowerM . f)--instance MonadPlus f => MonadPlus (Yoneda f) where-  mzero = lift mzero-  m `mplus` n = lift $ lowerM m `mplus` lowerM n--instance (Functor f, Lookup f) => Lookup (Yoneda f) where-  lookup k f = lookup k (lowerYoneda f)--instance (Functor f, Indexable f) => Indexable (Yoneda f) where-  index = index . lowerYoneda--instance Representable f => Representable (Yoneda f) where-  tabulate = liftYoneda . tabulate--instance Extend w => Extend (Yoneda w) where-  extended k (Yoneda f v) = Yoneda id $ extended (k . Yoneda f) v--instance Comonad w => Comonad (Yoneda w) where-  extend k (Yoneda f v) = Yoneda id $ extend (k . Yoneda f) v-  extract (Yoneda f v) = f (extract v)--instance ComonadTrans Yoneda where-  lower (Yoneda f a) = fmap f a--instance Foldable f => Foldable (Yoneda f) where-  foldMap f (Yoneda k a) = foldMap (f . k) a--instance FoldableWithKey f => FoldableWithKey (Yoneda f) where-  foldMapWithKey f (Yoneda k a) = foldMapWithKey (\x -> f x . k) a--instance Foldable1 f => Foldable1 (Yoneda f) where-  foldMap1 f (Yoneda k a) = foldMap1 (f . k) a--instance FoldableWithKey1 f => FoldableWithKey1 (Yoneda f) where-  foldMapWithKey1 f (Yoneda k a) = foldMapWithKey1 (\x -> f x . k) a--instance Traversable f => Traversable (Yoneda f) where-  traverse f (Yoneda k a) = Yoneda id <$> traverse (f . k) a--instance Traversable1 f => Traversable1 (Yoneda f) where-  traverse1 f (Yoneda k a) = Yoneda id <$> traverse1 (f . k) a--instance TraversableWithKey f => TraversableWithKey (Yoneda f) where-  traverseWithKey f (Yoneda k a) = Yoneda id <$> traverseWithKey (\x -> f x . k) a--instance TraversableWithKey1 f => TraversableWithKey1 (Yoneda f) where-  traverseWithKey1 f (Yoneda k a) = Yoneda id <$> traverseWithKey1 (\x -> f x . k) a--instance Distributive f => Distributive (Yoneda f) where-  collect f = liftYoneda . collect (lowerYoneda . f)--instance (Functor f, Show (f a)) => Show (Yoneda f a) where-  showsPrec d (Yoneda f a) = showParen (d > 10) $-    showString "liftYoneda " . showsPrec 11 (fmap f a)--#ifdef __GLASGOW_HASKELL__-instance (Functor f, Read (f a)) => Read (Yoneda f a) where-  readPrec = parens $ prec 10 $ do-    Ident "liftYoneda" <- lexP-    liftYoneda <$> step readPrec-#endif--instance (Functor f, Eq (f a)) => Eq (Yoneda f a) where-  (==) = (==) `on` lowerYoneda--instance (Functor f, Ord (f a)) => Ord (Yoneda f a) where-  compare = compare `on` lowerYoneda--instance Adjunction f g => Adjunction (Yoneda f) (Yoneda g) where-  unit = liftYoneda . fmap liftYoneda . unit-  counit = counit . fmap lowerYoneda . lowerYoneda-

@@ -0,0 +1,220 @@+{-# LANGUAGE CPP, GADTs, FlexibleContexts, MultiParamTypeClasses, UndecidableInstances, TypeFamilies #-}+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702+{-# LANGUAGE Trustworthy #-}+#endif+-----------------------------------------------------------------------------+-- |+-- Copyright   :  (C) 2011-2013 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  provisional+-- Portability :  GADTs, MPTCs, fundeps+--+-- Yoneda Reduction:+--+-- <http://ncatlab.org/nlab/show/Yoneda+reduction>+--+-- @Yoneda f@ is isomorphic to @Lan f Identity@+----------------------------------------------------------------------------+module Data.Functor.Yoneda.Reduction+  ( Yoneda(..)+  , liftYoneda+  , lowerYoneda+  , lowerM+  ) where++import Control.Applicative+import Control.Monad (MonadPlus(..), liftM)+import Control.Monad.Fix+import Control.Monad.Trans.Class+import Control.Comonad+import Control.Comonad.Trans.Class+import Data.Distributive+import Data.Function (on)+import Data.Functor.Bind+import Data.Functor.Extend+import Data.Functor.Plus+import Data.Functor.Adjunction+import Data.Functor.Representable+import Data.Key+import Data.Foldable+import Data.Traversable+import Data.Semigroup.Foldable+import Data.Semigroup.Traversable+import Prelude hiding (sequence, lookup, zipWith)+import Text.Read hiding (lift)++-- | A form suitable for Yoneda reduction+data Yoneda f a where+  Yoneda :: (b -> a) -> f b -> Yoneda f a++-- | Yoneda "expansion"+liftYoneda :: f a -> Yoneda f a+liftYoneda = Yoneda id+{-# INLINE liftYoneda #-}++-- | Yoneda reduction+lowerYoneda :: Functor f => Yoneda f a -> f a+lowerYoneda (Yoneda f m) = fmap f m+{-# INLINE lowerYoneda #-}++-- | Yoneda reduction given a 'Monad'.+lowerM :: Monad f => Yoneda f a -> f a+lowerM (Yoneda f m) = liftM f m+{-# INLINE lowerM #-}++instance Functor (Yoneda f) where+  fmap f (Yoneda g v) = Yoneda (f . g) v+  {-# INLINE fmap #-}++type instance Key (Yoneda f) = Key f++instance Keyed f => Keyed (Yoneda f) where+  mapWithKey f (Yoneda k a) = Yoneda id $ mapWithKey (\x -> f x . k) a+  {-# INLINE mapWithKey #-}++instance Apply f => Apply (Yoneda f) where+  m <.> n = liftYoneda $ lowerYoneda m <.> lowerYoneda n+  {-# INLINE (<.>) #-}++instance Applicative f => Applicative (Yoneda f) where+  pure = liftYoneda . pure+  {-# INLINE pure #-}+  m <*> n = liftYoneda $ lowerYoneda m <*> lowerYoneda n+  {-# INLINE (<*>) #-}++instance Zip f => Zip (Yoneda f) where+  zipWith f m n = liftYoneda $ zipWith f (lowerYoneda m) (lowerYoneda n)+  {-# INLINE zipWith #-}++instance ZipWithKey f => ZipWithKey (Yoneda f) where+  zipWithKey f m n = liftYoneda $ zipWithKey f (lowerYoneda m) (lowerYoneda n)+  {-# INLINE zipWithKey #-}++instance Alternative f => Alternative (Yoneda f) where+  empty = liftYoneda empty+  {-# INLINE empty #-}+  m <|> n = liftYoneda $ lowerYoneda m <|> lowerYoneda n+  {-# INLINE (<|>) #-}++instance Alt f => Alt (Yoneda f) where+  m <!> n = liftYoneda $ lowerYoneda m <!> lowerYoneda n+  {-# INLINE (<!>) #-}++instance Plus f => Plus (Yoneda f) where+  zero = liftYoneda zero+  {-# INLINE zero #-}++instance Bind m => Bind (Yoneda m) where+  Yoneda f v >>- k = liftYoneda (v >>- lowerYoneda . k . f)+  {-# INLINE (>>-) #-}++instance Monad m => Monad (Yoneda m) where+  return = Yoneda id . return+  {-# INLINE return #-}+  Yoneda f v >>= k = lift (v >>= lowerM . k . f)+  {-# INLINE (>>=) #-}++instance MonadTrans Yoneda where+  lift = Yoneda id+  {-# INLINE lift #-}++instance MonadFix f => MonadFix (Yoneda f) where+  mfix f = lift $ mfix (lowerM . f)+  {-# INLINE mfix #-}++instance MonadPlus f => MonadPlus (Yoneda f) where+  mzero = lift mzero+  {-# INLINE mzero #-}+  m `mplus` n = lift $ lowerM m `mplus` lowerM n+  {-# INLINE mplus #-}++instance (Functor f, Lookup f) => Lookup (Yoneda f) where+  lookup k f = lookup k (lowerYoneda f)+  {-# INLINE lookup #-}++instance (Functor f, Indexable f) => Indexable (Yoneda f) where+  index = index . lowerYoneda+  {-# INLINE index #-}++instance Representable f => Representable (Yoneda f) where+  tabulate = liftYoneda . tabulate+  {-# INLINE tabulate #-}++instance Extend w => Extend (Yoneda w) where+  extended k (Yoneda f v) = Yoneda id $ extended (k . Yoneda f) v+  {-# INLINE extended #-}++instance Comonad w => Comonad (Yoneda w) where+  extend k (Yoneda f v) = Yoneda id $ extend (k . Yoneda f) v+  {-# INLINE extend #-}+  extract (Yoneda f v) = f (extract v)+  {-# INLINE extract #-}++instance ComonadTrans Yoneda where+  lower (Yoneda f a) = fmap f a+  {-# INLINE lower #-}++instance Foldable f => Foldable (Yoneda f) where+  foldMap f (Yoneda k a) = foldMap (f . k) a+  {-# INLINE foldMap #-}++instance FoldableWithKey f => FoldableWithKey (Yoneda f) where+  foldMapWithKey f (Yoneda k a) = foldMapWithKey (\x -> f x . k) a+  {-# INLINE foldMapWithKey #-}++instance Foldable1 f => Foldable1 (Yoneda f) where+  foldMap1 f (Yoneda k a) = foldMap1 (f . k) a+  {-# INLINE foldMap1 #-}++instance FoldableWithKey1 f => FoldableWithKey1 (Yoneda f) where+  foldMapWithKey1 f (Yoneda k a) = foldMapWithKey1 (\x -> f x . k) a+  {-# INLINE foldMapWithKey1 #-}++instance Traversable f => Traversable (Yoneda f) where+  traverse f (Yoneda k a) = Yoneda id <$> traverse (f . k) a+  {-# INLINE traverse #-}++instance Traversable1 f => Traversable1 (Yoneda f) where+  traverse1 f (Yoneda k a) = Yoneda id <$> traverse1 (f . k) a+  {-# INLINE traverse1 #-}++instance TraversableWithKey f => TraversableWithKey (Yoneda f) where+  traverseWithKey f (Yoneda k a) = Yoneda id <$> traverseWithKey (\x -> f x . k) a+  {-# INLINE traverseWithKey #-}++instance TraversableWithKey1 f => TraversableWithKey1 (Yoneda f) where+  traverseWithKey1 f (Yoneda k a) = Yoneda id <$> traverseWithKey1 (\x -> f x . k) a+  {-# INLINE traverseWithKey1 #-}++instance Distributive f => Distributive (Yoneda f) where+  collect f = liftYoneda . collect (lowerYoneda . f)+  {-# INLINE collect #-}++instance (Functor f, Show (f a)) => Show (Yoneda f a) where+  showsPrec d (Yoneda f a) = showParen (d > 10) $+    showString "liftYoneda " . showsPrec 11 (fmap f a)+  {-# INLINE showsPrec #-}++#ifdef __GLASGOW_HASKELL__+instance (Functor f, Read (f a)) => Read (Yoneda f a) where+  readPrec = parens $ prec 10 $ do+    Ident "liftYoneda" <- lexP+    liftYoneda <$> step readPrec+  {-# INLINE readPrec #-}+#endif++instance (Functor f, Eq (f a)) => Eq (Yoneda f a) where+  (==) = (==) `on` lowerYoneda+  {-# INLINE (==) #-}++instance (Functor f, Ord (f a)) => Ord (Yoneda f a) where+  compare = compare `on` lowerYoneda+  {-# INLINE compare #-}++instance Adjunction f g => Adjunction (Yoneda f) (Yoneda g) where+  unit = liftYoneda . fmap liftYoneda . unit+  {-# INLINE unit #-}+  counit = counit . fmap lowerYoneda . lowerYoneda+  {-# INLINE counit #-}