{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Data.Functor.Day.Comonoid (
  -- * Comonoid type class
  Comonoid (..), erase1, erase2, duplicateDefault, extendDefault, dayToCompose,
  -- * Re-export
  Comonad(..)
  ) where

import Data.Functor.Day
import Data.Functor.Sum ( Sum(..) )
import Data.Functor.Identity (Identity(..))

import Control.Comonad (Comonad(..))
import Control.Comonad.Trans.Identity (IdentityT(..))
import Control.Comonad.Env (EnvT(..) )
import Control.Comonad.Traced (TracedT(..) )

-- | Comonoid with respect to Day convolution.
--
-- ==== Laws
-- 
-- 'coapply' must satisfy the following equations. Here, @erase1@ and @erase2@
-- are defined using 'extract' method inherited from 'Comonad'.
-- 
-- @
-- 'erase1' . 'coapply' = id
-- 'erase2' . 'coapply' = id
-- 'trans1' 'coapply' . 'coapply' = 'assoc' . 'trans2' 'coapply' . 'coapply'
-- @
-- 
-- Furthermore, 'duplicateDefault' derived from @coapply@ must be equivalent to 'duplicate'
-- inherited from 'Comonad'.
-- 
-- @
-- 'duplicateDefault' = 'dayToCompose' . coapply
--                  = 'duplicate'
-- @
--
-- ==== Examples
-- 
-- Env comonad, or @(,) e@, is an instance of @Comonoid@.
--
-- 
-- > instance Comonoid ((,) e) where
-- >   coapply :: forall x. (e, x) -> Day ((,) e) ((,) e) x
-- >   -- ~ forall x. (e,x) -> ∃b c. ((e,b), (e,c), b -> c -> x)
-- >   -- ~ forall x. (e,x) -> (e,e, ∃b c.(b, c, b -> c -> x))
-- >   -- ~ forall x. (e,x) -> (e,e,x)
-- >   -- ~ e -> (e,e)
-- >   coapply (e, x) = Day (e, ()) (e, ()) (\_ _ -> x)
--
-- Traced comonad, or @((->) m)@, is another example.
-- 
-- > instance Monoid m => Comonoid ((->) m) where
-- >   coapply :: forall x. (m -> x) -> Day ((->) m) ((->) m) x
-- >   -- ~ forall x. (m -> x) -> ∃b c. (m -> b, m -> c, b -> c -> x)
-- >   -- ~ forall x. (m -> x) -> (m -> m -> x)
-- >   -- ~ m -> m -> m
-- >   coapply f = Day id id (\x y -> f (x <> y))
--
-- ==== Non-example
--
-- Unlike @Env@ or @Traced@, 'Control.Comonad.Store.Store' comonad can't be an instance of @Comonoid@.
-- The law requires any lawful @Comonoid f@ to satisfy the following property.
-- 
-- * For any value of @f x@, 'coapply' doesn't change the \"shape\" of it. Precisely, for any value @fx :: f x@,
--   the following equation is true.
--
--     > () <$ coapply fx ≡ Day (() <$ fx) (() <$ fx) (\_ _ -> ())@
-- 
-- Therefore, any lawful @Comonoid (Store s)@ must satisfy the following equation:
--
-- > coapply (store u s0) ≡ Day (store u s0) (store u s0) (\_ _ -> ())
-- >   where u = const () :: s -> ()
-- 
-- But it's incompatible with another requirement that @duplicateDefault@ must be equivalent to @duplicate@ of
-- the @Comonad (Store s)@ instance.
--
-- > duplicateDefault (store u s0) = store (const (store u s0)) s0
-- > duplicate        (store u s0) = store (\s1 -> store u s1)  s0

class Comonad f => Comonoid f where
  coapply :: f a -> Day f f a

-- | Every 'Comonoid' is a 'Comonad'.
duplicateDefault :: Comonoid f => f a -> f (f a)
duplicateDefault :: forall (f :: * -> *) a. Comonoid f => f a -> f (f a)
duplicateDefault = forall (f :: * -> *) (g :: * -> *) a.
(Functor f, Functor g) =>
Day f g a -> f (g a)
dayToCompose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Comonoid f => f a -> Day f f a
coapply

-- | Every 'Comonoid' is a 'Comonad'.
extendDefault :: Comonoid f => (f a -> b) -> f a -> f b
extendDefault :: forall (f :: * -> *) a b. Comonoid f => (f a -> b) -> f a -> f b
extendDefault f a -> b
t = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> b
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Comonoid f => f a -> f (f a)
duplicateDefault


-- | @'Day' f g@ can be turned into a composition of @f@ and @g@.
dayToCompose :: (Functor f, Functor g) => Day f g a -> f (g a)
dayToCompose :: forall (f :: * -> *) (g :: * -> *) a.
(Functor f, Functor g) =>
Day f g a -> f (g a)
dayToCompose (Day f b
fb g c
fc b -> c -> a
op) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\b
b -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b -> c -> a
op b
b) g c
fc) f b
fb

-- | @erase1 = elim1 . trans1 (Identity . extract)@
erase1 :: (Comonad f, Functor g) => Day f g c -> g c
erase1 :: forall (f :: * -> *) (g :: * -> *) c.
(Comonad f, Functor g) =>
Day f g c -> g c
erase1 Day f g c
fg = case Day f g c
fg of
  Day f b
f g c
g b -> c -> c
op -> b -> c -> c
op (forall (w :: * -> *) a. Comonad w => w a -> a
extract f b
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g c
g

-- | @erase2 = elim2 . trans2 (Identity . extract)@
erase2 :: (Functor f, Comonad g) => Day f g c -> f c
erase2 :: forall (f :: * -> *) (g :: * -> *) c.
(Functor f, Comonad g) =>
Day f g c -> f c
erase2 Day f g c
fg = case Day f g c
fg of
  Day f b
f g c
g b -> c -> c
op -> (\b
a -> b -> c -> c
op b
a (forall (w :: * -> *) a. Comonad w => w a -> a
extract g c
g)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f b
f

-- | @transBi t u = trans1 t . trans2 u = trans2 u . trans1 t@
transBi :: (forall x. f x -> f' x) -> (forall x. g x -> g' x) -> Day f g a -> Day f' g' a
transBi :: forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (g' :: * -> *) a.
(forall x. f x -> f' x)
-> (forall x. g x -> g' x) -> Day f g a -> Day f' g' a
transBi forall x. f x -> f' x
t forall x. g x -> g' x
u (Day f b
f g c
g b -> c -> a
op) = forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day (forall x. f x -> f' x
t f b
f) (forall x. g x -> g' x
u g c
g) b -> c -> a
op

interchange :: Day (Day f f') (Day g g') x -> Day (Day f g) (Day f' g') x
-- interchange = disassoc . trans1 (assoc . trans2 swapped . disassoc) . assoc
interchange :: forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (g' :: * -> *) x.
Day (Day f f') (Day g g') x -> Day (Day f g) (Day f' g') x
interchange (Day (Day f b
fa f' c
fb b -> c -> b
ab_x) (Day g b
gc g' c
gd b -> c -> c
cd_y) b -> c -> x
xy_r) =
  forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day (forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day f b
fa g b
gc (,)) (forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day f' c
fb g' c
gd (,)) (\(b
a,b
c) (c
b,c
d) -> b -> c -> x
xy_r (b -> c -> b
ab_x b
a c
b) (b -> c -> c
cd_y b
c c
d))

instance Comonoid Identity where
  coapply :: forall a. Identity a -> Day Identity Identity a
coapply (Identity a
a) = forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day (forall a. a -> Identity a
Identity ()) (forall a. a -> Identity a
Identity ()) (\()
_ ()
_ -> a
a)

instance Comonoid ((,) e) where
  coapply :: forall x. (e, x) -> Day ((,) e) ((,) e) x
  coapply :: forall a. (e, a) -> Day ((,) e) ((,) e) a
coapply (e
e, x
x) = forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day (e
e, ()) (e
e, ()) (\()
_ ()
_ -> x
x)

instance Monoid m => Comonoid ((->) m) where
  coapply :: forall x. (m -> x) -> Day ((->) m) ((->) m) x
  coapply :: forall a. (m -> a) -> Day ((->) m) ((->) m) a
coapply m -> x
f = forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day forall a. a -> a
id forall a. a -> a
id (\m
x m
y -> m -> x
f (m
x forall a. Semigroup a => a -> a -> a
<> m
y))

instance (Comonoid f, Comonoid g) => Comonoid (Sum f g) where
  coapply :: forall a. Sum f g a -> Day (Sum f g) (Sum f g) a
coapply (InL f a
f) = forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (g' :: * -> *) a.
(forall x. f x -> f' x)
-> (forall x. g x -> g' x) -> Day f g a -> Day f' g' a
transBi forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (forall (f :: * -> *) a. Comonoid f => f a -> Day f f a
coapply f a
f)
  coapply (InR g a
g) = forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (g' :: * -> *) a.
(forall x. f x -> f' x)
-> (forall x. g x -> g' x) -> Day f g a -> Day f' g' a
transBi forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (forall (f :: * -> *) a. Comonoid f => f a -> Day f f a
coapply g a
g)

instance (Comonoid f, Comonoid g) => Comonoid (Day f g) where
  coapply :: forall a. Day f g a -> Day (Day f g) (Day f g) a
coapply = forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (g' :: * -> *) x.
Day (Day f f') (Day g g') x -> Day (Day f g) (Day f' g') x
interchange forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (g' :: * -> *) a.
(forall x. f x -> f' x)
-> (forall x. g x -> g' x) -> Day f g a -> Day f' g' a
transBi forall (f :: * -> *) a. Comonoid f => f a -> Day f f a
coapply forall (f :: * -> *) a. Comonoid f => f a -> Day f f a
coapply

instance (Comonoid f) => Comonoid (IdentityT f) where
  coapply :: forall a. IdentityT f a -> Day (IdentityT f) (IdentityT f) a
coapply (IdentityT f a
fx) = forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (g' :: * -> *) a.
(forall x. f x -> f' x)
-> (forall x. g x -> g' x) -> Day f g a -> Day f' g' a
transBi forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (forall (f :: * -> *) a. Comonoid f => f a -> Day f f a
coapply f a
fx)

instance (Comonoid f) => Comonoid (EnvT e f) where
  coapply :: forall a. EnvT e f a -> Day (EnvT e f) (EnvT e f) a
coapply (EnvT e
e f a
fx) = forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (g' :: * -> *) a.
(forall x. f x -> f' x)
-> (forall x. g x -> g' x) -> Day f g a -> Day f' g' a
transBi (forall e (w :: * -> *) a. e -> w a -> EnvT e w a
EnvT e
e) (forall e (w :: * -> *) a. e -> w a -> EnvT e w a
EnvT e
e) (forall (f :: * -> *) a. Comonoid f => f a -> Day f f a
coapply f a
fx)

instance (Monoid m, Comonoid f) => Comonoid (TracedT m f) where
  coapply :: forall a. TracedT m f a -> Day (TracedT m f) (TracedT m f) a
coapply (TracedT f (m -> a)
ft) = case forall (f :: * -> *) a. Comonoid f => f a -> Day f f a
coapply f (m -> a)
ft of
    Day f b
fa f c
fb b -> c -> m -> a
op -> forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day (forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a
TracedT ((,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f b
fa)) (forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a
TracedT ((,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f c
fb)) (\(b
a, m
m1) (c
b, m
m2) -> b -> c -> m -> a
op b
a c
b (m
m1 forall a. Semigroup a => a -> a -> a
<> m
m2))