{-# 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 #-}