{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE UndecidableInstances #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2013-2016 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <[email protected]>
-- 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 (f :: * -> *) a. (forall r. (r -> a) -> f r) -> Yoneda f a
Yoneda forall a b. (a -> b) -> a -> b
$ \r -> a
ra -> 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 = forall (f :: * -> *) a. Yoneda f a -> forall r. (r -> a) -> f r
runYoneda Yoneda f a
f 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 (f :: * -> *) a. (forall r. (r -> a) -> f r) -> Yoneda f a
Yoneda (forall r. (r -> a) -> f r
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (f :: * -> *) a. Contravariant f => f a -> Yoneda f a
liftYoneda forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (f :: * -> *) a. Representable f => f a -> a -> Rep f
index (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 = forall (f :: * -> *) a. Contravariant f => f a -> Yoneda f a
liftYoneda forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) b a.
Representable f =>
(b -> Either a (Rep f)) -> f a -> f b
contramapWithRep b -> Either a (Rep (Yoneda f))
beav forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (f :: * -> *) a. Contravariant f => f a -> Yoneda f a
liftYoneda forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (g :: * -> *) b a.
Adjunction f g =>
(b -> f a) -> a -> g b
leftAdjunct (forall (f :: * -> *) a. Yoneda f a -> f a
lowerYoneda 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 = forall (f :: * -> *) a. Contravariant f => f a -> Yoneda f a
liftYoneda forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (g :: * -> *) a b.
Adjunction f g =>
(a -> g b) -> b -> f a
rightAdjunct (forall (f :: * -> *) a. Yoneda f a -> f a
lowerYoneda forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Yoneda g b
f)
  {-# INLINE rightAdjunct #-}