Copyright | (C) 2008-2016 Edward Kmett |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Stability | experimental |
Portability | non-portable (GADTs, MPTCs) |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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 (
) forms a Lan
f fComonad
. This is
that Comonad
.
Synopsis
- data Density (k1 :: k -> Type) 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 :: forall {k} (f :: k -> Type) a. Density f a -> Lan f f a
- lanToDensity :: forall {k} (f :: k -> Type) a. Lan f f a -> Density f a
Documentation
liftDensity :: Comonad w => w a -> Density w a Source #
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 a Source #
lanToDensity :: forall {k} (f :: k -> Type) a. 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
.densityToLan
≡id
densityToLan
.lanToDensity
≡id