-----------------------------------------------------------------------------
-- |
-- Module      :  Control.Functor.KanExtension
-- 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)
--
-- Left and right Kan extensions, expressed as higher order functors
--
-- Included is the 'monad generated by a functor' @Ran f f@
-- and the comonad cogenerated by a functor @Lan f f@
-- and machinery for lifting (co)monads into and lowering (co)monads out of 
-- Kan extensions.
----------------------------------------------------------------------------
module Control.Functor.KanExtension 
	( 
	-- * Right Kan Extensions
	  Ran(..)
	, toRan, fromRan
	, liftRan, lowerRan
	, adjointToRan, ranToAdjoint
	, ranToComposedAdjoint, composedAdjointToRan
	, composeRan, decomposeRan
	-- * Left Kan Extensions
	, Lan(..)
	, toLan, fromLan
	, liftLan, lowerLan
	, adjointToLan, lanToAdjoint
	, composeLan, decomposeLan
	, lanToComposedAdjoint, composedAdjointToLan
	-- * Performance tweaks for (co)free (co)monads
	, improveFree
	, worsenCofree
	) where

import Prelude hiding (abs)
import Control.Comonad.Context
import Control.Comonad.Cofree
import Control.Functor.Composition
import Control.Functor.Extras
import Control.Functor.Pointed ()
import Control.Functor.HigherOrder
import Control.Functor.Adjunction
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Identity
import Control.Monad.Free

-- | Right Kan Extension
newtype Ran g h a = Ran { runRan :: forall b. (a -> g b) -> h b }

-- | Nat(k `o` g, h) is isomorphic to Nat(k, Ran g h) (forwards)
toRan :: (Composition o, Functor k) => (k `o` g :~> h) -> k :~> Ran g h
toRan s t = Ran (s . compose . flip fmap t)

-- | Nat(k `o` g, h) is isomorphic to Nat(k, Ran g h) (backwards)
fromRan :: Composition o => (k :~> Ran g h) -> (k `o` g) :~> h
fromRan s = flip runRan id . s . decompose

instance HFunctor (Ran g) where
	hfmap f (Ran m) = Ran (f . m)
	ffmap f m = Ran (\k -> runRan m (k . f))

instance Functor (Ran g h) where
	fmap f m = Ran (\k -> runRan m (k . f))

instance Pointed (Ran f f) where
	point x = Ran (\k -> k x)

instance Monad (Ran f f) where
	return = point
	m >>= k = Ran (\c -> runRan m (\a -> runRan (k a) c))

-- | The natural isomorphism from @Ran f (Ran g h)@ to @Ran (f `o` g) h@ (forwards)
composeRan :: Composition o => Ran f (Ran g h) :~> Ran (f `o` g) h
composeRan r = Ran (\f -> runRan (runRan r (decompose . f)) id)

-- | The natural isomorphism from @Ran f (Ran g h)@ to @Ran (f `o` g) h@ (backwards)
decomposeRan :: (Functor f, Composition o) => Ran (f `o` g) h :~> Ran f (Ran g h)
decomposeRan r = Ran (\f -> Ran (\g -> runRan r (compose . fmap g . f)))

-- | Lift a monad into its right Kan extension along itself. This is the same operation
-- as is performed by Voightlaender's rep in <http://wwwtcs.inf.tu-dresden.de/%7Evoigt/mpc08.pdf>
-- and the ContT monad's lift operation. This is also viewable as the forward half of the 
-- natural isomorphism between a monad m and the monad generated by m.
liftRan :: Monad m => m a -> Ran m m a
liftRan m = Ran (m >>=)

-- | The natural isomorphism between a monad m and the monad generated by m (backwards)
lowerRan :: Monad m => Ran m m a -> m a 
lowerRan a = runRan a return

instance MonadReader r m => MonadReader r (Ran m m) where
	ask = liftRan ask
	local f m = Ran (\c -> ask >>= \r -> local f (runRan m (local (const r) . c)))

instance MonadIO m => MonadIO (Ran m m) where
	liftIO = liftRan . liftIO 

instance MonadState s m => MonadState s (Ran m m) where
	get = liftRan get
	put = liftRan . put

instance MonadFree f m => MonadFree f (Ran m m) where
        inFree t = Ran (inFree . flip fmap t . flip runRan)

-- | @f -| g@ iff @Ran g Identity@ exists (forward)
adjointToRan :: Adjunction f g => f :~> Ran g Identity
adjointToRan f = Ran (\a -> Identity $ rightAdjunct a f)

-- | @f -| g@ iff @Ran g Identity@ exists (backwards)
ranToAdjoint :: Adjunction f g => Ran g Identity :~> f
ranToAdjoint r = runIdentity (runRan r unit)

ranToComposedAdjoint :: (Composition o, Adjunction f g) => Ran g h :~> (h `o` f)
ranToComposedAdjoint r = compose (runRan r unit)

composedAdjointToRan :: (Functor h, Composition o, Adjunction f g) => (h `o` f) :~> Ran g h
composedAdjointToRan f = Ran (\a -> fmap (rightAdjunct a) (decompose f))

-- | Left Kan Extension
data Lan g h a = forall b. Lan (g b -> a) (h b)

-- | @Nat(h, f.g)@ is isomorphic to @Nat (Lan g h, f)@ (forwards)
toLan :: (Composition o, Functor f) => (h :~> (f `o` g)) -> Lan g h :~> f
toLan s (Lan f v) = fmap f . decompose $ s v

-- | @Nat(h, f.g)@ is isomorphic to @Nat (Lan g h, f)@ (backwards)
fromLan :: Composition o => (Lan g h :~> f) -> h :~> (f `o` g)
fromLan s = compose . s . Lan id

instance Functor g => HFunctor (Lan g) where
	ffmap f (Lan g h) = Lan (f . g) h
	hfmap f (Lan g h) = Lan g (f h)

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

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

instance Comonad (Lan f f) where
	duplicate (Lan f ws) = Lan (Lan f) ws

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

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

-- | f -| g iff Lan f Identity is inhabited (forwards)
adjointToLan :: Adjunction f g => g :~> Lan f Identity
adjointToLan = Lan counit . Identity

-- | f -| g iff Lan f Identity is inhabited (backwards)
lanToAdjoint :: Adjunction f g => Lan f Identity :~> g
lanToAdjoint (Lan f v) = leftAdjunct f (runIdentity v)

lanToComposedAdjoint :: (Functor h, Composition o, Adjunction f g) => Lan f h :~> (h `o` g)
lanToComposedAdjoint (Lan f v) = compose (fmap (leftAdjunct f) v)

composedAdjointToLan :: (Composition o, Adjunction f g) => (h `o` g) :~> Lan f h 
composedAdjointToLan = Lan counit . decompose

instance ComonadContext e m => ComonadContext e (Lan m m) where
        getC = getC . lowerLan 
	modifyC f = modifyC f . lowerLan

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

-- | the natural isomorphism from @Lan f (Lan g h)@ to @Lan (f `o` g) h@ (forwards)
composeLan :: (Functor f, Composition o) => Lan f (Lan g h) :~> Lan (f `o` g) h
composeLan (Lan f (Lan g h)) = Lan (f . fmap g . decompose) h

-- | the natural isomorphism from @Lan f (Lan g h)@ to @Lan (f `o` g) h@ (backwards)
decomposeLan :: Composition o => Lan (f `o` g) h :~> Lan f (Lan g h)
decomposeLan (Lan f h) = Lan (f . compose) (Lan id h)


-- | Voigtlaender's asymptotic performance improvement for free monads
improveFree :: Functor f => (forall m. MonadFree f m => m a) -> Free f a
improveFree m = lowerRan m

worsenCofree :: Functor f => (forall w. ComonadCofree f w => w a) -> Cofree f a
worsenCofree m = lowerLan m

-- data AnyCofree f a = forall w. ComonadCofree f w => AnyCofree { runAnyCofree :: w a }
-- coimprove :: Functor f => Cofree f a -> AnyCofree f a
-- coimprove m = AnyCofree (liftLan m)