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

#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif

-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2011-2016 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  provisional
-- Portability :  GADTs, MPTCs, fundeps
--
-- The co-Yoneda lemma for a covariant 'Functor' @f@ states that @'Coyoneda' f@
-- is naturally isomorphic to @f@.
----------------------------------------------------------------------------
module Data.Functor.Coyoneda
  ( Coyoneda(..)
  , liftCoyoneda, lowerCoyoneda, lowerM
  -- * as a Left Kan extension
  , coyonedaToLan, lanToCoyoneda
  ) where

import Control.Applicative
import Control.Monad (MonadPlus(..), liftM)
import Control.Monad.Fix
import Control.Monad.Trans.Class
import Control.Comonad
import Control.Comonad.Trans.Class
import Data.Distributive
import Data.Function (on)
import Data.Functor.Adjunction
import Data.Functor.Bind
import Data.Functor.Extend
import Data.Functor.Identity
import Data.Functor.Kan.Lan
import Data.Functor.Plus
import Data.Functor.Rep
import Data.Foldable
import Data.Traversable
import Data.Semigroup.Foldable
import Data.Semigroup.Traversable
import Prelude hiding (sequence, lookup, zipWith)
import Text.Read hiding (lift)

-- | A covariant 'Functor' suitable for Yoneda reduction
--
data Coyoneda f a where
  Coyoneda :: (b -> a) -> f b -> Coyoneda f a

-- | @Coyoneda f@ is the left Kan extension of @f@ along the 'Identity' functor.
--
-- @Coyoneda f@ is always a functor, even if @f@ is not. In this case, it
-- is called the /free functor over @f@/. Note the following categorical fine
-- print: If @f@ is not a functor, @Coyoneda f@ is actually not the left Kan
-- extension of @f@ along the 'Identity' functor, but along the inclusion
-- functor from the discrete subcategory of /Hask/ which contains only identity
-- functions as morphisms to the full category /Hask/. (This is because @f@,
-- not being a proper functor, can only be interpreted as a categorical functor
-- by restricting the source category to only contain identities.)
--
-- @
-- 'coyonedaToLan' . 'lanToCoyoneda' ≡ 'id'
-- 'lanToCoyoneda' . 'coyonedaToLan' ≡ 'id'
-- @
coyonedaToLan :: Coyoneda f a -> Lan Identity f a
coyonedaToLan (Coyoneda ba fb) = Lan (ba . runIdentity) fb

lanToCoyoneda :: Lan Identity f a -> Coyoneda f a
lanToCoyoneda (Lan iba fb) = Coyoneda (iba . Identity) fb

-- {-# RULES "coyonedaToLan/lanToCoyoneda=id" coyonedaToLan . lanToCoyoneda = id #-}
-- {-# RULES "lanToCoyoneda/coyonedaToLan=id" lanToCoyoneda . coyonedaToLan = id #-}

instance Functor (Coyoneda f) where
  fmap f (Coyoneda g v) = Coyoneda (f . g) v
  {-# INLINE fmap #-}

instance Apply f => Apply (Coyoneda f) where
  m <.> n = liftCoyoneda $ lowerCoyoneda m <.> lowerCoyoneda n
  {-# INLINE (<.>) #-}

instance Applicative f => Applicative (Coyoneda f) where
  pure = liftCoyoneda . pure
  {-# INLINE pure #-}
  m <*> n = liftCoyoneda $ lowerCoyoneda m <*> lowerCoyoneda n
  {-# INLINE (<*>) #-}

instance Alternative f => Alternative (Coyoneda f) where
  empty = liftCoyoneda empty
  {-# INLINE empty #-}
  m <|> n = liftCoyoneda $ lowerCoyoneda m <|> lowerCoyoneda n
  {-# INLINE (<|>) #-}

instance Alt f => Alt (Coyoneda f) where
  m <!> n = liftCoyoneda $ lowerCoyoneda m <!> lowerCoyoneda n
  {-# INLINE (<!>) #-}

instance Plus f => Plus (Coyoneda f) where
  zero = liftCoyoneda zero
  {-# INLINE zero #-}

instance Bind m => Bind (Coyoneda m) where
  Coyoneda f v >>- k = liftCoyoneda (v >>- lowerCoyoneda . k . f)
  {-# INLINE (>>-) #-}

instance Monad m => Monad (Coyoneda m) where
#if __GLASGOW_HASKELL__ < 710
  return = Coyoneda id . return
  {-# INLINE return #-}
#endif
  Coyoneda f v >>= k = lift (v >>= lowerM . k . f)
  {-# INLINE (>>=) #-}

instance MonadTrans Coyoneda where
  lift = Coyoneda id
  {-# INLINE lift #-}

instance MonadFix f => MonadFix (Coyoneda f) where
  mfix f = lift $ mfix (lowerM . f)
  {-# INLINE mfix #-}

instance MonadPlus f => MonadPlus (Coyoneda f) where
  mzero = lift mzero
  {-# INLINE mzero #-}
  m `mplus` n = lift $ lowerM m `mplus` lowerM n
  {-# INLINE mplus #-}

instance Representable f => Representable (Coyoneda f) where
  type Rep (Coyoneda f) = Rep f
  tabulate = liftCoyoneda . tabulate
  {-# INLINE tabulate #-}
  index = index . lowerCoyoneda
  {-# INLINE index #-}

instance Extend w => Extend (Coyoneda w) where
  extended k (Coyoneda f v) = Coyoneda id $ extended (k . Coyoneda f) v
  {-# INLINE extended #-}

instance Comonad w => Comonad (Coyoneda w) where
  extend k (Coyoneda f v) = Coyoneda id $ extend (k . Coyoneda f) v
  {-# INLINE extend #-}
  extract (Coyoneda f v) = f (extract v)
  {-# INLINE extract #-}

instance ComonadTrans Coyoneda where
  lower (Coyoneda f a) = fmap f a
  {-# INLINE lower #-}

instance Foldable f => Foldable (Coyoneda f) where
  foldMap f (Coyoneda k a) = foldMap (f . k) a
  {-# INLINE foldMap #-}

instance Foldable1 f => Foldable1 (Coyoneda f) where
  foldMap1 f (Coyoneda k a) = foldMap1 (f . k) a
  {-# INLINE foldMap1 #-}

instance Traversable f => Traversable (Coyoneda f) where
  traverse f (Coyoneda k a) = Coyoneda id <$> traverse (f . k) a
  {-# INLINE traverse #-}

instance Traversable1 f => Traversable1 (Coyoneda f) where
  traverse1 f (Coyoneda k a) = Coyoneda id <$> traverse1 (f . k) a
  {-# INLINE traverse1 #-}

instance Distributive f => Distributive (Coyoneda f) where
  collect f = liftCoyoneda . collect (lowerCoyoneda . f)
  {-# INLINE collect #-}

instance (Functor f, Show (f a)) => Show (Coyoneda f a) where
  showsPrec d (Coyoneda f a) = showParen (d > 10) $
    showString "liftCoyoneda " . showsPrec 11 (fmap f a)
  {-# INLINE showsPrec #-}

#ifdef __GLASGOW_HASKELL__
instance (Functor f, Read (f a)) => Read (Coyoneda f a) where
  readPrec = parens $ prec 10 $ do
    Ident "liftCoyoneda" <- lexP
    liftCoyoneda <$> step readPrec
  {-# INLINE readPrec #-}
#endif

instance (Functor f, Eq (f a)) => Eq (Coyoneda f a) where
  (==) = (==) `on` lowerCoyoneda
  {-# INLINE (==) #-}

instance (Functor f, Ord (f a)) => Ord (Coyoneda f a) where
  compare = compare `on` lowerCoyoneda
  {-# INLINE compare #-}

instance Adjunction f g => Adjunction (Coyoneda f) (Coyoneda g) where
  unit = liftCoyoneda . fmap liftCoyoneda . unit
  {-# INLINE unit #-}
  counit = counit . fmap lowerCoyoneda . lowerCoyoneda
  {-# INLINE counit #-}

-- | Yoneda \"expansion\"
--
-- @
-- 'liftCoyoneda' . 'lowerCoyoneda' ≡ 'id'
-- 'lowerCoyoneda' . 'liftCoyoneda' ≡ 'id'
-- @
--
-- @
-- lowerCoyoneda (liftCoyoneda fa) = -- by definition
-- lowerCoyoneda (Coyoneda id fa)  = -- by definition
-- fmap id fa                      = -- functor law
-- fa
-- @
--
-- @
-- 'lift' = 'liftCoyoneda'
-- @
liftCoyoneda :: f a -> Coyoneda f a
liftCoyoneda = Coyoneda id
{-# INLINE liftCoyoneda #-}

-- | Yoneda reduction lets us walk under the existential and apply 'fmap'.
--
-- Mnemonically, \"Yoneda reduction\" sounds like and works a bit like β-reduction.
--
-- <http://ncatlab.org/nlab/show/Yoneda+reduction>
--
-- You can view 'Coyoneda' as just the arguments to 'fmap' tupled up.
--
-- @
-- 'lower' = 'lowerM' = 'lowerCoyoneda'
-- @
lowerCoyoneda :: Functor f => Coyoneda f a -> f a
lowerCoyoneda (Coyoneda f m) = fmap f m
{-# INLINE lowerCoyoneda #-}

-- | Yoneda reduction given a 'Monad' lets us walk under the existential and apply 'liftM'.
--
-- You can view 'Coyoneda' as just the arguments to 'liftM' tupled up.
--
-- @
-- 'lower' = 'lowerM' = 'lowerCoyoneda'
-- @
lowerM :: Monad f => Coyoneda f a -> f a
lowerM (Coyoneda f m) = liftM f m
{-# INLINE lowerM #-}