    {-# 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 { forall (g :: * -> *) (h :: * -> *) a.
    Curried g h a -> forall r. g (a -> r) -> h r
    runCurried :: forall r. g (a -> r) -> h r }

    instance Functor g => Functor (Curried g h) where
      fmap :: forall a b. (a -> b) -> Curried g h a -> Curried g h b
    fmap a -> b
    f (Curried forall r. g (a -> r) -> h r
    g) = (forall r. g (b -> r) -> h r) -> Curried g h b
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried (g (a -> r) -> h r
    forall r. g (a -> r) -> h r
    g (g (a -> r) -> h r)
    -> (g (b -> r) -> g (a -> r)) -> g (b -> r) -> h r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((b -> r) -> a -> r) -> g (b -> r) -> g (a -> r)
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((b -> r) -> (a -> b) -> a -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .a -> b
    f))
      {-# INLINE fmap #-}

    instance (Functor g, g ~ h) => Apply (Curried g h) where
      Curried forall r. g ((a -> b) -> r) -> h r
    mf <.> :: forall a b. Curried g h (a -> b) -> Curried g h a -> Curried g h b
    <.> Curried forall r. g (a -> r) -> h r
    ma = (forall r. g (b -> r) -> h r) -> Curried g h b
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried (g (a -> r) -> h r
    forall r. g (a -> r) -> h r
    ma (g (a -> r) -> h r)
    -> (g (b -> r) -> g (a -> r)) -> g (b -> r) -> h r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . g ((a -> b) -> a -> r) -> g (a -> r)
    g ((a -> b) -> a -> r) -> h (a -> r)
    forall r. g ((a -> b) -> r) -> h r
    mf (g ((a -> b) -> a -> r) -> g (a -> r))
    -> (g (b -> r) -> g ((a -> b) -> a -> r))
    -> g (b -> r)
    -> g (a -> r)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((b -> r) -> (a -> b) -> a -> r)
    -> g (b -> r) -> g ((a -> b) -> a -> r)
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (b -> r) -> (a -> b) -> a -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.))
      {-# INLINE (<.>) #-}
      liftF2 :: forall a b c.
    (a -> b -> c) -> Curried g h a -> Curried g h b -> Curried g h c
    liftF2 a -> b -> c
    f (Curried forall r. g (a -> r) -> h r
    g) (Curried forall r. g (b -> r) -> h r
    ma) = (forall r. g (c -> r) -> h r) -> Curried g h c
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried (g (b -> r) -> h r
    forall r. g (b -> r) -> h r
    ma (g (b -> r) -> h r)
    -> (g (c -> r) -> g (b -> r)) -> g (c -> r) -> h r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . g (a -> b -> r) -> g (b -> r)
    g (a -> b -> r) -> h (b -> r)
    forall r. g (a -> r) -> h r
    g (g (a -> b -> r) -> g (b -> r))
    -> (g (c -> r) -> g (a -> b -> r)) -> g (c -> r) -> g (b -> r)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((c -> r) -> a -> b -> r) -> g (c -> r) -> g (a -> b -> r)
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\c -> r
    p a
    q -> c -> r
    p (c -> r) -> (b -> c) -> b -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> b -> c
    f a
    q))
      {-# INLINE liftF2 #-}

    instance (Functor g, g ~ h) => App.Applicative (Curried g h) where
      pure :: forall a. a -> Curried g h a
    pure a
    a = (forall r. g (a -> r) -> h r) -> Curried g h a
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried (((a -> r) -> r) -> g (a -> r) -> g r
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a -> r) -> a -> r
    forall a b. (a -> b) -> a -> b
    $ a
    a))
      {-# INLINE pure #-}
      Curried forall r. g ((a -> b) -> r) -> h r
    mf <*> :: forall a b. Curried g h (a -> b) -> Curried g h a -> Curried g h b
    <*> Curried forall r. g (a -> r) -> h r
    ma = (forall r. g (b -> r) -> h r) -> Curried g h b
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried (g (a -> r) -> h r
    forall r. g (a -> r) -> h r
    ma (g (a -> r) -> h r)
    -> (g (b -> r) -> g (a -> r)) -> g (b -> r) -> h r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . g ((a -> b) -> a -> r) -> g (a -> r)
    g ((a -> b) -> a -> r) -> h (a -> r)
    forall r. g ((a -> b) -> r) -> h r
    mf (g ((a -> b) -> a -> r) -> g (a -> r))
    -> (g (b -> r) -> g ((a -> b) -> a -> r))
    -> g (b -> r)
    -> g (a -> r)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((b -> r) -> (a -> b) -> a -> r)
    -> g (b -> r) -> g ((a -> b) -> a -> r)
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (b -> r) -> (a -> b) -> a -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.))
      {-# INLINE (<*>) #-}
      liftA2 :: forall a b c.
    (a -> b -> c) -> Curried g h a -> Curried g h b -> Curried g h c
    liftA2 a -> b -> c
    f (Curried forall r. g (a -> r) -> h r
    g) (Curried forall r. g (b -> r) -> h r
    ma) = (forall r. g (c -> r) -> h r) -> Curried g h c
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried (g (b -> r) -> h r
    forall r. g (b -> r) -> h r
    ma (g (b -> r) -> h r)
    -> (g (c -> r) -> g (b -> r)) -> g (c -> r) -> h r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . g (a -> b -> r) -> g (b -> r)
    g (a -> b -> r) -> h (b -> r)
    forall r. g (a -> r) -> h r
    g (g (a -> b -> r) -> g (b -> r))
    -> (g (c -> r) -> g (a -> b -> r)) -> g (c -> r) -> g (b -> r)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((c -> r) -> a -> b -> r) -> g (c -> r) -> g (a -> b -> r)
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\c -> r
    p a
    q -> c -> r
    p (c -> r) -> (b -> c) -> b -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> b -> c
    f a
    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 :: forall (f :: * -> *) a. Applicative f => f a -> Curried f f a
    liftCurried f a
    fa = (forall r. f (a -> r) -> f r) -> Curried f f a
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried (f (a -> r) -> f a -> f r
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> f a
    fa)
    {-# INLINE liftCurried #-}

    -- | Lower 'Curried' by applying 'pure' 'id' to the continuation.
    --
    -- See 'liftCurried'.
    lowerCurried :: Applicative f => Curried f g a -> g a
    lowerCurried :: forall (f :: * -> *) (g :: * -> *) a.
    Applicative f =>
    Curried f g a -> g a
    lowerCurried (Curried forall r. f (a -> r) -> g r
    f) = f (a -> a) -> g a
    forall r. f (a -> r) -> g r
    f ((a -> a) -> f (a -> a)
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a -> a
    forall a. a -> a
    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 :: forall (f :: * -> *) (g :: * -> *) a b (h :: * -> *).
    Functor f =>
    Curried f g (a -> b) -> Curried g h a -> Curried f h b
    rap (Curried forall r. f ((a -> b) -> r) -> g r
    mf) (Curried forall r. g (a -> r) -> h r
    ma) = (forall r. f (b -> r) -> h r) -> Curried f h b
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried (g (a -> r) -> h r
    forall r. g (a -> r) -> h r
    ma (g (a -> r) -> h r)
    -> (f (b -> r) -> g (a -> r)) -> f (b -> r) -> h r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f ((a -> b) -> a -> r) -> g (a -> r)
    forall r. f ((a -> b) -> r) -> g r
    mf (f ((a -> b) -> a -> r) -> g (a -> r))
    -> (f (b -> r) -> f ((a -> b) -> a -> r))
    -> f (b -> r)
    -> g (a -> r)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((b -> r) -> (a -> b) -> a -> r)
    -> f (b -> r) -> f ((a -> b) -> a -> r)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (b -> r) -> (a -> b) -> a -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.))
    {-# 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 :: forall (f :: * -> *) (g :: * -> *) a.
    Functor f =>
    Day f (Curried f g) a -> g a
    applied (Day f b
    fb (Curried forall r. f (c -> r) -> g r
    fg) b -> c -> a
    bca) = f (c -> a) -> g a
    forall r. f (c -> r) -> g r
    fg (b -> c -> a
    bca (b -> c -> a) -> f b -> f (c -> a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f b
    fb)
    {-# INLINE applied #-}

    -- | This is the unit of the @Day f -| Curried f@ adjunction
    unapplied :: g a -> Curried f (Day f g) a
    unapplied :: forall (g :: * -> *) a (f :: * -> *). g a -> Curried f (Day f g) a
    unapplied g a
    ga = (forall r. f (a -> r) -> Day f g r) -> Curried f (Day f g) a
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried ((forall r. f (a -> r) -> Day f g r) -> Curried f (Day f g) a)
    -> (forall r. f (a -> r) -> Day f g r) -> Curried f (Day f g) a
    forall a b. (a -> b) -> a -> b
    $ \ f (a -> r)
    fab -> f (a -> r) -> g a -> ((a -> r) -> a -> r) -> Day f g r
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day f (a -> r)
    fab g a
    ga (a -> r) -> a -> r
    forall a. a -> a
    id
    {-# INLINE unapplied #-}

    -- | The universal property of 'Curried'
    toCurried :: (forall x. Day g k x -> h x) -> k a -> Curried g h a
    toCurried :: forall (g :: * -> *) (k :: * -> *) (h :: * -> *) a.
    (forall x. Day g k x -> h x) -> k a -> Curried g h a
    toCurried forall x. Day g k x -> h x
    h k a
    ka = (forall r. g (a -> r) -> h r) -> Curried g h a
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried ((forall r. g (a -> r) -> h r) -> Curried g h a)
    -> (forall r. g (a -> r) -> h r) -> Curried g h a
    forall a b. (a -> b) -> a -> b
    $ \g (a -> r)
    gar -> Day g k r -> h r
    forall x. Day g k x -> h x
    h (g (a -> r) -> k a -> ((a -> r) -> a -> r) -> Day g k r
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Day g (a -> r)
    gar k a
    ka (a -> r) -> a -> r
    forall a. a -> a
    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 :: forall (f :: * -> *) (k :: * -> *) (h :: * -> *) b.
    Functor f =>
    (forall a. k a -> Curried f h a) -> Day f k b -> h b
    fromCurried forall a. k a -> Curried f h a
    f (Day f b
    fc k c
    kd b -> c -> b
    cdb) = Curried f h c -> forall r. f (c -> r) -> h r
    forall (g :: * -> *) (h :: * -> *) a.
    Curried g h a -> forall r. g (a -> r) -> h r
    runCurried (k c -> Curried f h c
    forall a. k a -> Curried f h a
    f k c
    kd) (b -> c -> b
    cdb (b -> c -> b) -> f b -> f (c -> b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f b
    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 :: forall (f :: * -> *) (u :: * -> *) a.
    Adjunction f u =>
    u a -> Curried f Identity a
    adjointToCurried u a
    ua = (forall r. f (a -> r) -> Identity r) -> Curried f Identity a
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried (r -> Identity r
    forall a. a -> Identity a
    Identity (r -> Identity r) -> (f (a -> r) -> r) -> f (a -> r) -> Identity r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((a -> r) -> u r) -> f (a -> r) -> r
    forall a b. (a -> u b) -> f a -> b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (a -> u b) -> f a -> b
    rightAdjunct ((a -> r) -> u a -> u r
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> u a
    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 :: forall (f :: * -> *) (u :: * -> *) a.
    Adjunction f u =>
    Curried f Identity a -> u a
    curriedToAdjoint (Curried forall r. f (a -> r) -> Identity r
    m) = (f (a -> a) -> a) -> (a -> a) -> u a
    forall a b. (f a -> b) -> a -> u b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (f a -> b) -> a -> u b
    leftAdjunct (Identity a -> a
    forall a. Identity a -> a
    runIdentity (Identity a -> a) -> (f (a -> a) -> Identity a) -> f (a -> a) -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f (a -> a) -> Identity a
    forall r. f (a -> r) -> Identity r
    m) a -> a
    forall a. a -> a
    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 :: forall (f :: * -> *) (u :: * -> *) (h :: * -> *) a.
    Adjunction f u =>
    Curried f h a -> u (h a)
    curriedToComposedAdjoint (Curried forall r. f (a -> r) -> h r
    m) = (f (a -> a) -> h a) -> (a -> a) -> u (h a)
    forall a b. (f a -> b) -> a -> u b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (f a -> b) -> a -> u b
    leftAdjunct f (a -> a) -> h a
    forall r. f (a -> r) -> h r
    m a -> a
    forall a. a -> a
    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 :: forall (h :: * -> *) (f :: * -> *) (u :: * -> *) a.
    (Functor h, Adjunction f u) =>
    u (h a) -> Curried f h a
    composedAdjointToCurried u (h a)
    uha = (forall r. f (a -> r) -> h r) -> Curried f h a
    forall (g :: * -> *) (h :: * -> *) a.
    (forall r. g (a -> r) -> h r) -> Curried g h a
    Curried ((forall r. f (a -> r) -> h r) -> Curried f h a)
    -> (forall r. f (a -> r) -> h r) -> Curried f h a
    forall a b. (a -> b) -> a -> b
    $ ((a -> r) -> u (h r)) -> f (a -> r) -> h r
    forall a b. (a -> u b) -> f a -> b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (a -> u b) -> f a -> b
    rightAdjunct (\a -> r
    b -> (a -> r) -> h a -> h r
    forall a b. (a -> b) -> h a -> h b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> r
    b (h a -> h r) -> u (h a) -> u (h r)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> u (h a)
    uha)
    {-# INLINE composedAdjointToCurried #-}