```-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2008 Edward Kmett
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  experimental
-- Portability :  non-portable (rank-2 polymorphism)
--
-- The density comonad for a functor. aka the comonad cogenerated 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
----------------------------------------------------------------------------
( Density(..)
, densityToLan, lanToDensity
, toDensity, fromDensity
, liftDensity, lowerDensity
, improveCofree
) where

import Prelude hiding (abs)
import Control.Functor.Composition
import Control.Functor.Extras
import Control.Functor.Pointed ()
import Control.Functor.KanExtension

data Density k a = forall b. Density (k b -> a) (k b)

densityToLan :: Density k a -> Lan k k a
densityToLan (Density f v) = Lan f v

lanToDensity :: Lan k k a -> Density k a
lanToDensity (Lan f v) = Density f v

-- | @Nat(k, s.k)@ is isomorphic to @Nat (Density k, s)@ (forwards)
toDensity :: Functor s => (forall a. k a -> s (k a)) -> Density k :~> s
toDensity s (Density f v) = fmap f \$ s v

-- | @Nat(k, s.k)@ is isomorphic to @Nat (Density k, s)@ (backwards)
fromDensity :: (Density k :~> s) -> k a -> s (k a)
fromDensity s = s . Density id

colift = liftDensity

instance Functor (Density f) where
fmap f (Density g h) = Density (f . g) h

instance Copointed (Density f) where
extract (Density f a) = f a

duplicate (Density f ws) = Density (Density f) ws

-- | The natural isomorphism between a comonad w and the comonad generated by w (forwards).
liftDensity :: Comonad w => w a -> Density w a
liftDensity = Density extract

-- | The natural isomorphism between a comonad w and the comonad generated by w (backwards).
lowerDensity :: Comonad w => Density w a -> w a
lowerDensity (Density f c) = extend f c

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

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

densityToComposedAdjunction :: (Composition o, Adjunction f g) => Density f :~> (f `o` g)

composedAdjunctionToDensity :: (Composition o, Adjunction f g) => (f `o` g) :~> Density f
composedAdjunctionToDensity = Density counit . decompose