-- | The indexed cowriter transformer: each @'CowriterT' κ f@ term wants within @f@ a morphism of @κ@.

module Control.Comonad.Indexed.Trans.Cowriter where

import Prelude hiding ((.), id)
import qualified Control.Applicative as Base
import Control.Category hiding ((.))
import qualified Control.Comonad as Base
import qualified Control.Monad as Base
import Control.Semigroupoid
import Data.Functor.Indexed

newtype CowriterT κ f i j a = CowriterT { CowriterT κ f i j a -> f (κ i j -> a)
runCowriterT :: f (κ i j -> a) }
  deriving (a -> CowriterT κ f i j b -> CowriterT κ f i j a
(a -> b) -> CowriterT κ f i j a -> CowriterT κ f i j b
(forall a b.
 (a -> b) -> CowriterT κ f i j a -> CowriterT κ f i j b)
-> (forall a b. a -> CowriterT κ f i j b -> CowriterT κ f i j a)
-> Functor (CowriterT κ f i j)
forall a b. a -> CowriterT κ f i j b -> CowriterT κ f i j a
forall a b. (a -> b) -> CowriterT κ f i j a -> CowriterT κ f i j b
forall k k (κ :: k -> k -> *) (f :: * -> *) (i :: k) (j :: k) a b.
Functor f =>
a -> CowriterT κ f i j b -> CowriterT κ f i j a
forall k k (κ :: k -> k -> *) (f :: * -> *) (i :: k) (j :: k) a b.
Functor f =>
(a -> b) -> CowriterT κ f i j a -> CowriterT κ f i j b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> CowriterT κ f i j b -> CowriterT κ f i j a
$c<$ :: forall k k (κ :: k -> k -> *) (f :: * -> *) (i :: k) (j :: k) a b.
Functor f =>
a -> CowriterT κ f i j b -> CowriterT κ f i j a
fmap :: (a -> b) -> CowriterT κ f i j a -> CowriterT κ f i j b
$cfmap :: forall k k (κ :: k -> k -> *) (f :: * -> *) (i :: k) (j :: k) a b.
Functor f =>
(a -> b) -> CowriterT κ f i j a -> CowriterT κ f i j b
Functor)

instance Base.Applicative p => Base.Applicative (CowriterT κ p i j) where
    pure :: a -> CowriterT κ p i j a
pure = p (κ i j -> a) -> CowriterT κ p i j a
forall k k (κ :: k -> k -> *) (f :: * -> *) (i :: k) (j :: k) a.
f (κ i j -> a) -> CowriterT κ f i j a
CowriterT (p (κ i j -> a) -> CowriterT κ p i j a)
-> (a -> p (κ i j -> a)) -> a -> CowriterT κ p i j a
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
. (κ i j -> a) -> p (κ i j -> a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((κ i j -> a) -> p (κ i j -> a))
-> (a -> κ i j -> a) -> a -> p (κ i j -> a)
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
. a -> κ i j -> a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    CowriterT x :: p (κ i j -> a -> b)
x <*> :: CowriterT κ p i j (a -> b)
-> CowriterT κ p i j a -> CowriterT κ p i j b
<*> CowriterT y :: p (κ i j -> a)
y = p (κ i j -> b) -> CowriterT κ p i j b
forall k k (κ :: k -> k -> *) (f :: * -> *) (i :: k) (j :: k) a.
f (κ i j -> a) -> CowriterT κ f i j a
CowriterT (((κ i j -> a -> b) -> (κ i j -> a) -> κ i j -> b)
-> p (κ i j -> a -> b) -> p (κ i j -> a) -> p (κ i j -> b)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
Base.liftA2 (κ i j -> a -> b) -> (κ i j -> a) -> κ i j -> b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
(Base.<*>) p (κ i j -> a -> b)
x p (κ i j -> a)
y)

instance (Base.Comonad ɯ, Category κ) => Base.Comonad (CowriterT κ ɯ k k) where
    copure :: CowriterT κ ɯ k k a -> a
copure = κ k k -> CowriterT κ ɯ k k a -> a
forall k k (ɯ :: * -> *) (κ :: k -> k -> *) (i :: k) (j :: k) a.
Comonad ɯ =>
κ i j -> CowriterT κ ɯ i j a -> a
cotell κ k k
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
    cut :: CowriterT κ ɯ k k a -> CowriterT κ ɯ k k (CowriterT κ ɯ k k a)
cut = CowriterT κ ɯ k k a -> CowriterT κ ɯ k k (CowriterT κ ɯ k k a)
forall k (ɯ :: k -> k -> * -> *) (i :: k) (k :: k) a (j :: k).
Cobind ɯ =>
ɯ i k a -> ɯ i j (ɯ j k a)
cut

instance (Base.Comonad ɯ, Semigroupoid κ) => Cobind (CowriterT κ ɯ) where
    cut :: CowriterT κ ɯ i k a -> CowriterT κ ɯ i j (CowriterT κ ɯ j k a)
cut = (ɯ (κ i k -> a) -> ɯ (κ i j -> CowriterT κ ɯ j k a))
-> CowriterT κ ɯ i k a -> CowriterT κ ɯ i j (CowriterT κ ɯ j k a)
forall k k k k (f :: * -> *) (κ :: k -> k -> *) (i :: k) (j :: k) a
       (g :: * -> *) (κ' :: k -> k -> *) (u :: k) (v :: k) b.
(f (κ i j -> a) -> g (κ' u v -> b))
-> CowriterT κ f i j a -> CowriterT κ' g u v b
mapCowriterT (ɯ (κ i k -> a)
-> (ɯ (κ i k -> a) -> κ i j -> CowriterT κ ɯ j k a)
-> ɯ (κ i j -> CowriterT κ ɯ j k a)
forall (ɯ :: * -> *) a b. Comonad ɯ => ɯ a -> (ɯ a -> b) -> ɯ b
Base.=>> \ ɯ :: ɯ (κ i k -> a)
ɯ s :: κ i j
s -> ɯ (κ j k -> a) -> CowriterT κ ɯ j k a
forall k k (κ :: k -> k -> *) (f :: * -> *) (i :: k) (j :: k) a.
f (κ i j -> a) -> CowriterT κ f i j a
CowriterT (ɯ (κ j k -> a) -> CowriterT κ ɯ j k a)
-> ɯ (κ j k -> a) -> CowriterT κ ɯ j k a
forall a b. (a -> b) -> a -> b
$ ((κ i k -> a) -> (κ j k -> κ i k) -> κ j k -> a
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
. (κ j k -> κ i j -> κ i k
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
. κ i j
s)) ((κ i k -> a) -> κ j k -> a) -> ɯ (κ i k -> a) -> ɯ (κ j k -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ɯ (κ i k -> a)
ɯ)

mapCowriterT :: (f (κ i j -> a) -> g (κ' u v -> b)) -> CowriterT κ f i j a -> CowriterT κ' g u v b
mapCowriterT :: (f (κ i j -> a) -> g (κ' u v -> b))
-> CowriterT κ f i j a -> CowriterT κ' g u v b
mapCowriterT f :: f (κ i j -> a) -> g (κ' u v -> b)
f = g (κ' u v -> b) -> CowriterT κ' g u v b
forall k k (κ :: k -> k -> *) (f :: * -> *) (i :: k) (j :: k) a.
f (κ i j -> a) -> CowriterT κ f i j a
CowriterT (g (κ' u v -> b) -> CowriterT κ' g u v b)
-> (CowriterT κ f i j a -> g (κ' u v -> b))
-> CowriterT κ f i j a
-> CowriterT κ' g u v b
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
. f (κ i j -> a) -> g (κ' u v -> b)
f (f (κ i j -> a) -> g (κ' u v -> b))
-> (CowriterT κ f i j a -> f (κ i j -> a))
-> CowriterT κ f i j a
-> g (κ' u v -> b)
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
. CowriterT κ f i j a -> f (κ i j -> a)
forall k k (κ :: k -> k -> *) (f :: * -> *) (i :: k) (j :: k) a.
CowriterT κ f i j a -> f (κ i j -> a)
runCowriterT

cotell :: Base.Comonad ɯ => κ i j -> CowriterT κ ɯ i j a -> a
cotell :: κ i j -> CowriterT κ ɯ i j a -> a
cotell κ :: κ i j
κ = ((κ i j -> a) -> κ i j -> a
forall a b. (a -> b) -> a -> b
$ κ i j
κ) ((κ i j -> a) -> a)
-> (CowriterT κ ɯ i j a -> κ i j -> a) -> CowriterT κ ɯ i j a -> a
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
. ɯ (κ i j -> a) -> κ i j -> a
forall (ɯ :: * -> *) a. Comonad ɯ => ɯ a -> a
copure (ɯ (κ i j -> a) -> κ i j -> a)
-> (CowriterT κ ɯ i j a -> ɯ (κ i j -> a))
-> CowriterT κ ɯ i j a
-> κ i j
-> a
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
. CowriterT κ ɯ i j a -> ɯ (κ i j -> a)
forall k k (κ :: k -> k -> *) (f :: * -> *) (i :: k) (j :: k) a.
CowriterT κ f i j a -> f (κ i j -> a)
runCowriterT

listen :: Functor f => CowriterT κ f i j a -> CowriterT κ f i j (a, κ i j)
listen :: CowriterT κ f i j a -> CowriterT κ f i j (a, κ i j)
listen = ((f (κ i j -> a) -> f (κ i j -> (a, κ i j)))
-> CowriterT κ f i j a -> CowriterT κ f i j (a, κ i j)
forall k k k k (f :: * -> *) (κ :: k -> k -> *) (i :: k) (j :: k) a
       (g :: * -> *) (κ' :: k -> k -> *) (u :: k) (v :: k) b.
(f (κ i j -> a) -> g (κ' u v -> b))
-> CowriterT κ f i j a -> CowriterT κ' g u v b
mapCowriterT ((f (κ i j -> a) -> f (κ i j -> (a, κ i j)))
 -> CowriterT κ f i j a -> CowriterT κ f i j (a, κ i j))
-> (((κ i j -> a) -> κ i j -> (a, κ i j))
    -> f (κ i j -> a) -> f (κ i j -> (a, κ i j)))
-> ((κ i j -> a) -> κ i j -> (a, κ i j))
-> CowriterT κ f i j a
-> CowriterT κ f i j (a, κ i j)
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
. ((κ i j -> a) -> κ i j -> (a, κ i j))
-> f (κ i j -> a) -> f (κ i j -> (a, κ i j))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) ((κ i j -> a) -> (a -> κ i j -> (a, κ i j)) -> κ i j -> (a, κ i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
Base.>>= (,))

censor :: Functor f => (κ' u v -> κ i j) -> CowriterT κ f i j a -> CowriterT κ' f u v a
censor :: (κ' u v -> κ i j) -> CowriterT κ f i j a -> CowriterT κ' f u v a
censor = (f (κ i j -> a) -> f (κ' u v -> a))
-> CowriterT κ f i j a -> CowriterT κ' f u v a
forall k k k k (f :: * -> *) (κ :: k -> k -> *) (i :: k) (j :: k) a
       (g :: * -> *) (κ' :: k -> k -> *) (u :: k) (v :: k) b.
(f (κ i j -> a) -> g (κ' u v -> b))
-> CowriterT κ f i j a -> CowriterT κ' g u v b
mapCowriterT ((f (κ i j -> a) -> f (κ' u v -> a))
 -> CowriterT κ f i j a -> CowriterT κ' f u v a)
-> ((κ' u v -> κ i j) -> f (κ i j -> a) -> f (κ' u v -> a))
-> (κ' u v -> κ i j)
-> CowriterT κ f i j a
-> CowriterT κ' f u v a
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
. ((κ i j -> a) -> κ' u v -> a) -> f (κ i j -> a) -> f (κ' u v -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((κ i j -> a) -> κ' u v -> a)
 -> f (κ i j -> a) -> f (κ' u v -> a))
-> ((κ' u v -> κ i j) -> (κ i j -> a) -> κ' u v -> a)
-> (κ' u v -> κ i j)
-> f (κ i j -> a)
-> f (κ' u v -> a)
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
. ((κ i j -> a) -> (κ' u v -> κ i j) -> κ' u v -> a)
-> (κ' u v -> κ i j) -> (κ i j -> a) -> κ' u v -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (κ i j -> a) -> (κ' u v -> κ i j) -> κ' u v -> a
forall k (κ :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Semigroupoid κ =>
κ b c -> κ a b -> κ a c
(.)