The dual to Mo. A new comonad-to-monad transformer.

Como.hs

{-# LANGUAGE RankNTypes #-}
module Como where
import Control.Comonad
import Control.Monad.Identity
import Control.Monad.Trans

-- The dual to Mo.
-- Simplified (still isomorphic): ComoT { runComoT' :: forall r. (a -> m (w r)) -> m r }
-- ComoT w Identity ~ forall r. (a -> w r) -> r
-- Unlike (Mo m Identity), (ComoT w Identity) is interesting in its own right. In fact, it gives rise to some really strange monads. See below.
-- Check the bottom for a proof that ComoT actually builds proper monads.
newtype ComoT w m a = ComoT { runComoT :: forall r. (forall b. (w r -> b) -> a -> m b) -> m r }

-- compare Mo's:  (forall b. (b -> m r) -> w b -> a)      -- Transforms a Kleisli arrow into a Cokleisli arrow
-- with Como's:   (forall b. (w r -> b) -> a -> m b)      -- Transforms a Cokleisli arrow into a Kleisli arrow
-- I suspect this is more than just coincidence.


comoT' :: (forall r. (a -> m (w r)) -> m r) -> ComoT w m a
comoT' c = ComoT $ \c' -> c $ c' id

runComoT' :: Functor m => ComoT w m a -> (a -> m (w r)) -> m r
runComoT' cm f = runComoT cm $ \wr_c a -> fmap wr_c (f a)

type Como w = ComoT w Identity

runComo :: Como w a -> (a -> w r) -> r
runComo cm f = runIdentity $ runComoT cm $ \wr_b a -> Identity (wr_b (f a))

como :: (forall r. (forall b. (w r -> b) -> a -> b) -> r) -> Como w a
como f = ComoT $ \c -> Identity $ f $ \wr_b a -> runIdentity $ c wr_b a

como' :: (forall r. (a -> w r) -> r) -> Como w a
como' f = ComoT $ \c -> Identity . f $ runIdentity . c id

instance Functor (ComoT w m) where
    fmap f m = ComoT $ \c -> runComoT m $ \wr_c -> c wr_c . f

instance Comonad w => Applicative (ComoT w m) where
    pure a = ComoT $ \c -> c extract a
    ff <*> fa = ComoT $ \c -> runComoT ff $ \wr_b1 f -> runComoT fa $ \wb1_b2 a -> c (wr_b1 =>= wb1_b2) (f a)

instance Comonad w => Monad (ComoT w m) where
    m >>= f = ComoT $ \c -> runComoT m $ \wr_b1 a -> runComoT (f a) $ \wb1_b2 b -> c (wr_b1 =>= wb1_b2) b

instance Comonad w => MonadTrans (ComoT w) where
    lift ma = ComoT $ \c -> ma >>= c extract

{-

Like Co,
  Como ((->) s) a           ~ forall r. (a -> (s -> r)) -> r
                            ~ forall r. (s -> a -> r) -> r
                            ~ forall r. ((s, a) -> r) -> r
                            ~ Yoneda Identity (s, a)
                            ~ (s, a)

Unlike Co,
  Como ((,) s) a            ~ forall r. (a -> (s, r)) -> r
                            ~ forall r. (a -> s, a -> r) -> r
                            ~ forall r. (a -> s) -> (a -> r) -> r
                            ~ forall r. (a -> r) -> (a -> s) -> r
                            ~ Yoneda ((->) (a -> s)) a
                            ~ (a -> s) -> a
  Como (Store s) a          ~ forall r. (a -> (s, s -> r)) -> r
                            ~ forall r. (a -> s, a -> s -> r) -> r
                            ~ forall r. (a -> s) -> (a -> s -> r) -> r
                            ~ forall r. (a -> s -> r) -> (a -> s) -> r
                            ~ forall r. ((a, s) -> r) -> (a -> s) -> r
                            ~ Yoneda ((->) (a -> s)) (a, s)
                            ~ (a -> s) -> (a, s)

Como ((,) s) is Select in Control.Monad.Trans.Select from the transformers library.
Como (Store s) I don't recognize.

For the moment, I'm calling it Dull.
Dull is a very forced pun. Given a morphism, which could be seen as an edge between two objects, a Dull returns a pair of values of respective "vertix".
Get it? Dulling the edge?
-}

newtype Dull s a = Dull { runDull :: (a -> s) -> (a, s) }

-- I believe these instances represent the monad (Como (Store s) Identity) creates
instance Functor (Dull s) where
    fmap f m = Dull $ \bs -> case runDull m (bs . f) of
        ~(a, s) -> (f a, s)

instance Applicative (Dull s) where
    pure a = Dull $ \as -> (a, as a)
    (<*>) = ap

instance Monad (Dull s) where
    m >>= f = Dull $ \bs -> case (runDull m $ \a -> snd $ runDull (f a) bs) of
        ~(a, s) -> (fst $ runDull (f a) bs, s) -- I think it's this rather than simply "runDull (fa) bs"

through :: (s -> s) -> Dull s ()
through f = Dull $ \c -> ((), f (c ()))

with :: s -> Dull s s
with s = Dull $ \ss -> (ss s, ss s)

{-

Proof that (ComoT w m) is a monad.

I'll be using the following definition for join:
join m = ComoT $ \c -> runComoT m $ \wr_b1 m' -> runComoT m' $ \wb1_b2 -> c (wr_b1 =>= wb1_b2)

join . pure === id
  join (pure m)
      -- definition of pure
    === join $ ComoT $ \c -> c extract m
      -- definition of join:
    === ComoT $ \c' -> runComoT (ComoT $ \c -> c extract m) $ \wr_b1 m' -> runComoT m' $ \wb1_b2 -> c' (wr_b1 =>= wb1_b2)
      -- runComoT . ComoT === id
    === ComoT $ \c' -> (\c -> c extract m) $ \wr_b1 m' -> runComoT m' $ \wb1_b2 -> c' (wr_b1 =>= wb1_b2)
      -- apply c => (\wr_b1 m' -> ...)
    === ComoT $ \c' -> (\wr_b1 m' -> runComoT m' $ \wb1_b2 -> c' (wr_b1 =>= wb1_b2)) extract m
      -- apply wr_b1 => extract. apply m' => m
    === ComoT $ \c' -> runComoT m $ \wb1_b2 -> c' (extract =>= wb1_b2)
      -- (extract =>=) === id
    === ComoT $ \c' -> runComoT m $ \wb1_b2 -> c' wb1_b2
      -- eta reduction
    === ComoT $ \c' -> runComoT m c'
      -- eta reduction
    === ComoT $ runComoT m
      -- ComoT . runComoT === id
    === m

join . fmap pure === id
  join (fmap pure m)
      -- definition of fmap
    === join $ ComoT $ \c -> runComoT m $ \wr_b -> c wr_b . pure
      -- definition of join
    === ComoT $ \c' -> runComoT (ComoT $ \c -> runComoT m $ \wr_b -> c wr_b . pure) $ \wr_b1 m' -> runComoT m' $ \wb1_b2 -> c' (wr_b1 =>= wb1_b2)
      -- runComoT . ComoT === id
    === ComoT $ \c' -> (\c -> runComoT m $ \wr_b -> c wr_b . pure) $ \wr_b1 m' -> runComoT m' $ \wb1_b2 -> c' (wr_b1 =>= wb1_b2)
      -- apply c => (\wr_b1 m' -> ...)
    === ComoT $ \c' -> runComoT m $ \wr_b -> (\wr_b1 m' -> runComoT m' $ \wb1_b2 -> c' (wr_b1 =>= wb1_b2)) wr_b . pure
      -- eta abstraction
    === ComoT $ \c' -> runComoT m $ \wr_b a -> (\wr_b1 m' -> runComoT m' $ \wb1_b2 -> c' (wr_b1 =>= wb1_b2)) wr_b (pure a)
      -- apply wr_b1 => wr_b. apply m' => (pure a)
    === ComoT $ \c' -> runComoT m $ \wr_b a -> runComoT (pure a) $ \wb1_b2 -> c' (wr_b =>= wb1_b2)
      -- definition of pure
    === ComoT $ \c' -> runComoT m $ \wr_b a -> runComoT (ComoT $ \c'' -> c'' extract a) $ \wb1_b2 -> c' (wr_b =>= wb1_b2)
      -- runComoT . ComoT === id
    === ComoT $ \c' -> runComoT m $ \wr_b a -> (\c'' -> c'' extract a) $ \wb1_b2 -> c' (wr_b =>= wb1_b2)
      -- apply c'' => (\wb1_b2 -> ...)
    === ComoT $ \c' -> runComoT m $ \wr_b a -> (\wb1_b2 -> c' (wr_b =>= wb1_b2)) extract a
      -- apply wb1_b2 => extract
    === ComoT $ \c' -> runComoT m $ \wr_b a -> c' (wr_b =>= extract) a
      -- (=>= extract) === id
    === ComoT $ \c' -> runComoT m $ \wr_b a -> c' wr_b a
      -- eta reduction
    === ComoT $ \c' -> runComoT m c'
      -- eta reduction
    === ComoT $ runComoT m
      -- ComoT . runComoT === id
    === m

join . join === join . fmap join

  join (join m)
      -- definition of join
    === ComoT $ \c -> runComoT (join m) $ \wr_b1 m' -> runComoT m' $ \wb1_b2 -> c (wr_b1 =>= wb1_b2)
      -- definition of join
    === ComoT $ \c -> runComoT (ComoT $ \c' -> runComoT m $ \wr_b1' m'' -> runComoT m'' $ \wb1_b2' -> c' (wr_b1' =>= wb1_b2')) $ \wr_b1 m' -> ...
      -- runComoT . ComoT === id
    === ComoT $ \c -> (\c' -> runComoT m $ \wr_b1' m'' -> runComoT m'' $ \wb1_b2' -> c' (wr_b1' =>= wb1_b2')) $ \wr_b1 m' -> ...
      -- apply c' => (\wr_b1 m' -> ...)
    === ComoT $ \c -> runComoT m $ \wr_b1' m'' -> runComoT m'' $ \wb1_b2' -> (\wr_b1 m' -> ...) (wr_b1' =>= wb1_b2')
      -- apply wr_b1 => (wr_b1' =>= wb1_b2')
    === ComoT $ \c -> runComoT m $ \wr_b1' m'' -> runComoT m'' $ \wb1_b2' -> (\m' -> runComoT m' $ \wb1_b2 -> c ((wr_b1' =>= wb1_b2') =>= wb1_b2))
      -- combine lambdas
    === ComoT $ \c -> runComoT m $ \wr_b1' m'' -> runComoT m'' $ \wb1_b2' m' -> runComoT m' $ \wb1_b2 -> c ((wr_b1' =>= wb1_b2') =>= wb1_b2)
      -- ((a =>= b) =>= c) === (a =>= (b =>= c))
    === ComoT $ \c -> runComoT m $ \wr_b1' m'' -> runComoT m'' $ \wb1_b2' m' -> runComoT m' $ \wb1_b2 -> c (wr_b1' =>= wb1_b2' =>= wb1_b2)
      -- rename wr_b1' to wr_b1. m'' to m'. m' to m''. wb1_b2' to wb1_b2. wb1_b2 to wb2_b3
    === ComoT $ \c -> runComoT m $ \wr_b1 m' -> runComoT m' $ \wb1_b2 m'' -> runComoT m'' $ \wb2_b3 -> c (wr_b1 =>= wb1_b2 =>= wb2_b3)

  join (fmap join m)
      -- definition of join
    === ComoT $ \c -> runComoT (fmap join m) $ \wr_b1 m' -> runComoT m' $ \wb1_b2 -> c (wr_b1 =>= wb1_b2)
      -- definition of fmap
    === ComoT $ \c -> runComoT (ComoT $ \c' -> runComoT m $ \wr_b -> c' wr_b . join) $ \wr_b1 m' -> ...
      -- runComoT . ComoT === id
    === ComoT $ \c -> (\c' -> runComoT m $ \wr_b -> c' wr_b . join) $ \wr_b1 m' -> ...
      -- apply c' => (\wr_b1 m' -> ...)
    === ComoT $ \c -> runComoT m $ \wr_b -> (\wr_b1 m' -> ...) wr_b . join
      -- apply wr_b1 => wr_b
    === ComoT $ \c -> runComoT m $ \wr_b -> (\m' -> runComoT m' $ \wb1_b2 -> c (wr_b =>= wb1_b2)) . join
      -- eta abstraction
    === ComoT $ \c -> runComoT m $ \wr_b m'' -> (\m' -> runComoT m' $ \wb1_b2 -> c (wr_b =>= wb1_b2)) (join m'')
      -- apply m' => (join m'')
    === ComoT $ \c -> runComoT m $ \wr_b m'' -> runComoT (join m'') $ \wb1_b2 -> c (wr_b =>= wb1_b2)
      -- definition of join
    === ComoT $ \c -> runComoT m $ \wr_b m'' -> runComoT (ComoT $ \c' -> runComoT m'' $ \wr_b1' m''' -> runComoT m''' $ \wb1_b2' -> c' (wr_b1' =>= wb1_b2')) $ \wb1_b2 -> c (wr_b =>= wb1_b2)
      -- runComoT . ComoT === id
    === ComoT $ \c -> runComoT m $ \wr_b m'' -> (\c' -> runComoT m'' $ \wr_b1' m''' -> runComoT m''' $ \wb1_b2' -> c' (wr_b1' =>= wb1_b2')) $ \wb1_b2 -> c (wr_b =>= wb1_b2)
      -- apply c' => (\wb1_b2 -> ...)
    === ComoT $ \c -> runComoT m $ \wr_b m'' -> runComoT m'' $ \wr_b1' m''' -> runComoT m''' $ \wb1_b2' -> (\wb1_b2 -> c (wr_b =>= wb1_b2)) (wr_b1' =>= wb1_b2')
      -- apply wb1_b2 => (wr_b1' =>= wb1_b2')
    === ComoT $ \c -> runComoT m $ \wr_b m'' -> runComoT m'' $ \wr_b1' m''' -> runComoT m''' $ \wb1_b2' -> c (wr_b =>= (wr_b1' =>= wb1_b2'))
      -- (a =>= (b =>= c)) === ((a =>= b) =>= c)
    === ComoT $ \c -> runComoT m $ \wr_b m'' -> runComoT m'' $ \wr_b1' m''' -> runComoT m''' $ \wb1_b2' -> c (wr_b =>= wr_b1' =>= wb1_b2')
      -- rename wr_b to wr_b1. m'' to m'. wr_b1' to wb1_b2. m''' to m''. wb1_b2' to wb2_b3
    === ComoT $ \c -> runComoT m $ \wr_b1 m' -> runComoT m' $ \wb1_b2 m'' -> runComoT m'' $ \wb2_b3 -> c (wr_b1 =>= wb1_b2 =>= wb2_b3)

-}