{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

-- | 'FFunctor' with tensorial strength with respect to 'Day'.
module FStrong where

import Data.Coerce (coerce)

import Data.Functor.Day
import Data.Functor.Day.Curried

import FFunctor
import FMonad

import Data.Functor.Compose
import FFunctor.FCompose
import Data.Functor.Precompose ( Precompose(..) )
import Data.Functor.Bicompose ( Bicompose(..) )
import Control.Monad.Trans.Identity (IdentityT (..))
import Control.Monad.Trans.Reader (ReaderT (..))
import Control.Monad.Trans.State (StateT (..))
import Control.Monad.Trans.Writer (WriterT (..))
import Control.Comonad.Env (EnvT(..))
import Control.Comonad.Traced (TracedT(..))
import Control.Comonad.Store (StoreT (..))

-- | 'FFunctor' with tensorial strength with respect to 'Day'.
class FFunctor ff => FStrong ff where
  {-# MINIMAL fstrength | mapCurried #-}

  -- | Tensorial strength with respect to 'Day'.
  --
  -- 'fstrength' can be thought as a higher-order version of @strength@ function below.
  --
  -- @
  -- strength :: Functor f => (f a, b) -> f (a, b)
  -- strength (fa, b) = fmap (\a -> (a,b)) fa
  -- @
  --
  -- For the ordinary 'Functor', no additional type classes were needed to have @strength@ function,
  -- because it works for any @Functor f@. This is not the case for 'FFunctor' and 'fstrength'.
  --
  -- ==== Laws
  --
  -- These two equations must hold.
  --
  -- @
  -- ffmap 'elim2' . fstrength  = 'elim2'
  --       :: Day (ff g) 'Data.Functor.Identity.Identity' ~> ff g
  -- fstrength . 'trans1' fstrength = ffmap 'assoc' . fstrength . 'disassoc'
  --       :: Day (Day (ff g) h) k ~> ff (Day (Day g h) k))
  -- @
  --
  -- Alternatively, these diagrams must commute.
  --
  -- >                    fstrength
  -- >  ff g ⊗ Identity ----------->  ff (g ⊗ Identity)
  -- >            \                          |
  -- >             \                         |   ffmap elim2
  -- >              \                        |
  -- >        elim2  \                       v
  -- >                \---------------->   ff g
  --
  --
  -- >                     trans1 fstrength                      fstrength
  -- > (ff g ⊗ h) ⊗ k -------------------->  ff (g ⊗ h) ⊗ k ----------->  ff ((g ⊗ h) ⊗ k)
  -- >            |                                                                   ^
  -- >            | disassoc                                             ffmap assoc  |
  -- >            |                                                                   |
  -- >            v                           fstrength                               |
  -- >  ff g ⊗ (h ⊗ k) --------------------------------------------------->  ff (g ⊗ (h ⊗ k))
  --
  -- For readability, an infix operator @(⊗) was used instead of the type constructor @Day@.
  fstrength :: (Functor g) => Day (ff g) h ~> ff (Day g h)
  fstrength (Day ff g b
ffg h c
h b -> c -> x
op) =
    Curried (ff g) (ff (Day g h)) c
-> forall r. ff g (c -> r) -> ff (Day g h) r
forall (g :: * -> *) (h :: * -> *) a.
Curried g h a -> forall r. g (a -> r) -> h r
runCurried (Curried g (Day g h) c -> Curried (ff g) (ff (Day g h)) c
Curried g (Day g h) ~> Curried (ff g) (ff (Day g h))
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
Curried g h ~> Curried (ff g) (ff h)
forall (ff :: FF) (g :: * -> *) (h :: * -> *).
(FStrong ff, Functor g, Functor h) =>
Curried g h ~> Curried (ff g) (ff h)
mapCurried (h c -> Curried g (Day g h) c
forall (g :: * -> *) a (f :: * -> *). g a -> Curried f (Day f g) a
unapplied h c
h)) ((b -> c -> x) -> ff g b -> ff g (c -> x)
forall a b. (a -> b) -> ff g a -> ff g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> c -> x
op ff g b
ffg)

  -- | Internal 'ffmap'.
  --
  -- 'mapCurried' can be seen as @ffmap@ but by using "internal language" of
  -- \(\mathrm{Hask}^{\mathrm{Hask}}\), the category of @Functor@s.
  --
  -- @
  -- ffmap         :: (g ~> h)       ->  (ff g ~> ff h)
  -- mapCurried    :: (Curried g h)  ~>  (Curried (ff g) (ff h))
  -- @
  --
  -- @ffmap@ takes a natural transformations @(~>)@, in other words morphism in \(\mathrm{Hask}^{\mathrm{Hask}}\),
  -- and returns another @(~>)@. @ffmap@ itself is an usual function, which is an outsider for
  -- \(\mathrm{Hask}^{\mathrm{Hask}}\).
  --
  -- On the other hand, @mapCurried@ is a natural transformation @(~>)@ between @Curried _ _@,
  -- objects of \(\mathrm{Hask}^{\mathrm{Hask}}\).
  -- 
  -- The existence of 'mapCurried' is known to be equivalent to the existence of
  -- 'fstrength'.
  --
  -- ==== Laws
  --
  -- These equations must hold.
  --
  -- @
  -- mapCurried . 'Data.Functor.Day.Extra.unitCurried' = 'Data.Functor.Day.Extra.unitCurried'
  --     :: Identity ~> Curried (ff g) (ff g)
  -- mapCurried . 'Data.Functor.Day.Extra.composeCurried' = 'Data.Functor.Day.Extra.composeCurried' . trans1 mapCurried . trans2 mapCurried
  --     :: Day (Curried g h) (Curried h k) ~> Curried (ff g) (ff k)
  -- @
  mapCurried :: (Functor g, Functor h) => Curried g h ~> Curried (ff g) (ff h)
  mapCurried Curried g h x
gh = (forall r. ff g (x -> r) -> ff h r) -> Curried (ff g) (ff h) x
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried ((forall r. ff g (x -> r) -> ff h r) -> Curried (ff g) (ff h) x)
-> (forall r. ff g (x -> r) -> ff h r) -> Curried (ff g) (ff h) x
forall a b. (a -> b) -> a -> b
$ \ff g (x -> r)
ffg -> (Day g (Curried g h) ~> h) -> ff (Day g (Curried g h)) r -> ff h r
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap Day g (Curried g h) x -> h x
Day g (Curried g h) ~> h
forall (f :: * -> *) (g :: * -> *) a.
Functor f =>
Day f (Curried f g) a -> g a
applied (Day (ff g) (Curried g h) r -> ff (Day g (Curried g h)) r
Day (ff g) (Curried g h) ~> ff (Day g (Curried g h))
forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (ff g) h ~> ff (Day g h)
forall (ff :: FF) (g :: * -> *) (h :: * -> *).
(FStrong ff, Functor g) =>
Day (ff g) h ~> ff (Day g h)
fstrength (ff g (x -> r) -> Curried g h x -> Day (ff g) (Curried g h) r
forall (f :: * -> *) a b (g :: * -> *).
f (a -> b) -> g a -> Day f g b
day ff g (x -> r)
ffg Curried g h x
gh))

-- | 'fstrength' but from left
fstrength' :: (FStrong ff, Functor h) => Day g (ff h) ~> ff (Day g h)
fstrength' :: forall (ff :: FF) (h :: * -> *) (g :: * -> *).
(FStrong ff, Functor h) =>
Day g (ff h) ~> ff (Day g h)
fstrength' = (Day h g ~> Day g h) -> ff (Day h g) x -> ff (Day g h) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap Day h g x -> Day g h x
Day h g ~> Day g h
forall (f :: * -> *) (g :: * -> *) a. Day f g a -> Day g f a
swapped (ff (Day h g) x -> ff (Day g h) x)
-> (Day g (ff h) x -> ff (Day h g) x)
-> Day g (ff h) x
-> ff (Day g h) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Day (ff h) g x -> ff (Day h g) x
Day (ff h) g ~> ff (Day h g)
forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (ff g) h ~> ff (Day g h)
forall (ff :: FF) (g :: * -> *) (h :: * -> *).
(FStrong ff, Functor g) =>
Day (ff g) h ~> ff (Day g h)
fstrength (Day (ff h) g x -> ff (Day h g) x)
-> (Day g (ff h) x -> Day (ff h) g x)
-> Day g (ff h) x
-> ff (Day h g) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Day g (ff h) x -> Day (ff h) g x
forall (f :: * -> *) (g :: * -> *) a. Day f g a -> Day g f a
swapped

-- | Combine an applicative action(s) inside @ff@ to another action @h a@.
innerAp :: (FStrong ff, Applicative h) => ff h (a -> b) -> h a -> ff h b
innerAp :: forall (ff :: FF) (h :: * -> *) a b.
(FStrong ff, Applicative h) =>
ff h (a -> b) -> h a -> ff h b
innerAp ff h (a -> b)
ffh h a
h = (Day h h ~> h) -> ff (Day h h) b -> ff h b
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap Day h h x -> h x
Day h h ~> h
forall (f :: * -> *) a. Applicative f => Day f f a -> f a
dap (ff (Day h h) b -> ff h b) -> ff (Day h h) b -> ff h b
forall a b. (a -> b) -> a -> b
$ Day (ff h) h b -> ff (Day h h) b
Day (ff h) h ~> ff (Day h h)
forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (ff g) h ~> ff (Day g h)
forall (ff :: FF) (g :: * -> *) (h :: * -> *).
(FStrong ff, Functor g) =>
Day (ff g) h ~> ff (Day g h)
fstrength (ff h (a -> b) -> h a -> Day (ff h) h b
forall (f :: * -> *) a b (g :: * -> *).
f (a -> b) -> g a -> Day f g b
day ff h (a -> b)
ffh h a
h)

-- | Cf. 'Control.Monad.ap'
fap :: (FStrong mm, FMonad mm, Functor g, Functor h) => Day (mm g) (mm h) ~> mm (Day g h)
fap :: forall (mm :: FF) (g :: * -> *) (h :: * -> *).
(FStrong mm, FMonad mm, Functor g, Functor h) =>
Day (mm g) (mm h) ~> mm (Day g h)
fap = mm (mm (Day g h)) x -> mm (Day g h) x
mm (mm (Day g h)) ~> mm (Day g h)
forall (ff :: FF) (g :: * -> *).
(FMonad ff, Functor g) =>
ff (ff g) ~> ff g
fjoin (mm (mm (Day g h)) x -> mm (Day g h) x)
-> (Day (mm g) (mm h) x -> mm (mm (Day g h)) x)
-> Day (mm g) (mm h) x
-> mm (Day g h) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Day g (mm h) ~> mm (Day g h))
-> mm (Day g (mm h)) x -> mm (mm (Day g h)) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> mm g x -> mm h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap Day g (mm h) x -> mm (Day g h) x
Day g (mm h) ~> mm (Day g h)
forall (ff :: FF) (h :: * -> *) (g :: * -> *).
(FStrong ff, Functor h) =>
Day g (ff h) ~> ff (Day g h)
fstrength' (mm (Day g (mm h)) x -> mm (mm (Day g h)) x)
-> (Day (mm g) (mm h) x -> mm (Day g (mm h)) x)
-> Day (mm g) (mm h) x
-> mm (mm (Day g h)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Day (mm g) (mm h) x -> mm (Day g (mm h)) x
Day (mm g) (mm h) ~> mm (Day g (mm h))
forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (mm g) h ~> mm (Day g h)
forall (ff :: FF) (g :: * -> *) (h :: * -> *).
(FStrong ff, Functor g) =>
Day (ff g) h ~> ff (Day g h)
fstrength

instance FStrong IdentityT where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (IdentityT g) h ~> IdentityT (Day g h)
fstrength = Day (IdentityT g) h x -> IdentityT (Day g h) x
forall a b. Coercible a b => a -> b
coerce

instance FStrong (Day f) where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (Day f g) h ~> Day f (Day g h)
fstrength = Day (Day f g) h x -> Day f (Day g h) x
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
Day (Day f g) h a -> Day f (Day g h) a
disassoc

instance Functor f => FStrong (Curried f) where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (Curried f g) h ~> Curried f (Day g h)
fstrength = (forall x. Day f (Day (Curried f g) h) x -> Day g h x)
-> Day (Curried f g) h x -> Curried f (Day g h) x
forall (g :: * -> *) (k :: * -> *) (h :: * -> *) a.
(forall x. Day g k x -> h x) -> k a -> Curried g h a
toCurried ((forall x. Day f (Curried f g) x -> g x)
-> Day (Day f (Curried f g)) h x -> Day g h x
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
(forall x. f x -> g x) -> Day f h a -> Day g h a
trans1 Day f (Curried f g) x -> g x
forall x. Day f (Curried f g) x -> g x
forall (f :: * -> *) (g :: * -> *) a.
Functor f =>
Day f (Curried f g) a -> g a
applied (Day (Day f (Curried f g)) h x -> Day g h x)
-> (Day f (Day (Curried f g) h) x -> Day (Day f (Curried f g)) h x)
-> Day f (Day (Curried f g) h) x
-> Day g h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Day f (Day (Curried f g) h) x -> Day (Day f (Curried f g)) h x
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
Day f (Day g h) a -> Day (Day f g) h a
assoc)

instance Functor f => FStrong (Compose f) where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (Compose f g) h ~> Compose f (Day g h)
fstrength (Day (Compose f (g b)
fg) h c
h b -> c -> x
op) = f (Day g h x) -> Compose f (Day g h) x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((g b -> Day g h x) -> f (g b) -> f (Day g h x)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\g b
g -> g b -> h c -> (b -> c -> x) -> Day g h x
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day g b
g h c
h b -> c -> x
op) f (g b)
fg)

instance Functor f => FStrong (Precompose f) where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (Precompose f g) h ~> Precompose f (Day g h)
fstrength (Day (Precompose g (f b)
gf) h c
h b -> c -> x
op) = Day g h (f x) -> Precompose f (Day g h) x
forall j k (f :: j -> k) (g :: k -> *) (a :: j).
g (f a) -> Precompose f g a
Precompose (g (f b) -> h c -> (f b -> c -> f x) -> Day g h (f x)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day g (f b)
gf h c
h (\f b
fa c
b -> (b -> x) -> f b -> f x
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> c -> x) -> c -> b -> x
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> c -> x
op c
b) f b
fa))

instance (Functor f, Functor f') => FStrong (Bicompose f f') where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (Bicompose f f' g) h ~> Bicompose f f' (Day g h)
fstrength (Day (Bicompose f (g (f' b))
fgf') h c
h b -> c -> x
op) =
    f (Day g h (f' x)) -> Bicompose f f' (Day g h) x
forall k2 k0 k1 (f :: k2 -> *) (g :: k0 -> k1) (h :: k1 -> k2)
       (a :: k0).
f (h (g a)) -> Bicompose f g h a
Bicompose (f (Day g h (f' x)) -> Bicompose f f' (Day g h) x)
-> f (Day g h (f' x)) -> Bicompose f f' (Day g h) x
forall a b. (a -> b) -> a -> b
$
      (g (f' b) -> Day g h (f' x)) -> f (g (f' b)) -> f (Day g h (f' x))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\g (f' b)
gf' -> g (f' b) -> h c -> (f' b -> c -> f' x) -> Day g h (f' x)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day g (f' b)
gf' h c
h (\f' b
fa c
b -> (b -> x) -> f' b -> f' x
forall a b. (a -> b) -> f' a -> f' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> c -> x) -> c -> b -> x
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> c -> x
op c
b) f' b
fa)) f (g (f' b))
fgf'

instance FStrong (ReaderT e) where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (ReaderT e g) h ~> ReaderT e (Day g h)
fstrength (Day (ReaderT e -> g b
eg) h c
h b -> c -> x
op) = (e -> Day g h x) -> ReaderT e (Day g h) x
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((e -> Day g h x) -> ReaderT e (Day g h) x)
-> (e -> Day g h x) -> ReaderT e (Day g h) x
forall a b. (a -> b) -> a -> b
$ \e
e -> g b -> h c -> (b -> c -> x) -> Day g h x
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day (e -> g b
eg e
e) h c
h b -> c -> x
op

instance FStrong (WriterT m) where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (WriterT m g) h ~> WriterT m (Day g h)
fstrength (Day (WriterT g (b, m)
gm) h c
h b -> c -> x
op) = Day g h (x, m) -> WriterT m (Day g h) x
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (Day g h (x, m) -> WriterT m (Day g h) x)
-> Day g h (x, m) -> WriterT m (Day g h) x
forall a b. (a -> b) -> a -> b
$ g (b, m) -> h c -> ((b, m) -> c -> (x, m)) -> Day g h (x, m)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day g (b, m)
gm h c
h (\(b
b, m
m) c
c -> (b -> c -> x
op b
b c
c, m
m))

instance FStrong (StateT s) where
  -- StateT s = ReaderT s ∘ WriterT s = Compose ((->) s) ∘ WriterT s
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (StateT s g) h ~> StateT s (Day g h)
fstrength (Day (StateT s -> g (b, s)
sgs) h c
h b -> c -> x
op) = (s -> Day g h (x, s)) -> StateT s (Day g h) x
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((s -> Day g h (x, s)) -> StateT s (Day g h) x)
-> (s -> Day g h (x, s)) -> StateT s (Day g h) x
forall a b. (a -> b) -> a -> b
$ \s
s -> g (b, s) -> h c -> ((b, s) -> c -> (x, s)) -> Day g h (x, s)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day (s -> g (b, s)
sgs s
s) h c
h (\(b
b, s
s') c
c -> (b -> c -> x
op b
b c
c, s
s'))

instance (FStrong ff, FStrong gg) => FStrong (FCompose ff gg) where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (FCompose ff gg g) h ~> FCompose ff gg (Day g h)
fstrength = ff (gg (Day g h)) x -> FCompose ff gg (Day g h) x
forall (ff :: FF) (gg :: FF) (h :: * -> *) x.
ff (gg h) x -> FCompose ff gg h x
FCompose (ff (gg (Day g h)) x -> FCompose ff gg (Day g h) x)
-> (Day (FCompose ff gg g) h x -> ff (gg (Day g h)) x)
-> Day (FCompose ff gg g) h x
-> FCompose ff gg (Day g h) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Day (gg g) h ~> gg (Day g h))
-> ff (Day (gg g) h) x -> ff (gg (Day g h)) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap Day (gg g) h x -> gg (Day g h) x
Day (gg g) h ~> gg (Day g h)
forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (gg g) h ~> gg (Day g h)
forall (ff :: FF) (g :: * -> *) (h :: * -> *).
(FStrong ff, Functor g) =>
Day (ff g) h ~> ff (Day g h)
fstrength (ff (Day (gg g) h) x -> ff (gg (Day g h)) x)
-> (Day (FCompose ff gg g) h x -> ff (Day (gg g) h) x)
-> Day (FCompose ff gg g) h x
-> ff (gg (Day g h)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Day (ff (gg g)) h x -> ff (Day (gg g) h) x
Day (ff (gg g)) h ~> ff (Day (gg g) h)
forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (ff g) h ~> ff (Day g h)
forall (ff :: FF) (g :: * -> *) (h :: * -> *).
(FStrong ff, Functor g) =>
Day (ff g) h ~> ff (Day g h)
fstrength (Day (ff (gg g)) h x -> ff (Day (gg g) h) x)
-> (Day (FCompose ff gg g) h x -> Day (ff (gg g)) h x)
-> Day (FCompose ff gg g) h x
-> ff (Day (gg g) h) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Day (FCompose ff gg g) h x -> Day (ff (gg g)) h x
forall a b. Coercible a b => a -> b
coerce

instance FStrong (EnvT e) where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (EnvT e g) h ~> EnvT e (Day g h)
fstrength (Day (EnvT e
e g b
g) h c
h b -> c -> x
op) = e -> Day g h x -> EnvT e (Day g h) x
forall e (w :: * -> *) a. e -> w a -> EnvT e w a
EnvT e
e (g b -> h c -> (b -> c -> x) -> Day g h x
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day g b
g h c
h b -> c -> x
op)

instance FStrong (TracedT m) where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (TracedT m g) h ~> TracedT m (Day g h)
fstrength (Day (TracedT g (m -> b)
gf) h c
h b -> c -> x
op) = Day g h (m -> x) -> TracedT m (Day g h) x
forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a
TracedT (g (m -> b) -> h c -> ((m -> b) -> c -> m -> x) -> Day g h (m -> x)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day g (m -> b)
gf h c
h (\m -> b
mb c
c m
m -> b -> c -> x
op (m -> b
mb m
m) c
c))

instance FStrong (StoreT s) where
  fstrength :: forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (StoreT s g) h ~> StoreT s (Day g h)
fstrength (Day (StoreT g (s -> b)
gf s
s) h c
h b -> c -> x
op) = Day g h (s -> x) -> s -> StoreT s (Day g h) x
forall s (w :: * -> *) a. w (s -> a) -> s -> StoreT s w a
StoreT (g (s -> b) -> h c -> ((s -> b) -> c -> s -> x) -> Day g h (s -> x)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day g (s -> b)
gf h c
h (\s -> b
sb c
c s
s' -> b -> c -> x
op (s -> b
sb s
s') c
c)) s
s