kan-extensions-5.1: Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads

Copyright(C) 2008-2016 Edward Kmett
LicenseBSD-style (see the file LICENSE)
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilitynon-portable (GADTs, MPTCs)
Safe HaskellSafe
LanguageHaskell98

Control.Comonad.Density

Description

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 (Lan f f) forms a Comonad. This is that Comonad.

Synopsis

Documentation

data Density k a where Source #

Constructors

Density :: (k b -> a) -> k b -> Density k a 

Instances

ComonadTrans (Density *) Source # 

Methods

lower :: Comonad w => Density * w a -> w a #

Functor (Density k f) Source # 

Methods

fmap :: (a -> b) -> Density k f a -> Density k f b #

(<$) :: a -> Density k f b -> Density k f a #

Applicative f => Applicative (Density * f) Source # 

Methods

pure :: a -> Density * f a #

(<*>) :: Density * f (a -> b) -> Density * f a -> Density * f b #

liftA2 :: (a -> b -> c) -> Density * f a -> Density * f b -> Density * f c #

(*>) :: Density * f a -> Density * f b -> Density * f b #

(<*) :: Density * f a -> Density * f b -> Density * f a #

Comonad (Density k f) Source # 

Methods

extract :: Density k f a -> a #

duplicate :: Density k f a -> Density k f (Density k f a) #

extend :: (Density k f a -> b) -> Density k f a -> Density k f b #

Apply f => Apply (Density * f) Source # 

Methods

(<.>) :: Density * f (a -> b) -> Density * f a -> Density * f b #

(.>) :: Density * f a -> Density * f b -> Density * f b #

(<.) :: Density * f a -> Density * f b -> Density * f a #

liftF2 :: (a -> b -> c) -> Density * f a -> Density * f b -> Density * f c #

Extend (Density k f) Source # 

Methods

duplicated :: Density k f a -> Density k f (Density k f a) #

extended :: (Density k f a -> b) -> Density k f a -> Density k f b #

liftDensity :: Comonad w => w a -> Density w a Source #

The natural transformation from a Comonad w to the Comonad generated by w (forwards).

This is merely a right-inverse (section) of lower, rather than a full inverse.

lower . liftDensityid

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 . adjunctionToDensityid
adjunctionToDensity . densityToAdjunctionid

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

densityToLan :: Density f a -> Lan f f a Source #

lanToDensity :: Lan f f a -> Density f a Source #

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 . densityToLanid
densityToLan . lanToDensityid