{-# LANGUAGE CPP #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
{-# LANGUAGE DeriveDataTypeable #-}
#endif
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ <= 707
{-# LANGUAGE KindSignatures #-}
#endif
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2013-2014 Edward Kmett, Gershom Bazerman and Derek Elkins
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  provisional
-- Portability :  portable
--
-- The Day convolution of two contravariant functors is a contravariant
-- functor.
--
-- <http://ncatlab.org/nlab/show/Day+convolution>
----------------------------------------------------------------------------

module Data.Functor.Contravariant.Day
  ( Day(..)
  , day
  , runDay
  , assoc, disassoc
  , swapped
  , intro1, intro2
  , day1, day2
  , diag
  , trans1, trans2
  ) where

import Control.Applicative
import Data.Functor.Contravariant
import Data.Proxy
import Data.Tuple (swap)
#ifdef __GLASGOW_HASKELL__
import Data.Typeable
#endif

-- | The Day convolution of two contravariant functors.
data Day f g a = forall b c. Day (f b) (g c) (a -> (b, c))
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
  deriving Typeable
#endif

-- | Construct the Day convolution
--
-- @
-- 'day1' ('day' f g) = f
-- 'day2' ('day' f g) = g
-- @
day :: f a -> g b -> Day f g (a, b)
day fa gb = Day fa gb id

#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707
instance (Typeable1 f, Typeable1 g) => Typeable1 (Day f g) where
    typeOf1 tfga = mkTyConApp dayTyCon [typeOf1 (fa tfga), typeOf1 (ga tfga)]
        where fa :: t f (g :: * -> *) a -> f a
              fa = undefined
              ga :: t (f :: * -> *) g a -> g a
              ga = undefined

dayTyCon :: TyCon
#if MIN_VERSION_base(4,4,0)
dayTyCon = mkTyCon3 "contravariant" "Data.Functor.Contravariant.Day" "Day"
#else
dayTyCon = mkTyCon "Data.Functor.Contravariant.Day.Day"
#endif

#endif

instance Contravariant (Day f g) where
  contramap f (Day fb gc abc) = Day fb gc (abc . f)

-- | Break apart the Day convolution of two contravariant functors.
runDay :: (Contravariant f, Contravariant g) => Day f g a -> (f a, g a)
runDay (Day fb gc abc) =
  ( contramap (fst . abc) fb
  , contramap (snd . abc) gc
  )

-- | Day convolution provides a monoidal product. The associativity
-- of this monoid is witnessed by 'assoc' and 'disassoc'.
--
-- @
-- 'assoc' . 'disassoc' = 'id'
-- 'disassoc' . 'assoc' = 'id'
-- 'contramap' f '.' 'assoc' = 'assoc' '.' 'contramap' f
-- @
assoc :: Day f (Day g h) a -> Day (Day f g) h a
assoc (Day fb (Day gd he cde) abc) = Day (Day fb gd id) he $ \a ->
  case cde <$> abc a of
    (b, (d, e)) -> ((b, d), e)

-- | Day convolution provides a monoidal product. The associativity
-- of this monoid is witnessed by 'assoc' and 'disassoc'.
--
-- @
-- 'assoc' . 'disassoc' = 'id'
-- 'disassoc' . 'assoc' = 'id'
-- 'contramap' f '.' 'disassoc' = 'disassoc' '.' 'contramap' f
-- @
disassoc :: Day (Day f g) h a -> Day f (Day g h) a
disassoc (Day (Day fd ge bde) hc abc) = Day fd (Day ge hc id) $ \a ->
  case abc a of
    (b, c) -> case bde b of
      (d, e) -> (d, (e, c))

-- | The monoid for Day convolution /in Haskell/ is symmetric.
--
-- @
-- 'contramap' f '.' 'swapped' = 'swapped' '.' 'contramap' f
-- @
swapped :: Day f g a -> Day g f a
swapped (Day fb gc abc) = Day gc fb (swap . abc)

-- | Proxy serves as the unit of Day convolution.
--
-- @
-- 'day1' '.' 'intro1' = 'id'
-- 'contramap' f '.' 'intro1' = 'intro1' '.' 'contramap' f
-- @
intro1 :: f a -> Day Proxy f a
intro1 fa = Day Proxy fa $ \a -> ((),a)

-- | Proxy serves as the unit of Day convolution.
--
-- @
-- 'day2' '.' 'intro2' = 'id'
-- 'contramap' f '.' 'intro2' = 'intro2' '.' 'contramap' f
-- @
intro2 :: f a -> Day f Proxy a
intro2 fa = Day fa Proxy $ \a -> (a,())

-- | In Haskell we can do general purpose elimination, but in a more general setting
-- it is only possible to eliminate the unit.
--
-- @
-- 'day1' '.' 'intro1' = 'id'
-- 'day1' = 'fst' '.' 'runDay'
-- 'contramap' f '.' 'day1' = 'day1' '.' 'contramap' f
-- @
day1 :: Contravariant f => Day f g a -> f a
day1 (Day fb _ abc) = contramap (fst . abc) fb

-- | In Haskell we can do general purpose elimination, but in a more general setting
-- it is only possible to eliminate the unit.
-- @
-- 'day2' '.' 'intro2' = 'id'
-- 'day2' = 'snd' '.' 'runDay'
-- 'contramap' f '.' 'day2' = 'day2' '.' 'contramap' f
-- @
day2 :: Contravariant g => Day f g a -> g a
day2 (Day _ gc abc) = contramap (snd . abc) gc

-- | Diagonalize the Day convolution:
--
-- @
-- 'day1' '.' 'diag' = 'id'
-- 'day2' '.' 'diag' = 'id'
-- 'runDay' '.' 'diag' = \a -> (a,a)
-- 'contramap' f . 'diag' = 'diag' . 'contramap' f
-- @

diag :: f a -> Day f f a
diag fa = Day fa fa $ \a -> (a,a)

-- | Apply a natural transformation to the left-hand side of a Day convolution.
--
-- This respects the naturality of the natural transformation you supplied:
--
-- @
-- 'contramap' f '.' 'trans1' fg = 'trans1' fg '.' 'contramap' f
-- @
trans1 :: (forall x. f x -> g x) -> Day f h a -> Day g h a
trans1 fg (Day fb hc abc) = Day (fg fb) hc abc

-- | Apply a natural transformation to the right-hand side of a Day convolution.
--
-- This respects the naturality of the natural transformation you supplied:
--
-- @
-- 'contramap' f '.' 'trans2' fg = 'trans2' fg '.' 'contramap' f
-- @
trans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a
trans2 gh (Day fb gc abc) = Day fb (gh gc) abc