content: {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE TypeOperators #-}
  -------------------------------------------------------------------------------------------
  -- |
  -- Copyright 	: 2013-2016 Edward Kmett and Dan Doel
  -- License	: BSD
  --
  -- Maintainer	: Edward Kmett <ekmett@gmail.com>
  -- Stability	: experimental
  -- Portability	: rank N types
  --
  -- @'Day' f -| 'Curried' f@
  --
  -- @'Day' f ~ 'Compose' f@ when f preserves colimits / is a left adjoint. (Due in part to the
  -- strength of all functors in Hask.)
  --
  -- So by the uniqueness of adjoints, when f is a left adjoint, @'Curried' f ~ 'Rift' f@
  -------------------------------------------------------------------------------------------
  module Data.Functor.Day.Curried
    (
    -- * Right Kan lifts
      Curried(..)
    , toCurried, fromCurried, applied, unapplied
    , adjointToCurried, curriedToAdjoint
    , composedAdjointToCurried, curriedToComposedAdjoint
    , liftCurried, lowerCurried, rap
    ) where
  
  import qualified Control.Applicative as App
  import Data.Functor.Adjunction
  import Data.Functor.Day
  import Data.Functor.Identity
  import Data.Functor.Apply
  
  newtype Curried g h a =
    Curried { runCurried :: forall r. g (a -> r) -> h r }
  
  instance Functor g => Functor (Curried g h) where
    fmap f (Curried g) = Curried (g . fmap (.f))
    {-# INLINE fmap #-}
  
  instance (Functor g, g ~ h) => Apply (Curried g h) where
    Curried mf <.> Curried ma = Curried (ma . mf . fmap (.))
    {-# INLINE (<.>) #-}
    liftF2 f (Curried g) (Curried ma) = Curried (ma . g . fmap (\p q -> p . f q))
    {-# INLINE liftF2 #-}
  
  instance (Functor g, g ~ h) => App.Applicative (Curried g h) where
    pure a = Curried (fmap ($ a))
    {-# INLINE pure #-}
    Curried mf <*> Curried ma = Curried (ma . mf . fmap (.))
    {-# INLINE (<*>) #-}
    liftA2 f (Curried g) (Curried ma) = Curried (ma . g . fmap (\p q -> p . f q))
    {-# INLINE liftA2 #-}
  
  -- | The natural isomorphism between @f@ and @Curried f f@.
  -- @
  -- 'lowerCurried' '.' 'liftCurried' ≡ 'id'
  -- 'liftCurried' '.' 'lowerCurried' ≡ 'id'
  -- @
  --
  -- @
  -- 'lowerCurried' ('liftCurried' x)     -- definition
  -- 'lowerCurried' ('Curried' ('<*>' x))   -- definition
  -- ('<*>' x) ('pure' 'id')          -- beta reduction
  -- 'pure' 'id' '<*>' x              -- Applicative identity law
  -- x
  -- @
  liftCurried :: Applicative f => f a -> Curried f f a
  liftCurried fa = Curried (<*> fa)
  {-# INLINE liftCurried #-}
  
  -- | Lower 'Curried' by applying 'pure' 'id' to the continuation.
  --
  -- See 'liftCurried'.
  lowerCurried :: Applicative f => Curried f g a -> g a
  lowerCurried (Curried f) = f (pure id)
  {-# INLINE lowerCurried #-}
  
  -- | Indexed applicative composition of right Kan lifts.
  rap :: Functor f => Curried f g (a -> b) -> Curried g h a -> Curried f h b
  rap (Curried mf) (Curried ma) = Curried (ma . mf . fmap (.))
  {-# INLINE rap #-}
  
  -- | This is the counit of the @Day f -| Curried f@ adjunction
  applied :: Functor f => Day f (Curried f g) a -> g a
  applied (Day fb (Curried fg) bca) = fg (bca <$> fb)
  {-# INLINE applied #-}
  
  -- | This is the unit of the @Day f -| Curried f@ adjunction
  unapplied :: g a -> Curried f (Day f g) a
  unapplied ga = Curried $ \ fab -> Day fab ga id
  {-# INLINE unapplied #-}
  
  -- | The universal property of 'Curried'
  toCurried :: (forall x. Day g k x -> h x) -> k a -> Curried g h a
  toCurried h ka = Curried $ \gar -> h (Day gar ka id)
  {-# INLINE toCurried #-}
  
  -- |
  -- @
  -- 'toCurried' . 'fromCurried' ≡ 'id'
  -- 'fromCurried' . 'toCurried' ≡ 'id'
  -- @
  fromCurried :: Functor f => (forall a. k a -> Curried f h a) -> Day f k b -> h b
  fromCurried f (Day fc kd cdb) = runCurried (f kd) (cdb <$> fc)
  {-# INLINE fromCurried #-}
  
  -- | @Curried f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
  --
  -- @
  -- 'adjointToCurried' . 'curriedToAdjoint' ≡ 'id'
  -- 'curriedToAdjoint' . 'adjointToCurried' ≡ 'id'
  -- @
  adjointToCurried :: Adjunction f u => u a -> Curried f Identity a
  adjointToCurried ua = Curried (Identity . rightAdjunct (<$> ua))
  {-# INLINE adjointToCurried #-}
  
  -- | @Curried f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
  curriedToAdjoint :: Adjunction f u => Curried f Identity a -> u a
  curriedToAdjoint (Curried m) = leftAdjunct (runIdentity . m) id
  {-# INLINE curriedToAdjoint #-}
  
  -- | @Curried f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
  --
  -- @
  -- 'curriedToComposedAdjoint' . 'composedAdjointToCurried' ≡ 'id'
  -- 'composedAdjointToCurried' . 'curriedToComposedAdjoint' ≡ 'id'
  -- @
  
  curriedToComposedAdjoint :: Adjunction f u => Curried f h a -> u (h a)
  curriedToComposedAdjoint (Curried m) = leftAdjunct m id
  {-# INLINE curriedToComposedAdjoint #-}
  
  -- | @Curried f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
  composedAdjointToCurried :: (Functor h, Adjunction f u) => u (h a) -> Curried f h a
  composedAdjointToCurried uha = Curried $ rightAdjunct (\b -> fmap b <$> uha)
  {-# INLINE composedAdjointToCurried #-}
  
  