The monad-to-comonad transformer

Mo.hs

{-# LANGUAGE RankNTypes, GADTs #-}
module Mo where

import Control.Comonad
import Control.Comonad.Trans.Class
import Control.Monad
{-
    The monad-to-comonad transformer.
    Originally, Mo was defined as the simpler (and isomorphic):
        data Mo m w a where
            Mo :: (w (m r) -> a) -> w r -> Mo m w a

    The current version modifies this by lifting "w (m r)" to its Coyoneda variant,
    which prevents a "Functor w" constraint on Mo's Comonad instance, as well as making the methods themselves be more efficient.
    I've also managed to sketch out a solid proof that Mo is a comonad for Coyoneda version. For the "simplified" variant above,
    I was only able to do so by assuming a sketchy, non-obvious law.

    Credit goes to /u/davidfeuer on Reddit for creating the Coyoneda variant of Mo:
    https://www.reddit.com/r/haskell/comments/8enipw/a_possible_monadtocomonad_transformer/dxz80ll/
-}
-- Mo becomes a lot more interesting when you don't have w ~ Identity,
-- because (Mo m Identity a) is just isomorphic to (m () -> a)
-- This is why Mo isn't called MoT, and a type synonym "Mo m = MoT m Identity" doesn't exist.
data Mo m w a where
    Mo :: (forall b. (b -> m r) -> w b -> a) -> w r -> Mo m w a

-- A simpler way to create a mo. Makes use of the original definition.
mo' :: Functor w => (w (m r) -> a) -> w r -> Mo m w a
mo' ext = Mo ((ext .) . fmap)

-- These instances for the Coyoneda version of Mo were defined by /u/davidfeuer. Props to him!
instance Functor (Mo m w) where
  fmap f (Mo ext wr) = Mo ((f .) . ext) wr

instance Monad m => Comonad (Mo m w) where
  extract (Mo ext wr) = ext pure wr
  duplicate (Mo ext wr) = Mo (\bmr -> Mo (\q -> ext (q >=> bmr))) wr
  extend f (Mo ext wr) = Mo (\bmr -> f . Mo (\q -> ext (q >=> bmr))) wr

instance Applicative m => ComonadTrans (Mo m) where
  lower (Mo ext wr) = extend (ext pure) wr

{-

Proof that (Mo m w) is a Comonad.

  extract . duplicate === id

    extract (duplicate (Mo ext wr)) === extract $ Mo (\bmr -> Mo (\q -> ext (q >=> bmr))) wr
        -- definition of extract
      === (\bmr -> Mo (\q -> ext (q >=> bmr))) pure wr
        -- apply bmr => pure
      === Mo (\q -> ext (q >=> pure)) wr
        -- (>=> pure) === id
      === Mo (\q -> ext q) wr
        -- eta reduction
      === Mo ext wr

  fmap extract . duplicate === id

    fmap extract (duplicate (Mo ext wr)) === fmap extract $ Mo (\bmr -> Mo (\q -> ext (q >=> bmr))) wr
        -- definition of fmap
      === Mo (\bmr -> extract . Mo (\q -> ext (q >=> bmr))) wr
        -- eta abstraction
      === Mo (\bmr wb -> extract $ Mo (\q -> ext (q >=> bmr)) wb) wr
        -- definition of extract
      === Mo (\bmr wb -> (\q -> ext (q >=> bmr)) pure wb) wr
        -- apply q => pure
      === Mo (\bmr wb -> ext (pure >=> bmr) wb) wr
        -- (pure >=>) === id
      === Mo (\bmr wb -> ext bmr wb) wr
        -- eta reduction
      === Mo ext wr


  duplicate . duplicate === fmap duplicate . duplicate

    duplicate (duplicate (Mo ext wr)) === duplicate $ Mo (\bmr -> Mo (\q -> ext (q >=> bmr))) wr
        -- definition of duplicate.
      === Mo (\bmr' -> Mo (\q' -> (\bmr -> Mo (\q -> ext (q >=> bmr))) (q' >=> bmr'))) wr
        -- apply bmr => (q' >=> bmr')
      === Mo (\bmr' -> Mo (\q' -> Mo (\q -> ext (q >=> (q' >=> bmr'))))) wr
        -- a >=> (b >=> c) === (a >=> b) >=> c
      === Mo (\bmr' -> Mo (\q' -> Mo (\q -> ext (q >=> q' >=> bmr')))) wr
        -- rename bmr' to bmr
      === Mo (\bmr -> Mo (\q' -> Mo (\q -> ext (q >=> q' >=> bmr)))) wr

    fmap duplicate (duplicate (Mo ext wr)) === fmap duplicate $ Mo (\bmr -> Mo (\q -> ext (q >=> bmr))) wr
        -- definition of fmap
      === Mo (\bmr -> duplicate . Mo (\q -> ext (q >=> bmr))) wr
        -- eta abstraction
      === Mo (\bmr wb -> duplicate $ Mo (\q -> ext (q >=> bmr)) wb) wr
        -- definition of duplicate
      === Mo (\bmr wb -> Mo (\bmr' -> Mo (\q' -> (\q -> ext (q >=> bmr)) (q' >=> bmr'))) wb) wr
        -- apply q => (q' >=> bmr')
      === Mo (\bmr wb -> Mo (\bmr' -> Mo (\q' -> ext ((q' >=> bmr') >=> bmr))) wb) wr
        -- (a >=> b) >=> c === a >=> (b >=> c)
      === Mo (\bmr wb -> Mo (\bmr' -> Mo (\q' -> ext (q' >=> bmr' >=> bmr))) wb) wr
        -- eta reduction
      === Mo (\bmr -> Mo (\bmr' -> Mo (\q' -> ext (q' >=> bmr' >=> bmr)))) wr
       -- rename q' to q. rename bmr' to q'.
      === Mo (\bmr -> Mo (\q' -> Mo (\q -> ext (q >=> q' >=> bmr)))) wr

-}

-- This doesn't really need to exist. It's equivalent to (fmap (join . extract) . liftMo')
liftMo :: (Monad m, Comonad w) => w (m a) -> Mo m w (m a)
liftMo = Mo (\q -> join . q . extract)

-- More general than liftMo.
liftMo' :: Functor w => w a -> Mo m w (w (m a))
liftMo' = Mo fmap

runMo :: Mo m w a -> (forall r. w r -> w (m r)) -> a
runMo (Mo ext wr) f = ext id (f wr)

study' :: Mo m w a -> (forall r. w r -> b) -> b
study' (Mo _ wr) f = f wr

study :: Functor w => Mo m w a -> w ()
study = (`study'` void)

-- I'm honestly not sure if there's any difference between these two in practice.
(<|) :: Monad m => (forall r. w r -> w (m r)) -> Mo m w a -> Mo m w a
m <| mo = extend (`runMo` m) mo

(|>) :: Monad m => Mo m w a -> (forall r. w r -> w (m r)) -> Mo m w a
mo |> m = runMo (duplicate mo) m

appendLine :: (String -> r) -> String -> IO r
appendLine f s = do
    toAppend <- getLine
    return $ f (s ++ toAppend)

{-
putStrLn    :: String -> IO ()
            :: ((->) String) (IO ())
liftMo putStrLn :: Mo IO ((->) String) (IO ())
-}
example :: IO ()
example = extract $ liftMo putStrLn |> appendLine |> appendLine |> appendLine |> appendLine |> appendLine

{-
*Mo> example
ab
ra
ca
da
bra

abracadabra
-}