    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE Trustworthy #-}

    -----------------------------------------------------------------------------
    -- |
    -- Copyright   :  (C) 2013-2016 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    --
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  provisional
    -- Portability :  GADTs, TFs, MPTCs
    --
    -- The co-Yoneda lemma for presheafs states that @f@ is naturally isomorphic to @'Coyoneda' f@.
    --
    ----------------------------------------------------------------------------
    module Data.Functor.Contravariant.Coyoneda
      ( Coyoneda(..)
      , liftCoyoneda
      , lowerCoyoneda
      , hoistCoyoneda
      ) where

    import Control.Arrow
    import Data.Functor.Contravariant
    import Data.Functor.Contravariant.Adjunction
    import Data.Functor.Contravariant.Rep

    -- | A 'Contravariant' functor (aka presheaf) suitable for Yoneda reduction.
    --
    -- <http://ncatlab.org/nlab/show/Yoneda+reduction>
    data Coyoneda f a where
      Coyoneda :: (a -> b) -> f b -> Coyoneda f a

    instance Contravariant (Coyoneda f) where
      contramap :: forall a' a. (a' -> a) -> Coyoneda f a -> Coyoneda f a'
    contramap a' -> a
    f (Coyoneda a -> b
    g f b
    m) = (a' -> b) -> f b -> Coyoneda f a'
    forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
    Coyoneda (a -> b
    g(a -> b) -> (a' -> a) -> a' -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .a' -> a
    f) f b
    m
      {-# INLINE contramap #-}

    instance Representable f => Representable (Coyoneda f) where
      type Rep (Coyoneda f) = Rep f
      tabulate :: forall a. (a -> Rep (Coyoneda f)) -> Coyoneda f a
    tabulate = f a -> Coyoneda f a
    forall (f :: * -> *) a. f a -> Coyoneda f a
    liftCoyoneda (f a -> Coyoneda f a)
    -> ((a -> Rep f) -> f a) -> (a -> Rep f) -> Coyoneda f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> Rep f) -> f a
    forall a. (a -> Rep f) -> f a
    forall (f :: * -> *) a. Representable f => (a -> Rep f) -> f a
    tabulate
      {-# INLINE tabulate #-}
      index :: forall a. Coyoneda f a -> a -> Rep (Coyoneda f)
    index (Coyoneda a -> b
    ab f b
    fb) a
    a = f b -> b -> Rep f
    forall a. f a -> a -> Rep f
    forall (f :: * -> *) a. Representable f => f a -> a -> Rep f
    index f b
    fb (a -> b
    ab a
    a)
      {-# INLINE index #-}
      contramapWithRep :: forall b a.
    (b -> Either a (Rep (Coyoneda f))) -> Coyoneda f a -> Coyoneda f b
    contramapWithRep b -> Either a (Rep (Coyoneda f))
    beav (Coyoneda a -> b
    ac f b
    fc) = (b -> Either b (Rep f)) -> f (Either b (Rep f)) -> Coyoneda f b
    forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
    Coyoneda ((a -> b) -> Either a (Rep f) -> Either b (Rep f)
    forall b c d. (b -> c) -> Either b d -> Either c d
    forall (a :: * -> * -> *) b c d.
    ArrowChoice a =>
    a b c -> a (Either b d) (Either c d)
    left a -> b
    ac (Either a (Rep f) -> Either b (Rep f))
    -> (b -> Either a (Rep f)) -> b -> Either b (Rep f)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b -> Either a (Rep f)
    b -> Either a (Rep (Coyoneda f))
    beav) ((Either b (Rep f) -> Either b (Rep f))
    -> f b -> f (Either b (Rep f))
    forall b a. (b -> Either a (Rep f)) -> f a -> f b
    forall (f :: * -> *) b a.
    Representable f =>
    (b -> Either a (Rep f)) -> f a -> f b
    contramapWithRep Either b (Rep f) -> Either b (Rep f)
    forall a. a -> a
    id f b
    fc)
      {-# INLINE contramapWithRep #-}

    instance Adjunction f g => Adjunction (Coyoneda f) (Coyoneda g) where
      leftAdjunct :: forall b a. (b -> Coyoneda f a) -> a -> Coyoneda g b
    leftAdjunct b -> Coyoneda f a
    f = g b -> Coyoneda g b
    forall (f :: * -> *) a. f a -> Coyoneda f a
    liftCoyoneda (g b -> Coyoneda g b) -> (a -> g b) -> a -> Coyoneda g b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (b -> f a) -> a -> g b
    forall b a. (b -> f a) -> a -> g b
    forall (f :: * -> *) (g :: * -> *) b a.
    Adjunction f g =>
    (b -> f a) -> a -> g b
    leftAdjunct (Coyoneda f a -> f a
    forall (f :: * -> *) a. Contravariant f => Coyoneda f a -> f a
    lowerCoyoneda (Coyoneda f a -> f a) -> (b -> Coyoneda f a) -> b -> f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b -> Coyoneda f a
    f)
      {-# INLINE leftAdjunct #-}
      rightAdjunct :: forall a b. (a -> Coyoneda g b) -> b -> Coyoneda f a
    rightAdjunct a -> Coyoneda g b
    f = f a -> Coyoneda f a
    forall (f :: * -> *) a. f a -> Coyoneda f a
    liftCoyoneda (f a -> Coyoneda f a) -> (b -> f a) -> b -> Coyoneda f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> g b) -> b -> f a
    forall a b. (a -> g b) -> b -> f a
    forall (f :: * -> *) (g :: * -> *) a b.
    Adjunction f g =>
    (a -> g b) -> b -> f a
    rightAdjunct (Coyoneda g b -> g b
    forall (f :: * -> *) a. Contravariant f => Coyoneda f a -> f a
    lowerCoyoneda (Coyoneda g b -> g b) -> (a -> Coyoneda g b) -> a -> g b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Coyoneda g b
    f)
      {-# INLINE rightAdjunct #-}

    -- | Coyoneda "expansion" of a presheaf
    --
    -- @
    -- 'liftCoyoneda' . 'lowerCoyoneda' ≡ 'id'
    -- 'lowerCoyoneda' . 'liftCoyoneda' ≡ 'id'
    -- @
    liftCoyoneda :: f a -> Coyoneda f a
    liftCoyoneda :: forall (f :: * -> *) a. f a -> Coyoneda f a
    liftCoyoneda = (a -> a) -> f a -> Coyoneda f a
    forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
    Coyoneda a -> a
    forall a. a -> a
    id
    {-# INLINE liftCoyoneda #-}

    -- | Coyoneda reduction on a presheaf
    lowerCoyoneda :: Contravariant f => Coyoneda f a -> f a
    lowerCoyoneda :: forall (f :: * -> *) a. Contravariant f => Coyoneda f a -> f a
    lowerCoyoneda (Coyoneda a -> b
    f f b
    m) = (a -> b) -> f b -> f a
    forall a' a. (a' -> a) -> f a -> f a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap a -> b
    f f b
    m
    {-# INLINE lowerCoyoneda #-}

    -- | Lift a natural transformation from @f@ to @g@ to a natural transformation
    -- from @Coyoneda f@ to @Coyoneda g@.
    hoistCoyoneda :: (forall a. f a -> g a) -> (Coyoneda f b -> Coyoneda g b)
    hoistCoyoneda :: forall (f :: * -> *) (g :: * -> *) b.
    (forall a. f a -> g a) -> Coyoneda f b -> Coyoneda g b
    hoistCoyoneda forall a. f a -> g a
    f (Coyoneda b -> b
    g f b
    x) = (b -> b) -> g b -> Coyoneda g b
    forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
    Coyoneda b -> b
    g (f b -> g b
    forall a. f a -> g a
    f f b
    x)
    {-# INLINE hoistCoyoneda #-}