Last active
November 15, 2018 20:42
-
-
Save KingoftheHomeless/9faf31de808ab36ccafd4c714013969d to your computer and use it in GitHub Desktop.
The dual to Mo. A new comonad-to-monad 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 #-} | |
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) | |
-} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment