モナド変換子
Haskellにおいてモナド変換子(Monad transformer)は、以下の条件を満たすtです:
- tのkindは(* -> *) -> * -> *
- lift :: Monad m => m a -> t m aが定義されている
- liftが以下の法則を満たす:
- lift . return = return
- ∀m k. lift (m >>= k) = lift m >>= (lift . k)
(この定義を便宜上函数的定義(functional definition)と呼びます。)
この定義を圏論の言葉を使って書きなおすことを考えると、以下のようになります:
- tのkindは(* -> *) -> * -> *
- lift :: Monad m => m a -> t m aが定義されている
- liftが以下の法則を満たす:
(この定義を便宜上圏論的定義(categorical definition)と呼びます。)
この二つの定義が同値であることを示します。
函数的定義→圏論的定義
(1) lift . return = return
(2) ∀m k. lift (m >>= k) = lift m >>= (lift . k)
を仮定する。
(i) ∀(k :: a -> b). fmap k . lift = lift . fmap k
(2)においてk=return . fを代入すると
∀m f. lift (m >>= return . f) = lift m >>= (lift . return . f)
∀m f. lift (m >>= return . f) = lift m >>= (return . f) ((1)より)
fmap f m = m >>= return . fを利用すると
∀m f. lift (fmap f m) = fmap f (lift m)
∀f. lift . fmap f = fmap f . lift (mを消去)
(ii-i) lift . return = return
(1)から自明。
(ii-ii) lift . join = join . fmap lift . lift
(2)にk=idを代入すると
∀m. lift (m >>= id) = lift m >>= (lift . id)
m >>= id = join m, idは恒等射より
∀m. lift (join m) = lift m >>= lift
m >>= k = join (fmap k m)より
∀m. lift (join m) = join (fmap lift (lift m))
mを消去して
lift . join = join . fmap lift . lift
圏論的定義→函数的定義
読者の演習問題とする。(訳:疲れました)
追記(2014/06/25)要望があったので答えを載せます。(白い文字で書いているので選択すると読めます)
(i) ∀(k :: a -> b). fmap k . lift = lift . fmap k
(ii-i) lift . return = return
(ii-ii) lift . join = join . fmap lift . lift
を仮定する。
(1) lift . return = return
(i)から自明。
(2) ∀m k. lift (m >>= k) = lift m >>= (lift . k)
(以下白文字)
(i)の両辺に左からjoin . fmap liftを合成して
∀k. join . fmap lift . fmap k . lift = join . fmap lift . lift . fmap k
(ii-ii)を右辺に適用して
∀k. join . fmap lift . fmap k . lift = lift . join . fmap k
fmap (g . f) = fmap g . fmap fより
∀k. join . fmap (lift . k) . lift = lift . join . fmap k
両辺をmに適用して
∀m k. join (fmap (lift . k) (lift m)) = lift (join (fmap k m))
m >>= k = join (fmap k m)を利用して変形すると
∀m k. lift m >>= lift . k = lift (m >>= k)
