    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE Rank2Types #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# 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
    --
    ----------------------------------------------------------------------------
    module Data.Functor.Contravariant.Yoneda
      ( Yoneda(..)
      , liftYoneda, lowerYoneda
      ) where

    import Data.Functor.Contravariant
    import Data.Functor.Contravariant.Adjunction
    import Data.Functor.Contravariant.Rep

    -- | Yoneda embedding for a presheaf
    newtype Yoneda f a = Yoneda { forall (f :: * -> *) a. Yoneda f a -> forall r. (r -> a) -> f r
    runYoneda :: forall r. (r -> a) -> f r }

    -- |
    --
    -- @
    -- 'liftYoneda' . 'lowerYoneda' ≡ 'id'
    -- 'lowerYoneda' . 'liftYoneda' ≡ 'id'
    -- @

    liftYoneda :: Contravariant f => f a -> Yoneda f a
    liftYoneda :: forall (f :: * -> *) a. Contravariant f => f a -> Yoneda f a
    liftYoneda f a
    fa = (forall r. (r -> a) -> f r) -> Yoneda f a
    forall (f :: * -> *) a. (forall r. (r -> a) -> f r) -> Yoneda f a
    Yoneda ((forall r. (r -> a) -> f r) -> Yoneda f a)
    -> (forall r. (r -> a) -> f r) -> Yoneda f a
    forall a b. (a -> b) -> a -> b
    $ \r -> a
    ra -> (r -> a) -> f a -> f r
    forall a' a. (a' -> a) -> f a -> f a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap r -> a
    ra f a
    fa
    {-# INLINE liftYoneda #-}

    lowerYoneda :: Yoneda f a -> f a
    lowerYoneda :: forall (f :: * -> *) a. Yoneda f a -> f a
    lowerYoneda Yoneda f a
    f = Yoneda f a -> forall r. (r -> a) -> f r
    forall (f :: * -> *) a. Yoneda f a -> forall r. (r -> a) -> f r
    runYoneda Yoneda f a
    f a -> a
    forall a. a -> a
    id
    {-# INLINE lowerYoneda #-}

    instance Contravariant (Yoneda f) where
      contramap :: forall a' a. (a' -> a) -> Yoneda f a -> Yoneda f a'
    contramap a' -> a
    ab (Yoneda forall r. (r -> a) -> f r
    m) = (forall r. (r -> a') -> f r) -> Yoneda f a'
    forall (f :: * -> *) a. (forall r. (r -> a) -> f r) -> Yoneda f a
    Yoneda ((r -> a) -> f r
    forall r. (r -> a) -> f r
    m ((r -> a) -> f r) -> ((r -> a') -> r -> a) -> (r -> a') -> f r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a' -> a) -> (r -> a') -> r -> a
    forall a b. (a -> b) -> (r -> a) -> r -> b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a' -> a
    ab)
      {-# INLINE contramap #-}

    instance Representable f => Representable (Yoneda f) where
      type Rep (Yoneda f) = Rep f
      tabulate :: forall a. (a -> Rep (Yoneda f)) -> Yoneda f a
    tabulate = f a -> Yoneda f a
    forall (f :: * -> *) a. Contravariant f => f a -> Yoneda f a
    liftYoneda (f a -> Yoneda f a)
    -> ((a -> Rep f) -> f a) -> (a -> Rep f) -> Yoneda 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. Yoneda f a -> a -> Rep (Yoneda f)
    index Yoneda f a
    m a
    a = f a -> a -> Rep f
    forall a. f a -> a -> Rep f
    forall (f :: * -> *) a. Representable f => f a -> a -> Rep f
    index (Yoneda f a -> f a
    forall (f :: * -> *) a. Yoneda f a -> f a
    lowerYoneda Yoneda f a
    m) a
    a
      {-# INLINE index #-}
      contramapWithRep :: forall b a.
    (b -> Either a (Rep (Yoneda f))) -> Yoneda f a -> Yoneda f b
    contramapWithRep b -> Either a (Rep (Yoneda f))
    beav = f b -> Yoneda f b
    forall (f :: * -> *) a. Contravariant f => f a -> Yoneda f a
    liftYoneda (f b -> Yoneda f b)
    -> (Yoneda f a -> f b) -> Yoneda f a -> Yoneda f b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (b -> Either a (Rep f)) -> f a -> f b
    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 b -> Either a (Rep f)
    b -> Either a (Rep (Yoneda f))
    beav (f a -> f b) -> (Yoneda f a -> f a) -> Yoneda f a -> f b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Yoneda f a -> f a
    forall (f :: * -> *) a. Yoneda f a -> f a
    lowerYoneda
      {-# INLINE contramapWithRep #-}

    instance Adjunction f g => Adjunction (Yoneda f) (Yoneda g) where
      leftAdjunct :: forall b a. (b -> Yoneda f a) -> a -> Yoneda g b
    leftAdjunct b -> Yoneda f a
    f = g b -> Yoneda g b
    forall (f :: * -> *) a. Contravariant f => f a -> Yoneda f a
    liftYoneda (g b -> Yoneda g b) -> (a -> g b) -> a -> Yoneda 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 (Yoneda f a -> f a
    forall (f :: * -> *) a. Yoneda f a -> f a
    lowerYoneda (Yoneda f a -> f a) -> (b -> Yoneda f a) -> b -> f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b -> Yoneda f a
    f)
      {-# INLINE leftAdjunct #-}
      rightAdjunct :: forall a b. (a -> Yoneda g b) -> b -> Yoneda f a
    rightAdjunct a -> Yoneda g b
    f = f a -> Yoneda f a
    forall (f :: * -> *) a. Contravariant f => f a -> Yoneda f a
    liftYoneda (f a -> Yoneda f a) -> (b -> f a) -> b -> Yoneda 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 (Yoneda g b -> g b
    forall (f :: * -> *) a. Yoneda f a -> f a
    lowerYoneda (Yoneda g b -> g b) -> (a -> Yoneda g b) -> a -> g b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Yoneda g b
    f)
      {-# INLINE rightAdjunct #-}