Last active
November 15, 2018 20:42
-
-
Save KingoftheHomeless/97238d205a3b19f3185660111bfacf8e to your computer and use it in GitHub Desktop.
The monad-to-comonad transformer
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 | |
-} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment