Portability | non-portable (GADTs, MPTCs) |
---|---|

Stability | experimental |

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

Safe Haskell | Trustworthy |

The `Density`

`Comonad`

for a `Functor`

(aka the 'Comonad generated by a `Functor`

)
The `Density`

term dates back to Dubuc''s 1974 thesis. The term
`Monad`

genererated by a `Functor`

dates back to 1972 in Street''s
''Formal Theory of Monads''.

The left Kan extension of a `Functor`

along itself (

) forms a `Lan`

f f`Comonad`

. This is
that `Comonad`

.

- data Density k a where
- liftDensity :: Comonad w => w a -> Density w a
- densityToAdjunction :: Adjunction f g => Density f a -> f (g a)
- adjunctionToDensity :: Adjunction f g => f (g a) -> Density f a
- densityToLan :: Density f a -> Lan f f a
- lanToDensity :: Lan f f a -> Density f a

# Documentation

ComonadTrans Density | |

Functor (Density f) | |

Applicative f => Applicative (Density f) | |

Comonad (Density f) | |

Apply f => Apply (Density f) | |

Extend (Density f) |

liftDensity :: Comonad w => w a -> Density w aSource

densityToAdjunction :: Adjunction f g => Density f a -> f (g a)Source

The Density `Comonad`

of a left adjoint is isomorphic to the `Comonad`

formed by that `Adjunction`

.

This isomorphism is witnessed by `densityToAdjunction`

and `adjunctionToDensity`

.

`densityToAdjunction`

.`adjunctionToDensity`

≡`id`

`adjunctionToDensity`

.`densityToAdjunction`

≡`id`

adjunctionToDensity :: Adjunction f g => f (g a) -> Density f aSource

densityToLan :: Density f a -> Lan f f aSource

lanToDensity :: Lan f f a -> Density f aSource

The `Density`

`Comonad`

of a `Functor`

`f`

is obtained by taking the left Kan extension
(`Lan`

) of `f`

along itself. This isomorphism is witnessed by `lanToDensity`

and `densityToLan`

`lanToDensity`

.`densityToLan`

≡`id`

`densityToLan`

.`lanToDensity`

≡`id`