-----------------------------------------------------------------------------
-- |
-- Module      :  Control.Comonad.Density
-- Copyright   :  (C) 2008 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- 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 
-- ''Formal Theory of Monads''.
----------------------------------------------------------------------------
module Control.Comonad.Density
	( Density(..)
	, densityToLan, lanToDensity
	, toDensity, fromDensity
	, liftDensity, lowerDensity
	, densityToAdjunction, adjunctionToDensity
	, densityToComposedAdjunction, composedAdjunctionToDensity
	, improveCofree
	) where

import Prelude hiding (abs)
import Control.Comonad.Context
import Control.Comonad.Cofree
import Control.Comonad.Trans
import Control.Comonad.Reader
import Control.Functor.Adjunction
import Control.Functor.Composition
import Control.Functor.Extras
import Control.Functor.Pointed ()
import Control.Functor.KanExtension
import Control.Monad.Identity

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

instance ComonadTrans Density where
	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

instance Comonad (Density f) where
	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)
densityToAdjunction (Density f v) = fmap (leftAdjunct f) v

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

densityToComposedAdjunction :: (Composition o, Adjunction f g) => Density f :~> (f `o` g)
densityToComposedAdjunction (Density f v) = compose (fmap (leftAdjunct f) v)

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

instance ComonadReader e w => ComonadReader e (Density w) where
	askC = askC . lowerDensity

instance ComonadContext e w => ComonadContext e (Density w) where
        getC = getC . lowerDensity 
	modifyC f = modifyC f . lowerDensity

instance ComonadCofree f w => ComonadCofree f (Density w) where
        outCofree (Density f c) = fmap (Density f) (outCofree c)

instance RunComonadCofree f w => RunComonadCofree f (Density w) where
	anaCofree l r = liftDensity . anaCofree l r

improveCofree :: Functor f => (forall w. ComonadCofree f w => w a) -> Cofree f a
improveCofree m = lowerDensity m