-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads -- -- Kan extensions, Kan lifts, various forms of the Yoneda lemma, and -- (co)density (co)monads @package kan-extensions @version 5 -- | Eitan Chatav first introduced me to this construction -- -- The Day convolution of two covariant functors is a covariant functor. -- -- Day convolution is usually defined in terms of contravariant functors, -- however, it just needs a monoidal category, and Hask^op is also -- monoidal. -- -- Day convolution can be used to nicely describe monoidal functors as -- monoid objects w.r.t this product. -- -- http://ncatlab.org/nlab/show/Day+convolution module Data.Functor.Day -- | The Day convolution of two covariant functors. -- -- Day f g a -> h a is isomorphic to f a -> Rift g h -- a data Day f g a Day :: (f b) -> (g c) -> (b -> c -> a) -> Day f g a -- | Construct the Day convolution day :: f (a -> b) -> g a -> Day f g b -- | Collapse via a monoidal functor. -- --
--   dap (day f g) = f <*> g
--   
dap :: Applicative f => Day f f a -> f a -- | Day convolution provides a monoidal product. The associativity of this -- monoid is witnessed by assoc and disassoc. -- --
--   assoc . disassoc = id
--   disassoc . assoc = id
--   fmap f . assoc = assoc . fmap f
--   
assoc :: Day f (Day g h) a -> Day (Day f g) h a -- | Day convolution provides a monoidal product. The associativity of this -- monoid is witnessed by assoc and disassoc. -- --
--   assoc . disassoc = id
--   disassoc . assoc = id
--   fmap f . disassoc = disassoc . fmap f
--   
disassoc :: Day (Day f g) h a -> Day f (Day g h) a -- | The monoid for Day convolution on the cartesian monoidal -- structure is symmetric. -- --
--   fmap f . swapped = swapped . fmap f
--   
swapped :: Day f g a -> Day g f a -- | Identity is the unit of Day convolution -- --
--   intro1 . elim1 = id
--   elim1 . intro1 = id
--   
intro1 :: f a -> Day Identity f a -- | Identity is the unit of Day convolution -- --
--   intro2 . elim2 = id
--   elim2 . intro2 = id
--   
intro2 :: f a -> Day f Identity a -- | Identity is the unit of Day convolution -- --
--   intro1 . elim1 = id
--   elim1 . intro1 = id
--   
elim1 :: Functor f => Day Identity f a -> f a -- | Identity is the unit of Day convolution -- --
--   intro2 . elim2 = id
--   elim2 . intro2 = id
--   
elim2 :: Functor f => Day f Identity a -> f a -- | Apply a natural transformation to the left-hand side of a Day -- convolution. -- -- This respects the naturality of the natural transformation you -- supplied: -- --
--   fmap f . trans1 fg = trans1 fg . fmap f
--   
trans1 :: (forall x. f x -> g x) -> Day f h a -> Day g h a -- | Apply a natural transformation to the right-hand side of a Day -- convolution. -- -- This respects the naturality of the natural transformation you -- supplied: -- --
--   fmap f . trans2 fg = trans2 fg . fmap f
--   
trans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a instance GHC.Base.Functor (Data.Functor.Day.Day f g) instance (GHC.Base.Applicative f, GHC.Base.Applicative g) => GHC.Base.Applicative (Data.Functor.Day.Day f g) instance (Data.Functor.Rep.Representable f, Data.Functor.Rep.Representable g) => Data.Distributive.Distributive (Data.Functor.Day.Day f g) instance (Data.Functor.Rep.Representable f, Data.Functor.Rep.Representable g) => Data.Functor.Rep.Representable (Data.Functor.Day.Day f g) -- |
--   Day f -| Curried f
--   
-- -- Day f ~ Compose f when f preserves colimits / -- is a left adjoint. (Due in part to the strength of all functors in -- Hask.) -- -- So by the uniqueness of adjoints, when f is a left adjoint, -- Curried f ~ Rift f module Data.Functor.Day.Curried newtype Curried g h a Curried :: (forall r. g (a -> r) -> h r) -> Curried g h a [runCurried] :: Curried g h a -> forall r. g (a -> r) -> h r -- | The universal property of Curried toCurried :: (Functor g, Functor k) => (forall x. Day g k x -> h x) -> k a -> Curried g h a -- |
--   toCurried . fromCurriedid
--   fromCurried . toCurriedid
--   
fromCurried :: Functor f => (forall a. k a -> Curried f h a) -> Day f k b -> h b -- | This is the counit of the Day f -| Curried f adjunction applied :: Functor f => Day f (Curried f g) a -> g a -- | This is the unit of the Day f -| Curried f adjunction unapplied :: Functor f => g a -> Curried f (Day f g) a -- | Curried f Identity a is isomorphic to the right adjoint to -- f if one exists. -- --
--   adjointToCurried . curriedToAdjointid
--   curriedToAdjoint . adjointToCurriedid
--   
adjointToCurried :: Adjunction f u => u a -> Curried f Identity a -- | Curried f Identity a is isomorphic to the right adjoint to -- f if one exists. curriedToAdjoint :: Adjunction f u => Curried f Identity a -> u a -- | Curried f h a is isomorphic to the post-composition of the -- right adjoint of f onto h if such a right adjoint -- exists. composedAdjointToCurried :: (Functor h, Adjunction f u) => u (h a) -> Curried f h a -- | Curried f h a is isomorphic to the post-composition of the -- right adjoint of f onto h if such a right adjoint -- exists. -- --
--   curriedToComposedAdjoint . composedAdjointToCurriedid
--   composedAdjointToCurried . curriedToComposedAdjointid
--   
curriedToComposedAdjoint :: Adjunction f u => Curried f h a -> u (h a) -- | The natural isomorphism between f and Curried f f. -- lowerCurried . liftCurriedid -- liftCurried . lowerCurriedid -- --
--   lowerCurried (liftCurried x)     -- definition
--   lowerCurried (Curried (<*> x))   -- definition
--   (<*> x) (pure id)          -- beta reduction
--   pure id <*> x              -- Applicative identity law
--   x
--   
liftCurried :: Applicative f => f a -> Curried f f a -- | Lower Curried by applying pure id to the -- continuation. -- -- See liftCurried. lowerCurried :: Applicative f => Curried f g a -> g a -- | Indexed applicative composition of right Kan lifts. rap :: Functor f => Curried f g (a -> b) -> Curried g h a -> Curried f h b instance GHC.Base.Functor g => GHC.Base.Functor (Data.Functor.Day.Curried.Curried g h) instance (GHC.Base.Functor g, g ~ h) => GHC.Base.Applicative (Data.Functor.Day.Curried.Curried g h) -- | The co-Yoneda lemma for presheafs states that f is naturally -- isomorphic to Coyoneda f. module Data.Functor.Contravariant.Coyoneda -- | A Contravariant functor (aka presheaf) suitable for Yoneda -- reduction. -- -- http://ncatlab.org/nlab/show/Yoneda+reduction data Coyoneda f a Coyoneda :: (a -> b) -> f b -> Coyoneda f a -- | Coyoneda "expansion" of a presheaf -- --
--   liftCoyoneda . lowerCoyonedaid
--   lowerCoyoneda . liftCoyonedaid
--   
liftCoyoneda :: f a -> Coyoneda f a -- | Coyoneda reduction on a presheaf lowerCoyoneda :: Contravariant f => Coyoneda f a -> f a instance Data.Functor.Contravariant.Contravariant (Data.Functor.Contravariant.Coyoneda.Coyoneda f) instance Data.Functor.Contravariant.Rep.Representable f => Data.Functor.Contravariant.Rep.Representable (Data.Functor.Contravariant.Coyoneda.Coyoneda f) instance Data.Functor.Contravariant.Adjunction.Adjunction f g => Data.Functor.Contravariant.Adjunction.Adjunction (Data.Functor.Contravariant.Coyoneda.Coyoneda f) (Data.Functor.Contravariant.Coyoneda.Coyoneda g) module Data.Functor.Contravariant.Yoneda -- | Yoneda embedding for a presheaf newtype Yoneda f a Yoneda :: (forall r. (r -> a) -> f r) -> Yoneda f a [runYoneda] :: Yoneda f a -> forall r. (r -> a) -> f r -- |
--   liftYoneda . lowerYonedaid
--   lowerYoneda . liftYonedaid
--   
liftYoneda :: Contravariant f => f a -> Yoneda f a lowerYoneda :: Yoneda f a -> f a instance Data.Functor.Contravariant.Contravariant (Data.Functor.Contravariant.Yoneda.Yoneda f) instance Data.Functor.Contravariant.Rep.Representable f => Data.Functor.Contravariant.Rep.Representable (Data.Functor.Contravariant.Yoneda.Yoneda f) instance Data.Functor.Contravariant.Adjunction.Adjunction f g => Data.Functor.Contravariant.Adjunction.Adjunction (Data.Functor.Contravariant.Yoneda.Yoneda f) (Data.Functor.Contravariant.Yoneda.Yoneda g) -- | The Day convolution of two contravariant functors is a contravariant -- functor. -- -- http://ncatlab.org/nlab/show/Day+convolution module Data.Functor.Contravariant.Day -- | The Day convolution of two contravariant functors. data Day f g a Day :: (f b) -> (g c) -> (a -> (b, c)) -> Day f g a -- | Construct the Day convolution -- --
--   day1 (day f g) = f
--   day2 (day f g) = g
--   
day :: f a -> g b -> Day f g (a, b) -- | Break apart the Day convolution of two contravariant functors. runDay :: (Contravariant f, Contravariant g) => Day f g a -> (f a, g a) -- | Day convolution provides a monoidal product. The associativity of this -- monoid is witnessed by assoc and disassoc. -- --
--   assoc . disassoc = id
--   disassoc . assoc = id
--   contramap f . assoc = assoc . contramap f
--   
assoc :: Day f (Day g h) a -> Day (Day f g) h a -- | Day convolution provides a monoidal product. The associativity of this -- monoid is witnessed by assoc and disassoc. -- --
--   assoc . disassoc = id
--   disassoc . assoc = id
--   contramap f . disassoc = disassoc . contramap f
--   
disassoc :: Day (Day f g) h a -> Day f (Day g h) a -- | The monoid for Day convolution in Haskell is symmetric. -- --
--   contramap f . swapped = swapped . contramap f
--   
swapped :: Day f g a -> Day g f a -- | Proxy serves as the unit of Day convolution. -- --
--   day1 . intro1 = id
--   contramap f . intro1 = intro1 . contramap f
--   
intro1 :: f a -> Day Proxy f a -- | Proxy serves as the unit of Day convolution. -- --
--   day2 . intro2 = id
--   contramap f . intro2 = intro2 . contramap f
--   
intro2 :: f a -> Day f Proxy a -- | In Haskell we can do general purpose elimination, but in a more -- general setting it is only possible to eliminate the unit. -- --
--   day1 . intro1 = id
--   day1 = fst . runDay
--   contramap f . day1 = day1 . contramap f
--   
day1 :: Contravariant f => Day f g a -> f a -- | In Haskell we can do general purpose elimination, but in a more -- general setting it is only possible to eliminate the unit. -- day2 . intro2 = id day2 = -- snd . runDay contramap f . -- day2 = day2 . contramap f day2 :: Contravariant g => Day f g a -> g a -- | Diagonalize the Day convolution: -- --
--   day1 . diag = id
--   day2 . diag = id
--   runDay . diag = a -> (a,a)
--   contramap f . diag = diag . contramap f
--   
diag :: f a -> Day f f a -- | Apply a natural transformation to the left-hand side of a Day -- convolution. -- -- This respects the naturality of the natural transformation you -- supplied: -- --
--   contramap f . trans1 fg = trans1 fg . contramap f
--   
trans1 :: (forall x. f x -> g x) -> Day f h a -> Day g h a -- | Apply a natural transformation to the right-hand side of a Day -- convolution. -- -- This respects the naturality of the natural transformation you -- supplied: -- --
--   contramap f . trans2 fg = trans2 fg . contramap f
--   
trans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a instance Data.Functor.Contravariant.Contravariant (Data.Functor.Contravariant.Day.Day f g) instance (Data.Functor.Contravariant.Rep.Representable f, Data.Functor.Contravariant.Rep.Representable g) => Data.Functor.Contravariant.Rep.Representable (Data.Functor.Contravariant.Day.Day f g) -- | module Data.Functor.Kan.Ran -- | 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 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 :: (forall b. (a -> g b) -> h b) -> Ran g h a [runRan] :: Ran g h a -> forall b. (a -> g b) -> h b -- | 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 and fromRan witness a higher kinded adjunction. -- from (`Compose' g) to Ran g -- --
--   toRan . fromRanid
--   fromRan . toRanid
--   
fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b -- | This is the natural transformation that defines a Right Kan extension. gran :: Ran g h (g a) -> h a -- |
--   composeRan . decomposeRanid
--   decomposeRan . composeRanid
--   
composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) a -- |
--   adjointToRan . ranToAdjointid
--   ranToAdjoint . adjointToRanid
--   
adjointToRan :: Adjunction f g => f a -> Ran g Identity a ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a composedAdjointToRan :: (Adjunction f g, Functor h) => h (f a) -> Ran g h a -- |
--   composedAdjointToRan . ranToComposedAdjointid
--   ranToComposedAdjoint . composedAdjointToRanid
--   
ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f a) repToRan :: Representable u => Rep u -> a -> Ran u Identity a ranToRep :: Representable u => Ran u Identity a -> (Rep u, a) composedRepToRan :: (Representable u, Functor h) => h (Rep u, a) -> Ran u h a ranToComposedRep :: Representable u => Ran u h a -> h (Rep u, a) instance GHC.Base.Functor (Data.Functor.Kan.Ran.Ran g h) -- | The covariant form of the Yoneda lemma states that f is -- naturally isomorphic to Yoneda f. -- -- 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 -- | Yoneda f a can be viewed as the partial application of -- fmap to its second argument. newtype Yoneda f a Yoneda :: (forall b. (a -> b) -> f b) -> Yoneda f a [runYoneda] :: Yoneda f a -> forall b. (a -> b) -> f b -- | The natural isomorphism between f and Yoneda -- f given by the Yoneda lemma is witnessed by liftYoneda and -- lowerYoneda -- --
--   liftYoneda . lowerYonedaid
--   lowerYoneda . liftYonedaid
--   
-- --
--   lowerYoneda (liftYoneda fa) =         -- definition
--   lowerYoneda (Yoneda (f -> fmap f a)) -- definition
--   (f -> fmap f fa) id                  -- beta reduction
--   fmap id fa                            -- functor law
--   fa
--   
-- --
--   lift = liftYoneda
--   
liftYoneda :: Functor f => f a -> Yoneda f a lowerYoneda :: Yoneda f a -> f a maxF :: (Functor f, Ord (f a)) => Yoneda f a -> Yoneda f a -> Yoneda f a minF :: (Functor f, Ord (f a)) => Yoneda f a -> Yoneda f a -> Yoneda f a maxM :: (Monad m, Ord (m a)) => Yoneda m a -> Yoneda m a -> Yoneda m a minM :: (Monad m, Ord (m a)) => Yoneda m a -> Yoneda m a -> Yoneda m a -- | Yoneda f can be viewed as the right Kan extension of -- f along the Identity functor. -- --
--   yonedaToRan . ranToYonedaid
--   ranToYoneda . yonedaToRanid
--   
yonedaToRan :: Yoneda f a -> Ran Identity f a ranToYoneda :: Ran Identity f a -> Yoneda f a instance GHC.Base.Functor (Data.Functor.Yoneda.Yoneda f) instance Data.Functor.Bind.Class.Apply f => Data.Functor.Bind.Class.Apply (Data.Functor.Yoneda.Yoneda f) instance GHC.Base.Applicative f => GHC.Base.Applicative (Data.Functor.Yoneda.Yoneda f) instance Data.Foldable.Foldable f => Data.Foldable.Foldable (Data.Functor.Yoneda.Yoneda f) instance Data.Semigroup.Foldable.Class.Foldable1 f => Data.Semigroup.Foldable.Class.Foldable1 (Data.Functor.Yoneda.Yoneda f) instance Data.Traversable.Traversable f => Data.Traversable.Traversable (Data.Functor.Yoneda.Yoneda f) instance Data.Semigroup.Traversable.Class.Traversable1 f => Data.Semigroup.Traversable.Class.Traversable1 (Data.Functor.Yoneda.Yoneda f) instance Data.Distributive.Distributive f => Data.Distributive.Distributive (Data.Functor.Yoneda.Yoneda f) instance Data.Functor.Rep.Representable g => Data.Functor.Rep.Representable (Data.Functor.Yoneda.Yoneda g) instance Data.Functor.Adjunction.Adjunction f g => Data.Functor.Adjunction.Adjunction (Data.Functor.Yoneda.Yoneda f) (Data.Functor.Yoneda.Yoneda g) instance GHC.Show.Show (f a) => GHC.Show.Show (Data.Functor.Yoneda.Yoneda f a) instance (GHC.Base.Functor f, GHC.Read.Read (f a)) => GHC.Read.Read (Data.Functor.Yoneda.Yoneda f a) instance GHC.Classes.Eq (f a) => GHC.Classes.Eq (Data.Functor.Yoneda.Yoneda f a) instance GHC.Classes.Ord (f a) => GHC.Classes.Ord (Data.Functor.Yoneda.Yoneda f a) instance Data.Functor.Alt.Alt f => Data.Functor.Alt.Alt (Data.Functor.Yoneda.Yoneda f) instance Data.Functor.Plus.Plus f => Data.Functor.Plus.Plus (Data.Functor.Yoneda.Yoneda f) instance GHC.Base.Alternative f => GHC.Base.Alternative (Data.Functor.Yoneda.Yoneda f) instance Data.Functor.Bind.Class.Bind m => Data.Functor.Bind.Class.Bind (Data.Functor.Yoneda.Yoneda m) instance GHC.Base.Monad m => GHC.Base.Monad (Data.Functor.Yoneda.Yoneda m) instance Control.Monad.Fix.MonadFix m => Control.Monad.Fix.MonadFix (Data.Functor.Yoneda.Yoneda m) instance GHC.Base.MonadPlus m => GHC.Base.MonadPlus (Data.Functor.Yoneda.Yoneda m) instance Control.Monad.Trans.Class.MonadTrans Data.Functor.Yoneda.Yoneda instance (GHC.Base.Functor f, Control.Monad.Free.Class.MonadFree f m) => Control.Monad.Free.Class.MonadFree f (Data.Functor.Yoneda.Yoneda m) instance Data.Functor.Extend.Extend w => Data.Functor.Extend.Extend (Data.Functor.Yoneda.Yoneda w) instance Control.Comonad.Comonad w => Control.Comonad.Comonad (Data.Functor.Yoneda.Yoneda w) instance Control.Comonad.Trans.Class.ComonadTrans Data.Functor.Yoneda.Yoneda module Control.Monad.Codensity -- | 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 -- Voigtländer for more information about this type. -- -- http://www.iai.uni-bonn.de/~jv/mpc08.pdf newtype Codensity m a Codensity :: (forall b. (a -> m b) -> m b) -> Codensity m a [runCodensity] :: Codensity m a -> forall b. (a -> m b) -> m b -- | This serves as the *left*-inverse (retraction) of lift. -- --
--   lowerCodensity . liftid
--   
-- -- 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 :: Applicative f => Codensity f a -> f a -- | The Codensity monad of a right adjoint is isomorphic to the -- monad obtained from the Adjunction. -- --
--   codensityToAdjunction . adjunctionToCodensityid
--   adjunctionToCodensity . codensityToAdjunctionid
--   
codensityToAdjunction :: Adjunction f g => Codensity g a -> g (f a) adjunctionToCodensity :: Adjunction f g => g (f a) -> Codensity g a -- | The Codensity Monad of a Functor g is -- the right Kan extension (Ran) of g along itself. -- --
--   codensityToRan . ranToCodensityid
--   ranToCodensity . codensityToRanid
--   
codensityToRan :: Codensity g a -> Ran g g a ranToCodensity :: Ran g g a -> Codensity g a -- | 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 . composedRepToCodensityid
--   composedRepToCodensity . codensityToComposedRepid
--   
-- --
--   codensityToComposedRep = ranToComposedRep . codensityToRan
--   
codensityToComposedRep :: Representable u => Codensity u a -> u (Rep u, a) -- |
--   composedRepToCodensity = ranToCodensity . composedRepToRan
--   
composedRepToCodensity :: Representable u => u (Rep u, a) -> Codensity u a -- | 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 instance GHC.Base.Functor (Control.Monad.Codensity.Codensity k) instance Data.Functor.Bind.Class.Apply (Control.Monad.Codensity.Codensity f) instance GHC.Base.Applicative (Control.Monad.Codensity.Codensity f) instance GHC.Base.Monad (Control.Monad.Codensity.Codensity f) instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Control.Monad.Codensity.Codensity m) instance Control.Monad.Trans.Class.MonadTrans Control.Monad.Codensity.Codensity instance Data.Functor.Alt.Alt v => Data.Functor.Alt.Alt (Control.Monad.Codensity.Codensity v) instance Data.Functor.Plus.Plus v => Data.Functor.Plus.Plus (Control.Monad.Codensity.Codensity v) instance GHC.Base.Alternative v => GHC.Base.Alternative (Control.Monad.Codensity.Codensity v) instance GHC.Base.Alternative v => GHC.Base.MonadPlus (Control.Monad.Codensity.Codensity v) instance (GHC.Base.Functor f, Control.Monad.Free.Class.MonadFree f m) => Control.Monad.Free.Class.MonadFree f (Control.Monad.Codensity.Codensity m) instance Control.Monad.Reader.Class.MonadReader r m => Control.Monad.State.Class.MonadState r (Control.Monad.Codensity.Codensity m) instance Control.Monad.Reader.Class.MonadReader r m => Control.Monad.Reader.Class.MonadReader r (Control.Monad.Codensity.Codensity m) -- | Left Kan Extensions module Data.Functor.Kan.Lan -- | The left Kan extension of a Functor h along a -- Functor g. data Lan g h a Lan :: (g b -> a) -> h b -> Lan g h a -- | The universal property of a left Kan extension. toLan :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f b -- | fromLan and toLan witness a (higher kinded) adjunction -- between Lan g and (Compose g) -- --
--   toLan . fromLanid
--   fromLan . toLanid
--   
fromLan :: (forall a. Lan g h a -> f a) -> h b -> f (g b) -- | This is the natural transformation that defines a Left Kan extension. glan :: h a -> Lan g h (g a) -- | composeLan and decomposeLan witness the natural -- isomorphism from Lan f (Lan g h) and Lan (f o g) -- h -- --
--   composeLan . decomposeLanid
--   decomposeLan . composeLanid
--   
composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h a decomposeLan :: Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) a -- |
--   adjointToLan . lanToAdjointid
--   lanToAdjoint . adjointToLanid
--   
adjointToLan :: Adjunction f g => g a -> Lan f Identity a lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a composedAdjointToLan :: Adjunction f g => h (g a) -> Lan f h a -- | lanToComposedAdjoint and composedAdjointToLan witness -- the natural isomorphism between Lan f h and Compose h -- g given f -| g -- --
--   composedAdjointToLan . lanToComposedAdjointid
--   lanToComposedAdjoint . composedAdjointToLanid
--   
lanToComposedAdjoint :: (Functor h, Adjunction f g) => Lan f h a -> h (g a) instance GHC.Base.Functor (Data.Functor.Kan.Lan.Lan f g) instance (GHC.Base.Functor g, Data.Functor.Bind.Class.Apply h) => Data.Functor.Bind.Class.Apply (Data.Functor.Kan.Lan.Lan g h) instance (GHC.Base.Functor g, GHC.Base.Applicative h) => GHC.Base.Applicative (Data.Functor.Kan.Lan.Lan g h) -- | The co-Yoneda lemma for a covariant Functor f states -- that Coyoneda f is naturally isomorphic to f. module Data.Functor.Coyoneda -- | A covariant Functor suitable for Yoneda reduction data Coyoneda f a Coyoneda :: (b -> a) -> f b -> Coyoneda f a -- | Yoneda "expansion" -- --
--   liftCoyoneda . lowerCoyonedaid
--   lowerCoyoneda . liftCoyonedaid
--   
-- --
--   lowerCoyoneda (liftCoyoneda fa) = -- by definition
--   lowerCoyoneda (Coyoneda id fa)  = -- by definition
--   fmap id fa                      = -- functor law
--   fa
--   
-- --
--   lift = liftCoyoneda
--   
liftCoyoneda :: f a -> Coyoneda f a -- | Yoneda reduction lets us walk under the existential and apply -- fmap. -- -- Mnemonically, "Yoneda reduction" sounds like and works a bit like -- β-reduction. -- -- http://ncatlab.org/nlab/show/Yoneda+reduction -- -- You can view Coyoneda as just the arguments to fmap -- tupled up. -- --
--   lower = lowerM = lowerCoyoneda
--   
lowerCoyoneda :: Functor f => Coyoneda f a -> f a -- | Yoneda reduction given a Monad lets us walk under the -- existential and apply liftM. -- -- You can view Coyoneda as just the arguments to liftM -- tupled up. -- --
--   lower = lowerM = lowerCoyoneda
--   
lowerM :: Monad f => Coyoneda f a -> f a -- | Coyoneda f is the left Kan extension of f along the -- Identity functor. -- -- Coyoneda f is always a functor, even if f is not. In -- this case, it is called the free functor over f. Note -- the following categorical fine print: If f is not a functor, -- Coyoneda f is actually not the left Kan extension of -- f along the Identity functor, but along the inclusion -- functor from the discrete subcategory of Hask which contains -- only identity functions as morphisms to the full category Hask. -- (This is because f, not being a proper functor, can only be -- interpreted as a categorical functor by restricting the source -- category to only contain identities.) -- --
--   coyonedaToLan . lanToCoyonedaid
--   lanToCoyoneda . coyonedaToLanid
--   
coyonedaToLan :: Coyoneda f a -> Lan Identity f a lanToCoyoneda :: Lan Identity f a -> Coyoneda f a instance GHC.Base.Functor (Data.Functor.Coyoneda.Coyoneda f) instance Data.Functor.Bind.Class.Apply f => Data.Functor.Bind.Class.Apply (Data.Functor.Coyoneda.Coyoneda f) instance GHC.Base.Applicative f => GHC.Base.Applicative (Data.Functor.Coyoneda.Coyoneda f) instance GHC.Base.Alternative f => GHC.Base.Alternative (Data.Functor.Coyoneda.Coyoneda f) instance Data.Functor.Alt.Alt f => Data.Functor.Alt.Alt (Data.Functor.Coyoneda.Coyoneda f) instance Data.Functor.Plus.Plus f => Data.Functor.Plus.Plus (Data.Functor.Coyoneda.Coyoneda f) instance Data.Functor.Bind.Class.Bind m => Data.Functor.Bind.Class.Bind (Data.Functor.Coyoneda.Coyoneda m) instance GHC.Base.Monad m => GHC.Base.Monad (Data.Functor.Coyoneda.Coyoneda m) instance Control.Monad.Trans.Class.MonadTrans Data.Functor.Coyoneda.Coyoneda instance Control.Monad.Fix.MonadFix f => Control.Monad.Fix.MonadFix (Data.Functor.Coyoneda.Coyoneda f) instance GHC.Base.MonadPlus f => GHC.Base.MonadPlus (Data.Functor.Coyoneda.Coyoneda f) instance Data.Functor.Rep.Representable f => Data.Functor.Rep.Representable (Data.Functor.Coyoneda.Coyoneda f) instance Data.Functor.Extend.Extend w => Data.Functor.Extend.Extend (Data.Functor.Coyoneda.Coyoneda w) instance Control.Comonad.Comonad w => Control.Comonad.Comonad (Data.Functor.Coyoneda.Coyoneda w) instance Control.Comonad.Trans.Class.ComonadTrans Data.Functor.Coyoneda.Coyoneda instance Data.Foldable.Foldable f => Data.Foldable.Foldable (Data.Functor.Coyoneda.Coyoneda f) instance Data.Semigroup.Foldable.Class.Foldable1 f => Data.Semigroup.Foldable.Class.Foldable1 (Data.Functor.Coyoneda.Coyoneda f) instance Data.Traversable.Traversable f => Data.Traversable.Traversable (Data.Functor.Coyoneda.Coyoneda f) instance Data.Semigroup.Traversable.Class.Traversable1 f => Data.Semigroup.Traversable.Class.Traversable1 (Data.Functor.Coyoneda.Coyoneda f) instance Data.Distributive.Distributive f => Data.Distributive.Distributive (Data.Functor.Coyoneda.Coyoneda f) instance (GHC.Base.Functor f, GHC.Show.Show (f a)) => GHC.Show.Show (Data.Functor.Coyoneda.Coyoneda f a) instance (GHC.Base.Functor f, GHC.Read.Read (f a)) => GHC.Read.Read (Data.Functor.Coyoneda.Coyoneda f a) instance (GHC.Base.Functor f, GHC.Classes.Eq (f a)) => GHC.Classes.Eq (Data.Functor.Coyoneda.Coyoneda f a) instance (GHC.Base.Functor f, GHC.Classes.Ord (f a)) => GHC.Classes.Ord (Data.Functor.Coyoneda.Coyoneda f a) instance Data.Functor.Adjunction.Adjunction f g => Data.Functor.Adjunction.Adjunction (Data.Functor.Coyoneda.Coyoneda f) (Data.Functor.Coyoneda.Coyoneda g) -- | 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 data Density k a Density :: (k b -> a) -> k b -> Density k a -- | 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 . liftDensityid
--   
liftDensity :: Comonad w => w a -> Density w a -- | 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 . adjunctionToDensityid
--   adjunctionToDensity . densityToAdjunctionid
--   
densityToAdjunction :: Adjunction f g => Density f a -> f (g a) adjunctionToDensity :: Adjunction f g => f (g a) -> Density f a densityToLan :: Density f a -> Lan f f a -- | 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 . densityToLanid
--   densityToLan . lanToDensityid
--   
lanToDensity :: Lan f f a -> Density f a instance GHC.Base.Functor (Control.Comonad.Density.Density f) instance Data.Functor.Extend.Extend (Control.Comonad.Density.Density f) instance Control.Comonad.Comonad (Control.Comonad.Density.Density f) instance Control.Comonad.Trans.Class.ComonadTrans Control.Comonad.Density.Density instance Data.Functor.Bind.Class.Apply f => Data.Functor.Bind.Class.Apply (Control.Comonad.Density.Density f) instance GHC.Base.Applicative f => GHC.Base.Applicative (Control.Comonad.Density.Density f) -- | Monads from Comonads -- -- http://comonad.com/reader/2011/monads-from-comonads/ -- -- Co can be viewed as a right Kan lift along a Comonad. -- -- 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 type Co w = CoT w Identity co :: Functor w => (forall r. w (a -> r) -> r) -> Co w a runCo :: Functor w => Co w a -> w (a -> r) -> r -- |
--   Co w a ~ Rift w Identity a
--   
newtype CoT w m a CoT :: (forall r. w (a -> m r) -> m r) -> CoT w m a [runCoT] :: CoT w m a -> forall r. w (a -> m r) -> m r liftCoT0 :: Comonad w => (forall a. w a -> s) -> CoT w m s liftCoT0M :: (Comonad w, Monad m) => (forall a. w a -> m s) -> CoT w m s lowerCoT0 :: (Functor w, Monad m) => CoT w m s -> w a -> m s lowerCo0 :: Functor w => Co w s -> w a -> s liftCoT1 :: (forall a. w a -> a) -> CoT w m () liftCoT1M :: Monad m => (forall a. w a -> m a) -> CoT w m () lowerCoT1 :: (Functor w, Monad m) => CoT w m () -> w a -> m a lowerCo1 :: Functor w => Co w () -> w a -> a diter :: Functor f => a -> (a -> f a) -> Density (Cofree f) a dctrlM :: (Comonad w, Monad m) => (forall a. w a -> m (w a)) -> CoT (Density w) m () posW :: (ComonadStore s w, Monad m) => CoT w m s peekW :: (ComonadStore s w, Monad m) => s -> CoT w m () peeksW :: (ComonadStore s w, Monad m) => (s -> s) -> CoT w m () askW :: (ComonadEnv e w, Monad m) => CoT w m e asksW :: (ComonadEnv e w, Monad m) => (e -> a) -> CoT w m a traceW :: (ComonadTraced e w, Monad m) => e -> CoT w m () instance GHC.Base.Functor w => GHC.Base.Functor (Control.Monad.Co.CoT w m) instance Data.Functor.Extend.Extend w => Data.Functor.Bind.Class.Apply (Control.Monad.Co.CoT w m) instance Data.Functor.Extend.Extend w => Data.Functor.Bind.Class.Bind (Control.Monad.Co.CoT w m) instance Control.Comonad.Comonad w => GHC.Base.Applicative (Control.Monad.Co.CoT w m) instance Control.Comonad.Comonad w => GHC.Base.Monad (Control.Monad.Co.CoT w m) instance Control.Comonad.Comonad w => Control.Monad.Trans.Class.MonadTrans (Control.Monad.Co.CoT w) instance (Control.Comonad.Comonad w, Control.Monad.IO.Class.MonadIO m) => Control.Monad.IO.Class.MonadIO (Control.Monad.Co.CoT w m) instance (Control.Comonad.Comonad w, Control.Monad.Reader.Class.MonadReader e m) => Control.Monad.Reader.Class.MonadReader e (Control.Monad.Co.CoT w m) instance (Control.Comonad.Comonad w, Control.Monad.State.Class.MonadState s m) => Control.Monad.State.Class.MonadState s (Control.Monad.Co.CoT w m) instance (Control.Comonad.Comonad w, Control.Monad.Writer.Class.MonadWriter e m) => Control.Monad.Writer.Class.MonadWriter e (Control.Monad.Co.CoT w m) instance (Control.Comonad.Comonad w, Control.Monad.Error.Class.MonadError e m) => Control.Monad.Error.Class.MonadError e (Control.Monad.Co.CoT w m)