kan-extensions-3.4: Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads

Portabilityrank N types
Stabilityexperimental
MaintainerEdward Kmett <ekmett@gmail.com>
Safe HaskellTrustworthy

Data.Functor.KanLift

Contents

Description

Right and Left Kan lifts for functors over Hask, where they exist.

http://ncatlab.org/nlab/show/Kan+lift

Synopsis

Right Kan lifts

newtype Rift g h a Source

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 ~ 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.

Constructors

Rift 

Fields

runRift :: forall r. g (a -> r) -> h r
 

Instances

Functor g => Functor (Rift g h) 
(Functor g, ~ (* -> *) g h) => Applicative (Rift g h) 
(Functor g, ~ (* -> *) g h) => Pointed (Rift g h) 

toRift :: (Functor g, Functor k) => (forall x. g (k x) -> h x) -> k a -> Rift g h aSource

The universal property of Rift

fromRift :: Adjunction f u => (forall a. k a -> Rift f h a) -> f (k b) -> h bSource

When f -| u, then f -| Rift f Identity and

 toRift . fromRiftid
 fromRift . toRiftid

grift :: Adjunction f u => f (Rift f k a) -> k aSource

composeRift :: (Composition compose, Adjunction g u) => Rift f (Rift g h) a -> Rift (compose g f) h aSource

decomposeRift :: (Composition compose, Functor f, Functor g) => Rift (compose g f) h a -> Rift f (Rift g h) aSource

adjointToRift :: Adjunction f u => u a -> Rift f Identity aSource

Rift f Identity a is isomorphic to the right adjoint to f if one exists.

 adjointToRift . riftToAdjointid
 riftToAdjoint . adjointToRiftid

riftToAdjoint :: Adjunction f u => Rift f Identity a -> u aSource

Rift f Identity a is isomorphic to the right adjoint to f if one exists.

composedAdjointToRift :: (Functor h, Adjunction f u) => u (h a) -> Rift f h aSource

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 :: Adjunction f u => Rift f h a -> u (h a)Source

| 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 . composedAdjointToRiftid
 composedAdjointToRift . riftToComposedAdjointid

rap :: Functor f => Rift f g (a -> b) -> Rift g h a -> Rift f h bSource

Indexed applicative composition of right Kan lifts.

Left Kan lifts

newtype Lift g f a Source

 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.

Constructors

Lift 

Fields

runLift :: forall z. Functor z => (forall x. f x -> g (z x)) -> z a
 

Instances

Functor (Lift g h) 
(Functor g, ~ (* -> *) g h) => Copointed (Lift g h) 

toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z bSource

The universal property of Lift

fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b)Source

When the adjunction exists

 fromLift . toLiftid
 toLift . fromLiftid

glift :: Adjunction l g => k a -> g (Lift g k a)Source

f => g (Lift g f a)

composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h aSource

decomposeLift :: (Composition compose, Adjunction l g) => Lift (compose g f) h a -> Lift f (Lift g h) aSource

adjointToLift :: Adjunction f u => f a -> Lift u Identity aSource

Lift u Identity a is isomorphic to the left adjoint to u if one exists.

 adjointToLift . liftToAdjointid
 liftToAdjoint . adjointToLiftid

liftToAdjoint :: Adjunction f u => Lift u Identity a -> f aSource

Lift u Identity a is isomorphic to the left adjoint to u if one exists.

liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a)Source

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 . composedAdjointToLiftid
 composedAdjointToLift . liftToComposedAdjointid

composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h aSource

Lift u h a is isomorphic to the post-composition of the left adjoint of u onto h if such a left adjoint exists.