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