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

#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
--
-- 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) = forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
Coyoneda (a -> b
gforall 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 = forall (f :: * -> *) a. f a -> Coyoneda f a
liftCoyoneda 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. Coyoneda f a -> a -> Rep (Coyoneda f)
index (Coyoneda a -> b
ab f b
fb) a
a = 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) = forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
Coyoneda (forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left a -> b
ac forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Either a (Rep (Coyoneda f))
beav) (forall (f :: * -> *) b a.
Representable f =>
(b -> Either a (Rep f)) -> f a -> f b
contramapWithRep 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 = forall (f :: * -> *) a. f a -> Coyoneda f a
liftCoyoneda 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. Contravariant f => Coyoneda f a -> f a
lowerCoyoneda 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 = forall (f :: * -> *) a. f a -> Coyoneda f a
liftCoyoneda 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. Contravariant f => Coyoneda f a -> f a
lowerCoyoneda 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 = forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
Coyoneda 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) = 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) = forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
Coyoneda b -> b
g (forall a. f a -> g a
f f b
x)
{-# INLINE hoistCoyoneda #-}