Copyright | 2008-2016 Edward Kmett |
---|---|

License | BSD |

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

Stability | experimental |

Portability | rank 2 types |

Safe Haskell | Trustworthy |

Language | Haskell98 |

- Right Kan Extensions

- newtype Ran g h a = Ran {
- runRan :: forall b. (a -> g b) -> h b

- toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b
- fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b
- gran :: Ran g h (g a) -> h a
- 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 :: 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
- 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)

# Documentation

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

exists.`gran`

:: Ran g h (g a) -> h a

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.

toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b #

The universal property of a right Kan extension.

gran :: Ran g h (g a) -> h a #

This is the natural transformation that defines a Right Kan extension.

composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a #

`composeRan`

.`decomposeRan`

≡`id`

`decomposeRan`

.`composeRan`

≡`id`

decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) a #

adjointToRan :: Adjunction f g => f a -> Ran g Identity a #

`adjointToRan`

.`ranToAdjoint`

≡`id`

`ranToAdjoint`

.`adjointToRan`

≡`id`

ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a #

composedAdjointToRan :: (Adjunction f g, Functor h) => h (f a) -> Ran g h a #

ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f 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) #