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 f
Comonad
. This is
that
Comonad
.
Synopsis
- 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
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 #
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
.densityToLan
≡id
densityToLan
.lanToDensity
≡id