{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes                #-}
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2018 Brian Mckenna
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  provisional
-- Portability :  portable
--
-- The Day convolution of two invariant functors is an invariant
-- functor.
--
-- <http://ncatlab.org/nlab/show/Day+convolution>
----------------------------------------------------------------------------

module Data.Functor.Invariant.Day
  ( Day(..)
  , day
  , assoc, disassoc
  , swapped
  , intro1, intro2
  , elim1, elim2
  , trans1, trans2
  , toContravariant, toCovariant
  ) where

import qualified Data.Functor.Contravariant.Day as Contravariant
import qualified Data.Functor.Day               as Covariant
import           Data.Functor.Identity
import           Data.Functor.Invariant

-- | The Day convolution of two invariant functors.
data Day f g a = forall b c. Day (f b) (g c) (b -> c -> a) (a -> (b, c))

instance Invariant (Day f g) where
  invmap :: (a -> b) -> (b -> a) -> Day f g a -> Day f g b
invmap a -> b
f b -> a
g (Day f b
fb g c
gc b -> c -> a
bca a -> (b, c)
abc) = f b -> g c -> (b -> c -> b) -> (b -> (b, c)) -> Day f g b
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f b
fb g c
gc ((a -> b
f (a -> b) -> (c -> a) -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((c -> a) -> c -> b) -> (b -> c -> a) -> b -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> c -> a
bca) (a -> (b, c)
abc (a -> (b, c)) -> (b -> a) -> b -> (b, c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
g)

-- | Construct the Day convolution
day :: f a -> g b -> Day f g (a, b)
day :: f a -> g b -> Day f g (a, b)
day f a
fa g b
gb = f a
-> g b
-> (a -> b -> (a, b))
-> ((a, b) -> (a, b))
-> Day f g (a, b)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f a
fa g b
gb (,) (a, b) -> (a, b)
forall a. a -> a
id

-- | Day convolution provides a monoidal product. The associativity
-- of this monoid is witnessed by 'assoc' and 'disassoc'.
--
-- @
-- 'assoc' . 'disassoc' = 'id'
-- 'disassoc' . 'assoc' = 'id'
-- 'invmap' f g '.' 'assoc' = 'assoc' '.' 'invmap' f g
-- @
assoc :: Day f (Day g h) a -> Day (Day f g) h a
assoc :: Day f (Day g h) a -> Day (Day f g) h a
assoc (Day f b
fb (Day g b
gd h c
he b -> c -> c
dec c -> (b, c)
cde) b -> c -> a
bca a -> (b, c)
abc) = (((b, b) -> c -> a) -> (a -> ((b, b), c)) -> Day (Day f g) h a)
-> (a -> ((b, b), c)) -> ((b, b) -> c -> a) -> Day (Day f g) h a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Day f g (b, b)
-> h c
-> ((b, b) -> c -> a)
-> (a -> ((b, b), c))
-> Day (Day f g) h a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day (f b
-> g b
-> (b -> b -> (b, b))
-> ((b, b) -> (b, b))
-> Day f g (b, b)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f b
fb g b
gd (,) (b, b) -> (b, b)
forall a. a -> a
id) h c
he) a -> ((b, b), c)
f (b, b) -> c -> a
g
  where
    f :: a -> ((b, b), c)
f a
a =
      let (b
b,c
c) = a -> (b, c)
abc a
a
          (b
d,c
e) = c -> (b, c)
cde c
c
      in ((b
b,b
d),c
e)
    g :: (b, b) -> c -> a
g (b
b,b
d) c
e =
      b -> c -> a
bca b
b (b -> c -> c
dec b
d c
e)

-- | Day convolution provides a monoidal product. The associativity
-- of this monoid is witnessed by 'assoc' and 'disassoc'.
--
-- @
-- 'assoc' . 'disassoc' = 'id'
-- 'disassoc' . 'assoc' = 'id'
-- 'invmap' f g '.' 'disassoc' = 'disassoc' '.' 'invmap' f g
-- @
disassoc :: Day (Day f g) h a -> Day f (Day g h) a
disassoc :: Day (Day f g) h a -> Day f (Day g h) a
disassoc (Day (Day f b
fb g c
gc b -> c -> b
deb b -> (b, c)
bde) h c
hd b -> c -> a
bca a -> (b, c)
abc) = f b
-> Day g h (c, c)
-> (b -> (c, c) -> a)
-> (a -> (b, (c, c)))
-> Day f (Day g h) a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f b
fb (g c
-> h c
-> (c -> c -> (c, c))
-> ((c, c) -> (c, c))
-> Day g h (c, c)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day g c
gc h c
hd (,) (c, c) -> (c, c)
forall a. a -> a
id) b -> (c, c) -> a
f a -> (b, (c, c))
g
  where
    f :: b -> (c, c) -> a
f b
e (c
d,c
c) =
      b -> c -> a
bca (b -> c -> b
deb b
e c
d) c
c
    g :: a -> (b, (c, c))
g a
a =
      let (b
b,c
c) = a -> (b, c)
abc a
a
          (b
d,c
e) = b -> (b, c)
bde b
b
      in (b
d,(c
e,c
c))

-- | The monoid for 'Day' convolution on the cartesian monoidal structure is symmetric.
--
-- @
-- 'invmap' f g '.' 'swapped' = 'swapped' '.' 'invmap' f g
-- @
swapped :: Day f g a -> Day g f a
swapped :: Day f g a -> Day g f a
swapped (Day f b
fb g c
gc b -> c -> a
bca a -> (b, c)
abc) = g c -> f b -> (c -> b -> a) -> (a -> (c, b)) -> Day g f a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day g c
gc f b
fb ((b -> c -> a) -> c -> b -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> c -> a
bca) (\a
a -> let (b
b, c
c) = a -> (b, c)
abc a
a in (c
c, b
b))

-- | 'Identity' is the unit of 'Day' convolution
--
-- @
-- 'intro1' '.' 'elim1' = 'id'
-- 'elim1' '.' 'intro1' = 'id'
-- @
intro1 :: f a -> Day Identity f a
intro1 :: f a -> Day Identity f a
intro1 f a
fa = Identity ()
-> f a -> (() -> a -> a) -> (a -> ((), a)) -> Day Identity f a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day (() -> Identity ()
forall a. a -> Identity a
Identity ()) f a
fa (\()
_ a
a -> a
a) ((,) ())

-- | 'Identity' is the unit of 'Day' convolution
--
-- @
-- 'intro2' '.' 'elim2' = 'id'
-- 'elim2' '.' 'intro2' = 'id'
-- @
intro2 :: f a -> Day f Identity a
intro2 :: f a -> Day f Identity a
intro2 f a
fa = f a
-> Identity ()
-> (a -> () -> a)
-> (a -> (a, ()))
-> Day f Identity a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f a
fa (() -> Identity ()
forall a. a -> Identity a
Identity ()) a -> () -> a
forall a b. a -> b -> a
const ((a -> () -> (a, ())) -> () -> a -> (a, ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) ())

-- | 'Identity' is the unit of 'Day' convolution
--
-- @
-- 'intro1' '.' 'elim1' = 'id'
-- 'elim1' '.' 'intro1' = 'id'
-- @
elim1 :: Invariant f => Day Identity f a -> f a
elim1 :: Day Identity f a -> f a
elim1 (Day (Identity b
b) f c
fc b -> c -> a
bca a -> (b, c)
abc) = (c -> a) -> (a -> c) -> f c -> f a
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (b -> c -> a
bca b
b) ((b, c) -> c
forall a b. (a, b) -> b
snd ((b, c) -> c) -> (a -> (b, c)) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
abc) f c
fc

-- | 'Identity' is the unit of 'Day' convolution
--
-- @
-- 'intro2' '.' 'elim2' = 'id'
-- 'elim2' '.' 'intro2' = 'id'
-- @
elim2 :: Invariant f => Day f Identity a -> f a
elim2 :: Day f Identity a -> f a
elim2 (Day f b
fb (Identity c
c) b -> c -> a
bca a -> (b, c)
abc) = (b -> a) -> (a -> b) -> f b -> f a
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap ((b -> c -> a) -> c -> b -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> c -> a
bca c
c) ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (a -> (b, c)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
abc) f b
fb

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

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

-- | Drop the covariant part of the Day convolution.
toContravariant :: Day f g a -> Contravariant.Day f g a
toContravariant :: Day f g a -> Day f g a
toContravariant (Day f b
fb g c
gc b -> c -> a
_ a -> (b, c)
abc) = f b -> g c -> (a -> (b, c)) -> Day f g a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
Contravariant.Day f b
fb g c
gc a -> (b, c)
abc

-- | Drop the contravariant part of the Day convolution.
toCovariant :: Day f g a -> Covariant.Day f g a
toCovariant :: Day f g a -> Day f g a
toCovariant (Day f b
fb g c
gc b -> c -> a
bca a -> (b, c)
_) = f b -> g c -> (b -> c -> a) -> Day f g a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Covariant.Day f b
fb g c
gc b -> c -> a
bca