Modulekan-extensions-5.2.8Haskell2010

Control.Comonad.Density

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 generated 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.

1 type
5 values

Packagekan-extensions-5.2.8
Exports6
LanguageHaskell2010
LicenceBSD-3-Clause
SourceDensity.hs

datadata Density (k1 :: k -> Type) a where

Constructors

Density :: (k2 b -> a) -> k2 b -> Density k1 a

Instances6ComonadTrans, Functor, Applicative, Comonad, Apply, Extend

ComonadTrans DensityDefined in kan-extensions-5.2.8 · Control.Comonad.Density
Functor (Density f)Defined in kan-extensions-5.2.8 · Control.Comonad.Density
Applicative f => Applicative (Density f)Defined in kan-extensions-5.2.8 · Control.Comonad.Density
Comonad (Density f)Defined in kan-extensions-5.2.8 · Control.Comonad.Density
Apply f => Apply (Density f)Defined in kan-extensions-5.2.8 · Control.Comonad.Density
Extend (Density f)Defined in kan-extensions-5.2.8 · Control.Comonad.Density

valueliftDensity :: Comonad w => w a -> Density w a

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 . liftDensity ≡ id

valuedensityToAdjunction :: Adjunction f g => Density f a -> f (g a)

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

valueadjunctionToDensity :: Adjunction f g => f (g a) -> Density f a

valuedensityToLan :: Density f a -> Lan f f a

valuelanToDensity :: Lan f f a -> Density f a

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