    {-# LANGUAGE CPP #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE UndecidableInstances #-}
    #if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ <= 708
    {-# LANGUAGE Trustworthy #-}
    #endif
    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Profunctor.Composition
    -- Copyright   :  (C) 2014-2015 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    --
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  experimental
    -- Portability :  GADTs, TFs, MPTCs, RankN
    --
    ----------------------------------------------------------------------------
    module Data.Profunctor.Composition
      (
      -- * Profunctor Composition
        Procompose(..)
      , procomposed
      -- * Unitors and Associator
      , idl
      , idr
      , assoc
      -- * Categories as monoid objects
      , eta
      , mu
      -- * Generalized Composition
      , stars, kleislis
      , costars, cokleislis
      -- * Right Kan Lift
      , Rift(..)
      , decomposeRift
      ) where

    import Control.Arrow
    import Control.Category
    import Control.Comonad
    import Control.Monad (liftM)
    import Data.Functor.Compose
    import Data.Profunctor
    import Data.Profunctor.Adjunction
    import Data.Profunctor.Mapping
    import Data.Profunctor.Monad
    import Data.Profunctor.Rep
    import Data.Profunctor.Sieve
    import Data.Profunctor.Traversing
    import Data.Profunctor.Unsafe
    import Prelude hiding ((.),id)

    type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)

    -- * Profunctor Composition

    -- | @'Procompose' p q@ is the 'Profunctor' composition of the
    -- 'Profunctor's @p@ and @q@.
    --
    -- For a good explanation of 'Profunctor' composition in Haskell
    -- see Dan Piponi's article:
    --
    -- <http://blog.sigfpe.com/2011/07/profunctors-in-haskell.html>
    data Procompose p q d c where
      Procompose :: p x c -> q d x -> Procompose p q d c

    instance ProfunctorFunctor (Procompose p) where
      promap f (Procompose p q) = Procompose p (f q)

    instance Category p => ProfunctorMonad (Procompose p) where
      proreturn = Procompose id
      projoin (Procompose p (Procompose q r)) = Procompose (p . q) r

    procomposed :: Category p => Procompose p p a b -> p a b
    procomposed (Procompose pxc pdx) = pxc . pdx
    {-# INLINE procomposed #-}

    instance (Profunctor p, Profunctor q) => Profunctor (Procompose p q) where
      dimap l r (Procompose f g) = Procompose (rmap r f) (lmap l g)
      {-# INLINE dimap #-}
      lmap k (Procompose f g) = Procompose f (lmap k g)
      {-# INLINE rmap #-}
      rmap k (Procompose f g) = Procompose (rmap k f) g
      {-# INLINE lmap #-}
      k #. Procompose f g     = Procompose (k #. f) g
      {-# INLINE ( #. ) #-}
      Procompose f g .# k     = Procompose f (g .# k)
      {-# INLINE ( .# ) #-}

    instance Profunctor p => Functor (Procompose p q a) where
      fmap k (Procompose f g) = Procompose (rmap k f) g
      {-# INLINE fmap #-}

    instance (Sieve p f, Sieve q g) => Sieve (Procompose p q) (Compose g f) where
      sieve (Procompose g f) d = Compose $ sieve g <$> sieve f d
      {-# INLINE sieve #-}

    -- | The composition of two 'Representable' 'Profunctor's is 'Representable' by
    -- the composition of their representations.
    instance (Representable p, Representable q) => Representable (Procompose p q) where
      type Rep (Procompose p q) = Compose (Rep q) (Rep p)
      tabulate f = Procompose (tabulate id) (tabulate (getCompose . f))
      {-# INLINE tabulate #-}

    instance (Cosieve p f, Cosieve q g) => Cosieve (Procompose p q) (Compose f g) where
      cosieve (Procompose g f) (Compose d) = cosieve g $ cosieve f <$> d
      {-# INLINE cosieve #-}

    instance (Corepresentable p, Corepresentable q) => Corepresentable (Procompose p q) where
      type Corep (Procompose p q) = Compose (Corep p) (Corep q)
      cotabulate f = Procompose (cotabulate (f . Compose)) (cotabulate id)
      {-# INLINE cotabulate #-}

    instance (Strong p, Strong q) => Strong (Procompose p q) where
      first' (Procompose x y) = Procompose (first' x) (first' y)
      {-# INLINE first' #-}
      second' (Procompose x y) = Procompose (second' x) (second' y)
      {-# INLINE second' #-}

    instance (Choice p, Choice q) => Choice (Procompose p q) where
      left' (Procompose x y) = Procompose (left' x) (left' y)
      {-# INLINE left' #-}
      right' (Procompose x y) = Procompose (right' x) (right' y)
      {-# INLINE right' #-}

    instance (Closed p, Closed q) => Closed (Procompose p q) where
      closed (Procompose x y) = Procompose (closed x) (closed y)
      {-# INLINE closed #-}

    instance (Traversing p, Traversing q) => Traversing (Procompose p q) where
      traverse' (Procompose p q) = Procompose (traverse' p) (traverse' q)
      {-# INLINE traverse' #-}

    instance (Mapping p, Mapping q) => Mapping (Procompose p q) where
      map' (Procompose p q) = Procompose (map' p) (map' q)
      {-# INLINE map' #-}

    instance (Corepresentable p, Corepresentable q) => Costrong (Procompose p q) where
      unfirst = unfirstCorep
      {-# INLINE unfirst #-}
      unsecond = unsecondCorep
      {-# INLINE unsecond #-}

    -- * Lax identity

    -- | @(->)@ functions as a lax identity for 'Profunctor' composition.
    --
    -- This provides an 'Iso' for the @lens@ package that witnesses the
    -- isomorphism between @'Procompose' (->) q d c@ and @q d c@, which
    -- is the left identity law.
    --
    -- @
    -- 'idl' :: 'Profunctor' q => Iso' ('Procompose' (->) q d c) (q d c)
    -- @
    idl :: Profunctor q => Iso (Procompose (->) q d c) (Procompose (->) r d' c') (q d c) (r d' c')
    idl = dimap (\(Procompose g f) -> rmap g f) (fmap (Procompose id))

    -- | @(->)@ functions as a lax identity for 'Profunctor' composition.
    --
    -- This provides an 'Iso' for the @lens@ package that witnesses the
    -- isomorphism between @'Procompose' q (->) d c@ and @q d c@, which
    -- is the right identity law.
    --
    -- @
    -- 'idr' :: 'Profunctor' q => Iso' ('Procompose' q (->) d c) (q d c)
    -- @
    idr :: Profunctor q => Iso (Procompose q (->) d c) (Procompose r (->) d' c') (q d c) (r d' c')
    idr = dimap (\(Procompose g f) -> lmap f g) (fmap (`Procompose` id))

    -- | The associator for 'Profunctor' composition.
    --
    -- This provides an 'Iso' for the @lens@ package that witnesses the
    -- isomorphism between @'Procompose' p ('Procompose' q r) a b@ and
    -- @'Procompose' ('Procompose' p q) r a b@, which arises because
    -- @Prof@ is only a bicategory, rather than a strict 2-category.
    assoc :: Iso (Procompose p (Procompose q r) a b) (Procompose x (Procompose y z) a b)
                 (Procompose (Procompose p q) r a b) (Procompose (Procompose x y) z a b)
    assoc = dimap (\(Procompose f (Procompose g h)) -> Procompose (Procompose f g) h)
                  (fmap (\(Procompose (Procompose f g) h) -> Procompose f (Procompose g h)))

    -- | 'Profunctor' composition generalizes 'Functor' composition in two ways.
    --
    -- This is the first, which shows that @exists b. (a -> f b, b -> g c)@ is
    -- isomorphic to @a -> f (g c)@.
    --
    -- @'stars' :: 'Functor' f => Iso' ('Procompose' ('Star' f) ('Star' g) d c) ('Star' ('Compose' f g) d c)@
    stars :: Functor g
            => Iso (Procompose (Star f ) (Star g ) d  c )
                   (Procompose (Star f') (Star g') d' c')
                   (Star (Compose g  f ) d  c )
                   (Star (Compose g' f') d' c')
    stars = dimap hither (fmap yon) where
      hither (Procompose (Star xgc) (Star dfx)) = Star (Compose . fmap xgc . dfx)
      yon (Star dfgc) = Procompose (Star id) (Star (getCompose . dfgc))

    -- | 'Profunctor' composition generalizes 'Functor' composition in two ways.
    --
    -- This is the second, which shows that @exists b. (f a -> b, g b -> c)@ is
    -- isomorphic to @g (f a) -> c@.
    --
    -- @'costars' :: 'Functor' f => Iso' ('Procompose' ('Costar' f) ('Costar' g) d c) ('Costar' ('Compose' g f) d c)@
    costars :: Functor f
              => Iso (Procompose (Costar f ) (Costar g ) d  c )
                     (Procompose (Costar f') (Costar g') d' c')
                     (Costar (Compose f  g ) d  c )
                     (Costar (Compose f' g') d' c')
    costars = dimap hither (fmap yon) where
      hither (Procompose (Costar gxc) (Costar fdx)) = Costar (gxc . fmap fdx . getCompose)
      yon (Costar dgfc) = Procompose (Costar (dgfc . Compose)) (Costar id)

    -- | This is a variant on 'stars' that uses 'Kleisli' instead of 'Star'.
    --
    -- @'kleislis' :: 'Monad' f => Iso' ('Procompose' ('Kleisli' f) ('Kleisli' g) d c) ('Kleisli' ('Compose' f g) d c)@
    kleislis :: Monad g
            => Iso (Procompose (Kleisli f ) (Kleisli g ) d  c )
                   (Procompose (Kleisli f') (Kleisli g') d' c')
                   (Kleisli (Compose g  f ) d  c )
                   (Kleisli (Compose g' f') d' c')
    kleislis = dimap hither (fmap yon) where
      hither (Procompose (Kleisli xgc) (Kleisli dfx)) = Kleisli (Compose . liftM xgc . dfx)
      yon (Kleisli dfgc) = Procompose (Kleisli id) (Kleisli (getCompose . dfgc))

    -- | This is a variant on 'costars' that uses 'Cokleisli' instead
    -- of 'Costar'.
    --
    -- @'cokleislis' :: 'Functor' f => Iso' ('Procompose' ('Cokleisli' f) ('Cokleisli' g) d c) ('Cokleisli' ('Compose' g f) d c)@
    cokleislis :: Functor f
              => Iso (Procompose (Cokleisli f ) (Cokleisli g ) d  c )
                     (Procompose (Cokleisli f') (Cokleisli g') d' c')
                     (Cokleisli (Compose f  g ) d  c )
                     (Cokleisli (Compose f' g') d' c')
    cokleislis = dimap hither (fmap yon) where
      hither (Procompose (Cokleisli gxc) (Cokleisli fdx)) = Cokleisli (gxc . fmap fdx . getCompose)
      yon (Cokleisli dgfc) = Procompose (Cokleisli (dgfc . Compose)) (Cokleisli id)

    ----------------------------------------------------------------------------
    -- * Rift
    ----------------------------------------------------------------------------

    -- | This represents the right Kan lift of a 'Profunctor' @q@ along a 'Profunctor' @p@ in a limited version of the 2-category of Profunctors where the only object is the category Hask, 1-morphisms are profunctors composed and compose with Profunctor composition, and 2-morphisms are just natural transformations.
    newtype Rift p q a b = Rift { runRift :: forall x. p b x -> q a x }

    instance ProfunctorFunctor (Rift p) where
      promap f (Rift g) = Rift (f . g)

    instance Category p => ProfunctorComonad (Rift p) where
      proextract (Rift f) = f id
      produplicate (Rift f) = Rift $ \p -> Rift $ \q -> f (q . p)

    instance (Profunctor p, Profunctor q) => Profunctor (Rift p q) where
      dimap ca bd f = Rift (lmap ca . runRift f . lmap bd)
      {-# INLINE dimap #-}
      lmap ca f = Rift (lmap ca . runRift f)
      {-# INLINE lmap #-}
      rmap bd f = Rift (runRift f . lmap bd)
      {-# INLINE rmap #-}
      bd #. f = Rift (\p -> runRift f (p .# bd))
      {-# INLINE ( #. ) #-}
      f .# ca = Rift (\p -> runRift f p .# ca)
      {-# INLINE (.#) #-}

    instance Profunctor p => Functor (Rift p q a) where
      fmap bd f = Rift (runRift f . lmap bd)
      {-# INLINE fmap #-}

    -- | @'Rift' p p@ forms a 'Monad' in the 'Profunctor' 2-category, which is isomorphic to a Haskell 'Category' instance.
    instance p ~ q => Category (Rift p q) where
      id = Rift id
      {-# INLINE id #-}
      Rift f . Rift g = Rift (g . f)
      {-# INLINE (.) #-}

    -- | The 2-morphism that defines a left Kan lift.
    --
    -- Note: When @p@ is right adjoint to @'Rift' p (->)@ then 'decomposeRift' is the 'counit' of the adjunction.
    decomposeRift :: Procompose p (Rift p q) :-> q
    decomposeRift (Procompose p (Rift pq)) = pq p
    {-# INLINE decomposeRift #-}

    instance ProfunctorAdjunction (Procompose p) (Rift p) where
      counit (Procompose p (Rift pq)) = pq p
      unit q = Rift $ \p -> Procompose p q

    --instance (ProfunctorAdjunction f g, ProfunctorAdjunction f' g') => ProfunctorAdjunction (ProfunctorCompose f' f) (ProfunctorCompose g g') where

    ----------------------------------------------------------------------------
    -- * Monoids
    ----------------------------------------------------------------------------

    -- | a 'Category' that is also a 'Profunctor' is a 'Monoid' in @Prof@

    eta :: (Profunctor p, Category p) => (->) :-> p
    eta f = rmap f id

    mu :: Category p => Procompose p p :-> p
    mu (Procompose f g) = f . g