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

Portability rank N types experimental Edward Kmett Trustworthy

Data.Functor.Kan.Rift

Contents

Description

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

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

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 Identity m` can be a `Monad` for any `Monad` `m`, as it is isomorphic to `Yoneda m`.

Constructors

 Rift FieldsrunRift :: 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` . `fromRift` ≡ `id`
`fromRift` . `toRift` ≡ `id`
```

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

``` `composeRift` . `decomposeRift` ≡ `id`
`decomposeRift` . `composeRift` ≡ `id`
```

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` . `riftToAdjoint` ≡ `id`
`riftToAdjoint` . `adjointToRift` ≡ `id`
```

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` . `composedAdjointToRift` ≡ `id`
`composedAdjointToRift` . `riftToComposedAdjoint` ≡ `id`
```

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

Indexed applicative composition of right Kan lifts.