kan-extensions-4.0.3: Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads

Portability non-portable (rank-2 polymorphism) provisional Edward Kmett Trustworthy

Description

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

Synopsis

type Co w = CoT w IdentitySource

co :: Functor w => (forall r. w (a -> r) -> r) -> Co w aSource

runCo :: Functor w => Co w a -> w (a -> r) -> rSource

newtype CoT w m a Source

``` `Co` w a ~ `Rift` w `Identity` a
```

Constructors

 CoT FieldsrunCoT :: forall r. w (a -> m r) -> m r

Instances

Klesili from CoKleisli

liftCoT0 :: Comonad w => (forall a. w a -> s) -> CoT w m sSource

liftCoT0M :: (Comonad w, Monad m) => (forall a. w a -> m s) -> CoT w m sSource

lowerCoT0 :: (Functor w, Monad m) => CoT w m s -> w a -> m sSource

lowerCo0 :: Functor w => Co w s -> w a -> sSource

liftCoT1 :: (forall a. w a -> a) -> CoT w m ()Source

liftCoT1M :: Monad m => (forall a. w a -> m a) -> CoT w m ()Source

lowerCoT1 :: (Functor w, Monad m) => CoT w m () -> w a -> m aSource

lowerCo1 :: Functor w => Co w () -> w a -> aSource

diter :: Functor f => a -> (a -> f a) -> Density (Cofree f) aSource

dctrlM :: (Comonad w, Monad m) => (forall a. w a -> m (w a)) -> CoT (Density w) m ()Source

posW :: (ComonadStore s w, Monad m) => CoT w m sSource

peekW :: (ComonadStore s w, Monad m) => s -> CoT w m ()Source

peeksW :: (ComonadStore s w, Monad m) => (s -> s) -> CoT w m ()Source