Too lazy to evaluate - ストリング図でMonad再入門(2)

前回、ストリング図について紹介しました。例として、ストリング図を使ってモナド則を視覚的に表して、 Stateモナドのモナド則をストリング図の変形で証明しています。

しかし、Stateモナドのような単純なケースでは、ストリング図のありがたみがまだわからないかもしれません。

今回は、StateTモナド変換子（Control.Monad.Trans.State.Lazyを参照）のモナド則を、ストリング図で示してみます。

（あと、ちょっときれいな図を描けるようになりました。）

ストリング図で`StateT`

前回の記事で使ったStateモナドの定義を再掲します。（証明を楽にするために、Monadクラスの定義もHaskell標準のものからちょっと変えています。）

type G s = (->) s -- (s ->) と書きたいが、Haskellはこの書き方は不可
type F s = (,) s  -- (s, )  〃

newtype State s a = State { runState :: G s (F s a) }
  -- State s a ~ Compose (G s) (F s) a

instance Monad (State s) where
  pure = open >>> State
  join =   runState              -- :: State s (State s a) -> G s (F s (State s a))
       >>> fmap (fmap runState)  -- :: G s (F s (State s a)) -> G s (F s (G s (F s a)))
       >>> fmap close            -- :: G s (F s (G s (F s a))) -> G s (F s a)
       >>> State                 -- :: G s (F s a) -> State s a

open :: a -> G s (F s a)   -- a -> (s -> (s, a))
open a = \s -> (s, a)

close :: F s (G s a) -> a  -- (s, s -> a) -> a
close (s, f) = f s

この流儀に沿って、StateTを定義し直してみます。嬉しいことに、Stateモナドの定義からopenとcloseを流用できます。

newtype StateT s m a = State { runState :: G s (m (F s a)) }
  -- StateT s m a ~ (G s `Compose` m `Compose` F s) a
  --              ~ s -> m (s, a)

instance Monad m => Monad (StateT s m) where
  pure =   open       -- a -> G s (F s a)
       >>> fmap pure  -- G s (F s a) -> G s (m (F s a))
       >>> StateT     -- G s (m (F s a)) -> StateT s m a
  
  join =   fmap runState     -- :: StateT s m (StateT s m a) -> StateT s m (G s (m (F s a)))
       >>> runState          -- :: StateT s m (G s (m (F s a))) -> G s (m (F s (G s (m (F s a)))))
       >>> fmap (fmap close) -- :: G s (m (m (F s a)))
       >>> fmap join         -- :: G s (m (F s a))
       >>> StateT            -- :: G s (m (F s a)) -> StateT s m a