Copyright | 2013 Edward Kmett and Dan Doel |
---|---|

License | BSD |

Maintainer | Edward Kmett <ekmett@gmail.com> |

Stability | experimental |

Portability | rank N types |

Safe Haskell | Safe |

Language | Haskell98 |

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

- newtype Rift g h a = Rift {
- runRift :: forall r. g (a -> r) -> h r

- toRift :: (Functor g, Functor k) => (forall x. g (k x) -> h x) -> k a -> Rift g h a
- fromRift :: Adjunction f u => (forall a. k a -> Rift f h a) -> f (k b) -> h b
- grift :: Adjunction f u => f (Rift f k a) -> k a
- composeRift :: (Composition compose, Adjunction g u) => Rift f (Rift g h) a -> Rift (compose g f) h a
- decomposeRift :: (Composition compose, Functor f, Functor g) => Rift (compose g f) h a -> Rift f (Rift g h) a
- adjointToRift :: Adjunction f u => u a -> Rift f Identity a
- riftToAdjoint :: Adjunction f u => Rift f Identity a -> u a
- composedAdjointToRift :: (Functor h, Adjunction f u) => u (h a) -> Rift f h a
- riftToComposedAdjoint :: Adjunction f u => Rift f h a -> u (h a)
- liftRift :: Applicative f => f a -> Rift f f a
- lowerRift :: Applicative f => Rift f g a -> g a
- rap :: Functor f => Rift f g (a -> b) -> Rift g h a -> Rift f h b

# Right Kan lifts

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

, and since `Rift`

f `Identity`

is isomorphic to `Rift`

f f

, this is the `Rift`

f `Identity`

(f a)`Monad`

formed by the adjunction.

can be a `Rift`

`Identity`

m`Monad`

for any `Monad`

`m`

, as it is isomorphic to

.`Yoneda`

m

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

The universal property of `Rift`

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

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

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

`composeRift`

.`decomposeRift`

≡`id`

`decomposeRift`

.`composeRift`

≡`id`

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

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

`Rift f Identity a`

is isomorphic to the right adjoint to `f`

if one exists.

`adjointToRift`

.`riftToAdjoint`

≡`id`

`riftToAdjoint`

.`adjointToRift`

≡`id`

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

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

.`composedAdjointToRift`

≡`id`

`composedAdjointToRift`

.`riftToComposedAdjoint`

≡`id`

liftRift :: Applicative f => f a -> Rift f f a Source

lowerRift :: Applicative f => Rift f g a -> g a Source