{-# LANGUAGE Rank2Types, GADTs #-}
-------------------------------------------------------------------------------------------
-- |
-- Module	: Data.Functor.KanExtension
-- Copyright 	: 2008-2011 Edward Kmett
-- License	: BSD
--
-- Maintainer	: Edward Kmett <ekmett@gmail.com>
-- Stability	: experimental
-- Portability	: rank 2 types
--
-------------------------------------------------------------------------------------------
module Data.Functor.KanExtension where

import Data.Functor.Identity
import Data.Functor.Adjunction
import Data.Functor.Composition
import Data.Functor.Apply
import Control.Applicative

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

instance Functor (Ran g h) where
  fmap f m = Ran (\k -> runRan m (k . f))
 
-- | 'toRan' and 'fromRan' witness a higher kinded adjunction. from @(`'Compose'` g)@ to @'Ran' g@
toRan :: (Composition compose, Functor k) => (forall a. compose k g a -> h a) -> k b -> Ran g h b
toRan s t = Ran (s . compose . flip fmap t)

fromRan :: Composition compose => (forall a. k a -> Ran g h a) -> compose k g b -> h b
fromRan s = flip runRan id . s . decompose

composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a
composeRan r = Ran (\f -> runRan (runRan r (decompose . f)) id)

decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) a
decomposeRan r = Ran (\f -> Ran (\g -> runRan r (compose . fmap g . f)))

adjointToRan :: Adjunction f g => f a -> Ran g Identity a
adjointToRan f = Ran (\a -> Identity $ rightAdjunct a f)

ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a
ranToAdjoint r = runIdentity (runRan r unit)

ranToComposedAdjoint :: (Composition compose, Adjunction f g) => Ran g h a -> compose h f a
ranToComposedAdjoint r = compose (runRan r unit)

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

data Lan g h a where
  Lan :: (g b -> a) -> h b -> Lan g h a

-- 'fromLan' and 'toLan' witness a (higher kinded) adjunction between @'Lan' g@ and @(`Compose` g)@
toLan :: (Composition compose, Functor f) => (forall a. h a -> compose f g a) -> Lan g h b -> f b
toLan s (Lan f v) = fmap f . decompose $ s v

fromLan :: (Composition compose) => (forall a. Lan g h a -> f a) -> h b -> compose f g b
fromLan s = compose . s . Lan id

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

instance (Functor g, Apply h) => Apply (Lan g h) where
  Lan kxf x <.> Lan kya y =
    Lan (\k -> kxf (fmap fst k) (kya (fmap snd k))) ((,) <$> x <.> y)

instance (Functor g, Applicative h) => Applicative (Lan g h) where
  pure a = Lan (const a) (pure ())
  Lan kxf x <*> Lan kya y =
    Lan (\k -> kxf (fmap fst k) (kya (fmap snd k))) (liftA2 (,) x y)

adjointToLan :: Adjunction f g => g a -> Lan f Identity a
adjointToLan = Lan counit . Identity

lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a
lanToAdjoint (Lan f v) = leftAdjunct f (runIdentity v)

-- | 'lanToComposedAdjoint' and 'composedAdjointToLan' witness the natural isomorphism between @Lan f h@ and @Compose h g@ given @f -| g@
lanToComposedAdjoint :: (Composition compose, Functor h, Adjunction f g) => Lan f h a -> compose h g a
lanToComposedAdjoint (Lan f v) = compose (fmap (leftAdjunct f) v)

composedAdjointToLan :: Composition compose => Adjunction f g => compose h g a -> Lan f h a
composedAdjointToLan = Lan counit . decompose

-- | 'composeLan' and 'decomposeLan' witness the natural isomorphism from @Lan f (Lan g h)@ and @Lan (f `o` g) h@
composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h a
composeLan (Lan f (Lan g h)) = Lan (f . fmap g . decompose) h

decomposeLan :: Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) a
decomposeLan (Lan f h) = Lan (f . compose) (Lan id h)