読者です 読者をやめる 読者になる 読者になる

モナド変換子の圏論的理解(Categorical understanding of monad transformers)

モナド変換子

Haskellにおいてモナド変換子(Monad transformer)は、以下の条件を満たすtです:

  • tのkindは(* -> *) -> * -> *
  • lift :: Monad m => m a -> t m aが定義されている
  • liftが以下の法則を満たす:
    1. lift . return = return
    2. m k. lift (m >>= k) = lift m >>= (lift . k)

(この定義を便宜上函数的定義(functional definition)と呼びます。)
この定義を圏論の言葉を使って書きなおすことを考えると、以下のようになります:

  • tのkindは(* -> *) -> * -> *
  • lift :: Monad m => m a -> t m aが定義されている
  • liftが以下の法則を満たす:
    1. liftはmからt mへの自然変換(natural transformation)になっている。つまり、
      • ∀(k :: a -> b). fmap k . lift = lift . fmap k
    2. liftはEndofunctorの圏におけるモノイド対象の準同型である。つまり、以下が成立する:
      • lift . return = return (単位元を保つ)
      • lift . join = join . fmap lift . 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)