{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE LambdaCase #-}

-- | Monad transformer from @Comonad@.
--
-- This module provides the 'CoT' monad transformer, which adds a "comonadic context"
-- to another monad.
--
-- ==== What does @CoT@ do?
--
-- For any @Comonad f@ and @Monad g@, @CoT f g@ is a monad that combines the original
-- effect of the monad @g@ with the ability to use the comonad @f@ as a context. For example:
--
-- * @CoT ('Env' e) g@ is a monad with the @g@ effect and access to a value of type @e@.
--
--     * This is exactly what @'ReaderT' e g@ provides, and in fact, @CoT (Env e) g@ is isomorphic to
--       @ReaderT e g@: see 'fromReaderT' and 'toReaderT'.
--
-- * @CoT ('Store' s) g@ is a monad with the @g@ effect and access to a context that holds
--   a store of @s@ values, which can be queried or updated.
--
--     * This corresponds exactly to what @'StateT' s g@ provides, and indeed,
--       @CoT (Store s) g@ is isomorphic to @StateT s g@: see 'fromStateT' and 'toStateT'.
--
-- * Similarly, @CoT ('Traced' m) g@ is isomorphic to @'WriterT' m g@.
--
-- The "contextual" effects introduced by @CoT@ can be composed freely. Any nested use of the
-- @CoT@ monad transformer can be flattened into a single layer using the 'Day' functor to
-- combine the contexts:
--
-- @
-- uncurryCoT :: Functor g => CoT f1 (CoT f2 g) ~> CoT (Day f1 f2) g
-- curryCoT   :: Functor g => CoT (Day f1 f2) g ~> CoT f1 (CoT f2 g)
-- @
--
-- ==== Relation to other types
--
-- As a @Functor@, @CoT f g@ is isomorphic to the @'Curried' f g@ type.
-- However, since @Curried@ has an @Applicative@ instance that is not compatible
-- with the @Monad@ instance of @CoT@, a new type was necessary to support the monad
-- behavior described here.
--
-- The non-transformer version, @'Co' f@, is isomorphic to the
-- @'Control.Monad.Co.Co' f@ type from the "Control.Monad.Co" module
-- (which is actually the source of inspiration for this module!).
--
-- The name collision is unfortunate — the author has not yet decided on a final name
-- for this monad transformer. Suggestions are welcome!
--
-- ==== For category theory nerds
-- 
-- The construction of monad @CoT f g@, given @Comonad f@ and @Monad g@,
-- can be explained via Kleisli category.
-- 
-- Recall that providing a @Monad@ instance for a functor @m@ is equivalent to
-- providing a @Category (Kleisli m)@ instance.
--
-- @
-- -- The type of Kleisli category morphisms
-- newtype Kleisli m a b = Kl { runKl :: a -> m b }
-- 
-- -- Derive @Category (Kleisli m)@ from @Monad m@
-- instance Monad m => Category (Kleisli m) where
--   id :: Kleisli m a a
--   id = Kl return
--   (.) :: Kleisli m b c -> Kleisli m a b -> Kleisli m a c
--   Kl f . Kl g = Kl (f <=< g)
--
-- -- Derive @Monad m@ from @Category (Kleisli m)@
-- -- (pseudocode, can't be real Haskell)
-- instance Category (Kleisli m) => Monad m where
--   return = runKl id
--   ma >>= k = runKl (Kl k . Kl (const ma)) ()
-- @
-- 
-- @Kleisli (CoT f g)@ is isomorphic to the following @Arr f g@.
--
-- @
-- type Arr f g a b = forall r. (a, f r) -> g (b, r)
-- @
-- 
-- Here's the transformations showing the isomorphism between @Kleisli (CoT f g)@ and @Arr f g@.
-- 
-- @
-- Kleisli (CoT f g) a b
--  ≅ a -> CoT f g b
--  ≅ a -> ∀r. f r -> g (b, r)
--  ≅ ∀r. a -> f r -> g (b, r)
--  ≅ ∀r. (a, f r) -> g (b, r)
--  ~ Arr f g a b
-- @
-- 
-- @Arr f g@ can be made into @Category@ with the following identity and composition.
-- The @Monad (CoT f g)@ instance is the one derived from this construction.
--
-- @
-- idArr :: (Comonad f, Monad g) => Arr f g a a
-- idArr (a, fr) = pure (a, extract fr)
--
-- compArr :: (Comonad f, Monad g) => Arr f g a b -> Arr f g b c -> Arr f g a c
-- compArr t u (a, fr) =
--   t (a, duplicate fr) >>= u
-- @
-- 
-- Diagramatically, @idArr@ is the following composite
-- 
-- \[
-- \require{AMScd}
-- \begin{CD}
-- (a, \_) \circ f @>>{\mathop{\mathtt{fmap}} \mathop{\mathtt{extract}}}> (a, \_) @>>{\mathtt{pure}}> g \circ (a, \_)
-- \end{CD}
-- \]
--
-- and @compArr t u@ is the following composite. 
-- 
-- \[
-- \require{AMScd}
-- \begin{CD}
-- (a, \_) \circ f
--   @>>{\mathop{\mathtt{fmap}} \mathop{\mathtt{duplicate}}}>
-- (a, \_) \circ f \circ f
--   @>>{t}>
-- g \circ (b, \_) \circ f
--   @>>{\mathop{\mathtt{fmap}} u}>
-- g \circ g \circ (c, \_)
--   @>>{\mathop{\mathtt{join}}}>
-- g \circ (c, \_)
-- \end{CD}
-- \]
-- 
-- Proving category laws for @(idArr, compArr)@ will be simple enough.
module Control.Monad.CoComonad(
  -- * The @CoT@ monad transformer
  CoT(..),

  -- ** Manipulating comonadic part
  contrahoist,
  elimCoT,
  curryCoT,
  uncurryCoT,
  eitherCoT, uneitherCoT,

  -- ** Representing @Reader@, @Writer@, or @State@ effects
  toReaderT, toWriterT, toStateT,
  fromReaderT, fromWriterT, fromStateT,
  asking, telling, stating,

  -- ** Conversion
  toCurried,
  fromCurried,

  -- * Non-transformer version
  type Co,
  co, runCo,
  generalize,
  
  -- ** Conversion
  --
  -- The other @Control.Monad.Co.Co@ monad (in @Control.Monad.Co@ module)
  -- is isomorphic to 'Co' defined here.
  --
  -- @Control.Monad.Co.CoT@ is a kind of @Codensity@ monad with access to some @Comonad@ context,
  -- thus the name.
  
  toCodensityCo,
  fromCodensityCo,
) where

import Control.Monad
import Data.Functor.Day.Curried (Curried(..))
import FFunctor
import Control.Monad.Morph
import Data.Functor.Identity

import Control.Monad.IO.Class (MonadIO(..))

import Control.Comonad (Comonad(..))
import Control.Comonad.Env (ComonadEnv(..), Env, env)
import Control.Comonad.Traced (ComonadTraced(..), Traced, traced)
import Control.Comonad.Store (ComonadStore(..), Store, store)
import Control.Monad.Trans.Reader (ReaderT(..))
import Control.Monad.Trans.Writer (WriterT (..))
import Control.Monad.Trans.State (StateT (..))
import qualified Control.Monad.Reader.Class as Reader
import qualified Control.Monad.Writer.Class as Writer
import qualified Control.Monad.State.Class as State
import Data.Functor.Day (Day (..))
import Data.Function ((&))
import Data.Functor.Sum (Sum (..))
import Data.Functor.Product (Product (..))
import qualified Control.Monad.Co

-- | @CoT f g@ is a @Monad@ which is based on @Monad g@ but can use @Comonad f@
--   as a context. 
newtype CoT f g a = CoT { forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT :: forall r. f r -> g (a, r) }
  deriving stock (forall a b. (a -> b) -> CoT f g a -> CoT f g b)
-> (forall a b. a -> CoT f g b -> CoT f g a) -> Functor (CoT f g)
forall a b. a -> CoT f g b -> CoT f g a
forall a b. (a -> b) -> CoT f g a -> CoT f g b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (f :: * -> *) (g :: * -> *) a b.
Functor g =>
a -> CoT f g b -> CoT f g a
forall (f :: * -> *) (g :: * -> *) a b.
Functor g =>
(a -> b) -> CoT f g a -> CoT f g b
$cfmap :: forall (f :: * -> *) (g :: * -> *) a b.
Functor g =>
(a -> b) -> CoT f g a -> CoT f g b
fmap :: forall a b. (a -> b) -> CoT f g a -> CoT f g b
$c<$ :: forall (f :: * -> *) (g :: * -> *) a b.
Functor g =>
a -> CoT f g b -> CoT f g a
<$ :: forall a b. a -> CoT f g b -> CoT f g a
Functor

-- | As a mere @Functor@, @CoT f g@ is isomorphic to @'Curried' f g@.
toCurried :: Functor g => CoT f g ~> Curried f g
toCurried :: forall (g :: * -> *) (f :: * -> *).
Functor g =>
CoT f g ~> Curried f g
toCurried CoT f g x
ta = (forall r. f (x -> r) -> g r) -> Curried f g x
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried ((forall r. f (x -> r) -> g r) -> Curried f g x)
-> (forall r. f (x -> r) -> g r) -> Curried f g x
forall a b. (a -> b) -> a -> b
$ \f (x -> r)
far -> (x -> (x -> r) -> r) -> (x, x -> r) -> r
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry x -> (x -> r) -> r
forall a b. a -> (a -> b) -> b
(&) ((x, x -> r) -> r) -> g (x, x -> r) -> g r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoT f g x -> forall r. f r -> g (x, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT CoT f g x
ta f (x -> r)
far

-- | The inverse of 'toCurried'
fromCurried :: Functor f => Curried f g ~> CoT f g
fromCurried :: forall (f :: * -> *) (g :: * -> *).
Functor f =>
Curried f g ~> CoT f g
fromCurried Curried f g x
ca = (forall r. f r -> g (x, r)) -> CoT f g x
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((forall r. f r -> g (x, r)) -> CoT f g x)
-> (forall r. f r -> g (x, r)) -> CoT f g x
forall a b. (a -> b) -> a -> b
$ \f r
fr -> Curried f g x -> forall r. f (x -> r) -> g r
forall (g :: * -> *) (h :: * -> *) a.
Curried g h a -> forall r. g (a -> r) -> h r
runCurried Curried f g x
ca ((x -> r -> (x, r)) -> r -> x -> (x, r)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) (r -> x -> (x, r)) -> f r -> f (x -> (x, r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f r
fr)

instance (Comonad f, Monad g) => Applicative (CoT f g) where
  pure :: forall a. a -> CoT f g a
pure a
a = (forall r. f r -> g (a, r)) -> CoT f g a
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((forall r. f r -> g (a, r)) -> CoT f g a)
-> (forall r. f r -> g (a, r)) -> CoT f g a
forall a b. (a -> b) -> a -> b
$ \f r
fr -> (a, r) -> g (a, r)
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, f r -> r
forall a. f a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract f r
fr)
  <*> :: forall a b. CoT f g (a -> b) -> CoT f g a -> CoT f g b
(<*>) = CoT f g (a -> b) -> CoT f g a -> CoT f g b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (Comonad f, Monad g) => Monad (CoT f g) where
  CoT f g a
ta >>= :: forall a b. CoT f g a -> (a -> CoT f g b) -> CoT f g b
>>= a -> CoT f g b
k = (forall r. f r -> g (b, r)) -> CoT f g b
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((forall r. f r -> g (b, r)) -> CoT f g b)
-> (forall r. f r -> g (b, r)) -> CoT f g b
forall a b. (a -> b) -> a -> b
$ \f r
fr -> do
    (a
a, f r
fr') <- CoT f g a -> forall r. f r -> g (a, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT CoT f g a
ta (f r -> f (f r)
forall a. f a -> f (f a)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate f r
fr)
    CoT f g b -> forall r. f r -> g (b, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT (a -> CoT f g b
k a
a) f r
fr'

instance MFunctor (CoT f) where
  hoist :: Monad g => (forall a. g a -> h a) -> CoT f g b -> CoT f h b
  hoist :: forall (m :: * -> *) (n :: * -> *) b.
Monad m =>
(forall a. m a -> n a) -> CoT f m b -> CoT f n b
hoist forall a. g a -> h a
gh (CoT forall r. f r -> g (b, r)
fg) = (forall r. f r -> h (b, r)) -> CoT f h b
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT (g (b, r) -> h (b, r)
forall a. g a -> h a
gh (g (b, r) -> h (b, r)) -> (f r -> g (b, r)) -> f r -> h (b, r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f r -> g (b, r)
forall r. f r -> g (b, r)
fg)

instance (Comonad f) => MonadTrans (CoT f) where
  lift :: Monad g => g a -> CoT f g a
  lift :: forall (m :: * -> *) a. Monad m => m a -> CoT f m a
lift g a
ga = (forall r. f r -> g (a, r)) -> CoT f g a
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((forall r. f r -> g (a, r)) -> CoT f g a)
-> (forall r. f r -> g (a, r)) -> CoT f g a
forall a b. (a -> b) -> a -> b
$ \f r
fr -> ( , f r -> r
forall a. f a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract f r
fr) (a -> (a, r)) -> g a -> g (a, r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a
ga

instance (Comonad f, MonadIO g) => MonadIO (CoT f g) where
  liftIO :: forall a. IO a -> CoT f g a
liftIO = g a -> CoT f g a
forall (m :: * -> *) a. Monad m => m a -> CoT f m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (g a -> CoT f g a) -> (IO a -> g a) -> IO a -> CoT f g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> g a
forall a. IO a -> g a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO


-- | Change of the @Comonad@ part.
--
-- @contrahoist φ@ is a monad morphism @CoT k g ~> CoT f g@ /if/ @φ :: f ~> k@
-- is a comonad morphism.
contrahoist :: (forall x. f x -> k x) -> CoT k g a -> CoT f g a
contrahoist :: forall (f :: * -> *) (k :: * -> *) (g :: * -> *) a.
(forall x. f x -> k x) -> CoT k g a -> CoT f g a
contrahoist forall x. f x -> k x
fk (CoT forall r. k r -> g (a, r)
kg) = (forall r. f r -> g (a, r)) -> CoT f g a
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT (k r -> g (a, r)
forall r. k r -> g (a, r)
kg (k r -> g (a, r)) -> (f r -> k r) -> f r -> g (a, r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f r -> k r
forall x. f x -> k x
fk)

-- | When the context @f@ can be constructed as @pure x : f a@,
--   @CoT f@ can be removed by supplying the \"pure\" context.
-- 
--   There are two notable special cases of 'elimCoT':
--
--   @
--   -- If the context f is Identity comonad, 'elimCoT' is monad isomorphism and
--   -- is the inverse of @lift@.
--   elimCoT :: (Functor g) => CoT 'Identity' g ~> g
--   @
--
--   @
--   -- If the context f is NonEmpty comonad, 'elimCoT' is monad morphism,
--   -- and @elimCoT . lift = id@ holds.
--   elimCoT :: (Functor g) => CoT 'Data.List.NonEmpty.NonEmpty' g ~> g
--   @
elimCoT :: (Applicative f, Functor g) => CoT f g ~> g
elimCoT :: forall (f :: * -> *) (g :: * -> *).
(Applicative f, Functor g) =>
CoT f g ~> g
elimCoT CoT f g x
ig = (x, ()) -> x
forall a b. (a, b) -> a
fst ((x, ()) -> x) -> g (x, ()) -> g x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoT f g x -> forall r. f r -> g (x, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT CoT f g x
ig (() -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

-- | Nesting of @CoT f1@ and @CoT f2@ can be represented as a single @CoT (Day f1 f2)@ using 
--   'Day' to combine two comonads.
--
-- This is also a /monad isomorphism/.
uncurryCoT :: (Functor g) => CoT f1 (CoT f2 g) ~> CoT (Day f1 f2) g
uncurryCoT :: forall (g :: * -> *) (f1 :: * -> *) (f2 :: * -> *).
Functor g =>
CoT f1 (CoT f2 g) ~> CoT (Day f1 f2) g
uncurryCoT CoT f1 (CoT f2 g) x
tt = (forall r. Day f1 f2 r -> g (x, r)) -> CoT (Day f1 f2) g x
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((forall r. Day f1 f2 r -> g (x, r)) -> CoT (Day f1 f2) g x)
-> (forall r. Day f1 f2 r -> g (x, r)) -> CoT (Day f1 f2) g x
forall a b. (a -> b) -> a -> b
$ \(Day f1 b
f1b f2 c
f2c b -> c -> r
op) ->
  (\((x
a,b
b),c
c) -> (x
a, b -> c -> r
op b
b c
c)) (((x, b), c) -> (x, r)) -> g ((x, b), c) -> g (x, r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoT f1 (CoT f2 g) x
tt CoT f1 (CoT f2 g) x -> forall r. f1 r -> CoT f2 g (x, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
`runCoT` f1 b
f1b) CoT f2 g (x, b) -> forall r. f2 r -> g ((x, b), r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
`runCoT` f2 c
f2c

-- | The inverse of 'uncurryCo'.
curryCoT :: Functor g => CoT (Day f1 f2) g ~> CoT f1 (CoT f2 g)
curryCoT :: forall (g :: * -> *) (f1 :: * -> *) (f2 :: * -> *).
Functor g =>
CoT (Day f1 f2) g ~> CoT f1 (CoT f2 g)
curryCoT CoT (Day f1 f2) g x
t = (forall r. f1 r -> CoT f2 g (x, r)) -> CoT f1 (CoT f2 g) x
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((forall r. f1 r -> CoT f2 g (x, r)) -> CoT f1 (CoT f2 g) x)
-> (forall r. f1 r -> CoT f2 g (x, r)) -> CoT f1 (CoT f2 g) x
forall a b. (a -> b) -> a -> b
$ \f1 r
f1b ->
  (forall r. f2 r -> g ((x, r), r)) -> CoT f2 g (x, r)
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((forall r. f2 r -> g ((x, r), r)) -> CoT f2 g (x, r))
-> (forall r. f2 r -> g ((x, r), r)) -> CoT f2 g (x, r)
forall a b. (a -> b) -> a -> b
$ \f2 r
f2c ->
    (\(x
a,(r
b,r
c)) -> ((x
a,r
b),r
c)) ((x, (r, r)) -> ((x, r), r)) -> g (x, (r, r)) -> g ((x, r), r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoT (Day f1 f2) g x -> forall r. Day f1 f2 r -> g (x, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT CoT (Day f1 f2) g x
t (f1 r -> f2 r -> (r -> r -> (r, r)) -> Day f1 f2 (r, r)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day f1 r
f1b f2 r
f2c (,))

-- * Consuming @Env, Traced, Store@ coeffects === Effects @Reader, Writer, State@

toReaderT :: (Monad g) => CoT (Env e) g a -> ReaderT e g a
toReaderT :: forall (g :: * -> *) e a.
Monad g =>
CoT (Env e) g a -> ReaderT e g a
toReaderT CoT (Env e) g a
ta = (e -> g a) -> ReaderT e g a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((e -> g a) -> ReaderT e g a) -> (e -> g a) -> ReaderT e g a
forall a b. (a -> b) -> a -> b
$ \e
e -> (a, ()) -> a
forall a b. (a, b) -> a
fst ((a, ()) -> a) -> g (a, ()) -> g a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoT (Env e) g a -> forall r. Env e r -> g (a, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT CoT (Env e) g a
ta (e -> () -> Env e ()
forall e a. e -> a -> Env e a
env e
e ())

toWriterT :: (Monad g) => CoT (Traced m) g a -> WriterT m g a
toWriterT :: forall (g :: * -> *) m a.
Monad g =>
CoT (Traced m) g a -> WriterT m g a
toWriterT CoT (Traced m) g a
ta = g (a, m) -> WriterT m g a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (g (a, m) -> WriterT m g a) -> g (a, m) -> WriterT m g a
forall a b. (a -> b) -> a -> b
$ CoT (Traced m) g a -> forall r. Traced m r -> g (a, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT CoT (Traced m) g a
ta ((m -> m) -> Traced m m
forall m a. (m -> a) -> Traced m a
traced m -> m
forall a. a -> a
id)

toStateT :: (Monad g) => CoT (Store s) g a -> StateT s g a
toStateT :: forall (g :: * -> *) s a.
Monad g =>
CoT (Store s) g a -> StateT s g a
toStateT CoT (Store s) g a
ta = (s -> g (a, s)) -> StateT s g a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((s -> g (a, s)) -> StateT s g a)
-> (s -> g (a, s)) -> StateT s g a
forall a b. (a -> b) -> a -> b
$ \s
s0 -> CoT (Store s) g a -> forall r. Store s r -> g (a, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT CoT (Store s) g a
ta ((s -> s) -> s -> Store s s
forall s a. (s -> a) -> s -> Store s a
store s -> s
forall a. a -> a
id s
s0)

fromReaderT :: (ComonadEnv e f, Monad g) => ReaderT e g a -> CoT f g a
fromReaderT :: forall e (f :: * -> *) (g :: * -> *) a.
(ComonadEnv e f, Monad g) =>
ReaderT e g a -> CoT f g a
fromReaderT ReaderT e g a
ma = (forall r. f r -> g (a, r)) -> CoT f g a
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((forall r. f r -> g (a, r)) -> CoT f g a)
-> (forall r. f r -> g (a, r)) -> CoT f g a
forall a b. (a -> b) -> a -> b
$ \f r
fr -> ( , f r -> r
forall a. f a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract f r
fr) (a -> (a, r)) -> g a -> g (a, r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT e g a -> e -> g a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT e g a
ma (f r -> e
forall a. f a -> e
forall e (w :: * -> *) a. ComonadEnv e w => w a -> e
ask f r
fr)

fromWriterT :: (ComonadTraced m f, Monad g) => WriterT m g a -> CoT f g a
fromWriterT :: forall m (f :: * -> *) (g :: * -> *) a.
(ComonadTraced m f, Monad g) =>
WriterT m g a -> CoT f g a
fromWriterT WriterT m g a
ma = (forall r. f r -> g (a, r)) -> CoT f g a
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((forall r. f r -> g (a, r)) -> CoT f g a)
-> (forall r. f r -> g (a, r)) -> CoT f g a
forall a b. (a -> b) -> a -> b
$ \f r
fr -> (\(a
a,m
m) -> (a
a, m -> f r -> r
forall a. m -> f a -> a
forall m (w :: * -> *) a. ComonadTraced m w => m -> w a -> a
trace m
m f r
fr)) ((a, m) -> (a, r)) -> g (a, m) -> g (a, r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WriterT m g a -> g (a, m)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT WriterT m g a
ma

fromStateT :: (ComonadStore s f, Monad g) => StateT s g a -> CoT f g a
fromStateT :: forall s (f :: * -> *) (g :: * -> *) a.
(ComonadStore s f, Monad g) =>
StateT s g a -> CoT f g a
fromStateT StateT s g a
ma = (forall r. f r -> g (a, r)) -> CoT f g a
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((forall r. f r -> g (a, r)) -> CoT f g a)
-> (forall r. f r -> g (a, r)) -> CoT f g a
forall a b. (a -> b) -> a -> b
$ \f r
fr ->
  (\(a
a,s
s1) -> (a
a, s -> f r -> r
forall a. s -> f a -> a
forall s (w :: * -> *) a. ComonadStore s w => s -> w a -> a
peek s
s1 f r
fr)) ((a, s) -> (a, r)) -> g (a, s) -> g (a, r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT s g a -> s -> g (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT s g a
ma (f r -> s
forall a. f a -> s
forall s (w :: * -> *) a. ComonadStore s w => w a -> s
pos f r
fr)

asking :: (ComonadEnv e f, Monad g) => CoT f g e
asking :: forall e (f :: * -> *) (g :: * -> *).
(ComonadEnv e f, Monad g) =>
CoT f g e
asking = ReaderT e g e -> CoT f g e
forall e (f :: * -> *) (g :: * -> *) a.
(ComonadEnv e f, Monad g) =>
ReaderT e g a -> CoT f g a
fromReaderT ReaderT e g e
forall r (m :: * -> *). MonadReader r m => m r
Reader.ask

telling :: (Monoid m, ComonadTraced m f, Monad g) => m -> CoT f g ()
telling :: forall m (f :: * -> *) (g :: * -> *).
(Monoid m, ComonadTraced m f, Monad g) =>
m -> CoT f g ()
telling m
m = WriterT m g () -> CoT f g ()
forall m (f :: * -> *) (g :: * -> *) a.
(ComonadTraced m f, Monad g) =>
WriterT m g a -> CoT f g a
fromWriterT (m -> WriterT m g ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
Writer.tell m
m)

stating :: (ComonadStore s f, Monad g) => (s -> (a, s)) -> CoT f g a
stating :: forall s (f :: * -> *) (g :: * -> *) a.
(ComonadStore s f, Monad g) =>
(s -> (a, s)) -> CoT f g a
stating s -> (a, s)
st = StateT s g a -> CoT f g a
forall s (f :: * -> *) (g :: * -> *) a.
(ComonadStore s f, Monad g) =>
StateT s g a -> CoT f g a
fromStateT ((s -> (a, s)) -> StateT s g a
forall a. (s -> (a, s)) -> StateT s g a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state s -> (a, s)
st)

-- * Sum and Product

-- | Product of @CoT@ into the same monad is @CoT@ from the sum of comonads.
--
-- Compare it with 'either' function:
-- 
-- @
-- either  :: (a -> c) -> (b -> c) -> (Either a b -> c)
-- either' :: (a -> c, b -> c) -> (Either a b -> c)
-- @
--
-- @eitherCoT@ is a /monad isomorphism/ (witnessed by 'uneitherCoT'.)
eitherCoT :: Product (CoT f1 g) (CoT f2 g) ~> CoT (Sum f1 f2) g
eitherCoT :: forall (f1 :: * -> *) (g :: * -> *) (f2 :: * -> *) x.
Product (CoT f1 g) (CoT f2 g) x -> CoT (Sum f1 f2) g x
eitherCoT (Pair CoT f1 g x
fg1 CoT f2 g x
fg2) = (forall r. Sum f1 f2 r -> g (x, r)) -> CoT (Sum f1 f2) g x
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((forall r. Sum f1 f2 r -> g (x, r)) -> CoT (Sum f1 f2) g x)
-> (forall r. Sum f1 f2 r -> g (x, r)) -> CoT (Sum f1 f2) g x
forall a b. (a -> b) -> a -> b
$ \case
  InL f1 r
f1 -> CoT f1 g x -> forall r. f1 r -> g (x, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT CoT f1 g x
fg1 f1 r
f1
  InR f2 r
f2 -> CoT f2 g x -> forall r. f2 r -> g (x, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT CoT f2 g x
fg2 f2 r
f2

-- | The inverse of 'eitherCoT'.
uneitherCoT :: CoT (Sum f1 f2) g ~> Product (CoT f1 g) (CoT f2 g)
uneitherCoT :: forall (f1 :: * -> *) (f2 :: * -> *) (g :: * -> *) x.
CoT (Sum f1 f2) g x -> Product (CoT f1 g) (CoT f2 g) x
uneitherCoT CoT (Sum f1 f2) g x
sum2g = CoT f1 g x -> CoT f2 g x -> Product (CoT f1 g) (CoT f2 g) x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair ((forall x. f1 x -> Sum f1 f2 x)
-> CoT (Sum f1 f2) g x -> CoT f1 g x
forall (f :: * -> *) (k :: * -> *) (g :: * -> *) a.
(forall x. f x -> k x) -> CoT k g a -> CoT f g a
contrahoist f1 x -> Sum f1 f2 x
forall x. f1 x -> Sum f1 f2 x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL CoT (Sum f1 f2) g x
sum2g) ((forall x. f2 x -> Sum f1 f2 x)
-> CoT (Sum f1 f2) g x -> CoT f2 g x
forall (f :: * -> *) (k :: * -> *) (g :: * -> *) a.
(forall x. f x -> k x) -> CoT k g a -> CoT f g a
contrahoist f2 x -> Sum f1 f2 x
forall x. f2 x -> Sum f1 f2 x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR CoT (Sum f1 f2) g x
sum2g)

-- * Non-transformer version

-- | Non-transformer version of @CoT@.
type Co f = CoT f Identity

co :: (forall r. f r -> (a,r)) -> Co f a
co :: forall (f :: * -> *) a. (forall r. f r -> (a, r)) -> Co f a
co forall r. f r -> (a, r)
k = (forall r. f r -> Identity (a, r)) -> CoT f Identity a
forall (f :: * -> *) (g :: * -> *) a.
(forall r. f r -> g (a, r)) -> CoT f g a
CoT ((a, r) -> Identity (a, r)
forall a. a -> Identity a
Identity ((a, r) -> Identity (a, r))
-> (f r -> (a, r)) -> f r -> Identity (a, r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f r -> (a, r)
forall r. f r -> (a, r)
k)

runCo :: Co f a -> f r -> (a, r)
runCo :: forall (f :: * -> *) a r. Co f a -> f r -> (a, r)
runCo Co f a
c f r
fr = Identity (a, r) -> (a, r)
forall a. Identity a -> a
runIdentity (Identity (a, r) -> (a, r)) -> Identity (a, r) -> (a, r)
forall a b. (a -> b) -> a -> b
$ Co f a -> forall r. f r -> Identity (a, r)
forall (f :: * -> *) (g :: * -> *) a.
CoT f g a -> forall r. f r -> g (a, r)
runCoT Co f a
c f r
fr

toCodensityCo :: Functor f => Co f ~> Control.Monad.Co.Co f
toCodensityCo :: forall (f :: * -> *). Functor f => Co f ~> Co f
toCodensityCo Co f x
c = (forall r. f (x -> r) -> r) -> Co f x
forall (w :: * -> *) a.
Functor w =>
(forall r. w (a -> r) -> r) -> Co w a
Control.Monad.Co.co ((forall r. f (x -> r) -> r) -> Co f x)
-> (forall r. f (x -> r) -> r) -> Co f x
forall a b. (a -> b) -> a -> b
$ \f (x -> r)
far -> Identity r -> r
forall a. Identity a -> a
runIdentity (Identity r -> r) -> Identity r -> r
forall a b. (a -> b) -> a -> b
$ Curried f Identity x -> forall r. f (x -> r) -> Identity r
forall (g :: * -> *) (h :: * -> *) a.
Curried g h a -> forall r. g (a -> r) -> h r
runCurried (Co f x -> Curried f Identity x
CoT f Identity ~> Curried f Identity
forall (g :: * -> *) (f :: * -> *).
Functor g =>
CoT f g ~> Curried f g
toCurried Co f x
c) f (x -> r)
far

fromCodensityCo :: Functor f => Control.Monad.Co.Co f ~> Co f
fromCodensityCo :: forall (f :: * -> *). Functor f => Co f ~> Co f
fromCodensityCo Co f x
c = Curried f Identity x -> CoT f Identity x
Curried f Identity ~> CoT f Identity
forall (f :: * -> *) (g :: * -> *).
Functor f =>
Curried f g ~> CoT f g
fromCurried (Curried f Identity x -> CoT f Identity x)
-> Curried f Identity x -> CoT f Identity x
forall a b. (a -> b) -> a -> b
$ (forall r. f (x -> r) -> Identity r) -> Curried f Identity x
forall (g :: * -> *) (h :: * -> *) a.
(forall r. g (a -> r) -> h r) -> Curried g h a
Curried ((forall r. f (x -> r) -> Identity r) -> Curried f Identity x)
-> (forall r. f (x -> r) -> Identity r) -> Curried f Identity x
forall a b. (a -> b) -> a -> b
$ \f (x -> r)
far -> Co f x -> f (x -> Identity r) -> Identity r
forall (w :: * -> *) a r. Functor w => Co w a -> w (a -> r) -> r
Control.Monad.Co.runCo Co f x
c ((r -> Identity r
forall a. a -> Identity a
Identity (r -> Identity r) -> (x -> r) -> x -> Identity r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((x -> r) -> x -> Identity r) -> f (x -> r) -> f (x -> Identity r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (x -> r)
far)