🏹

随伴を使って理解するStateモナドの実装

2020/09/21に公開

Haskell

圏論

math

tech

前回の記事は魔法のように見えるStateモナドの実装も、順を追って見ていけば理解することは難しくないという話でした。

しかし状態の変更を順番に処理するというような手続き的な考え方にかなり近い構造が、うまくモナドになってくれるというのは少し不思議ですよね。

この記事では

タプル (a, b)
関数 a -> b
カリー化 curry :: ((a, b) -> c) -> a -> b -> c
uncurry :: (a -> b -> c) -> (a, b) -> c

といったHaskellの基本的な要素が随伴と呼ばれる関係を構成することを見て、
その随伴からStateモナドが導かれることを説明していきたいと思います。

随伴

二つの圏 $C, D$ と二つの関手 $F : C \rightarrow D, G : D \rightarrow C$ が与えられたとしましょう。

もし $GF = {\rm 1}_C, FG = {\rm 1}_D$ であれば $C$ と $D$ は圏同型であると言います。これは圏の圏 ${\rm Cats}$ において $C$ と $D$ が同型であることを示しており、二つの圏 $C, D$ を"同じ"とみなすとても強い関係です。

今、 $F, G$ は関手であるので、自然変換を使ってもう少しゆるい同値関係を考えることもできます。 $GF \cong {\rm 1}_C, FG \cong {\rm 1}_D$ というように恒等関手と厳密に一致する必要はなく自然同型が存在すると仮定した場合、 $C$ と $D$ は圏同値であると言います。圏同値は、例えば圏 $C$ の対象 $c$ を $GF$ で写した対象 $GFc$ が元の対象 $c$ と一致する必要はなく同型であれば良いということ言っており、圏同型よりゆるい同値関係を表しています。

さらに自然同型であるという仮定も弱めて、二つの自然変換 $\eta: {\rm 1}_C \rightarrow GF, \epsilon: FG \rightarrow {\rm 1}_D$ が存在して必要な公理を満たすと仮定した場合、随伴と呼ばれる関係が定まります。満たすべき公理は $F, G, \eta, \epsilon$ が以下の図式を可換にすることです（これらは三角等式と呼ばれます）。

これらの関係を満たす時、 $F$ は $G$ の左随伴、 $G$ は $F$ の右随伴と呼ばれ

F \dashv G

と表します。随伴を構成する２つの自然変換 $\eta, \epsilon$ はそれぞれ単位(unit), 余単位(counit)と呼びます。

そろそろ抽象的な話にも疲れてきたので、ここで随伴をHaskellで実装することにしましょう。２つの関手（Functor）が随伴（Adjunction）の関係にあることは自然変換（unit, counit）の存在によって定まるので、これを型クラスを使って表現しましょう。

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}

class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where
  unit :: a -> g (f a)
  counit :: f (g a) -> a

自然変換は多相関数を使って表現しています。この実装では恒等関手Identityが明示的に現れていないことにも注意して下さい。同様の実装はHaskellのライブラリadjunctionsにも見ることができます。

ところで随伴にはもう一つ同値な定義があります。2つの（局所小）圏 $C, D$ の間の随伴とは2つの関手 $F: C \rightarrow D, G: D \rightarrow C$ が存在して、これらが定める $C^{op}\times D$ から ${\rm Sets}$ への2つの関手が以下のように自然同型であるものを言います。

{\rm Hom}_D\left(F-, -\right) \cong {\rm Hom}_C\left(-, G-\right)

この定義が前述の自然変換 $\epsilon, \eta$ を導くことを見てみましょう^[1]。圏 $C$ の各対象 $c$ を使って自然同型に $c$ と $Fc$ を代入すれば

{\rm Hom}_D\left(Fc, Fc\right) \cong {\rm Hom}_C\left(c, GFc\right)

という同型が存在することが分かります。この同型により恒等射 ${\rm 1}_{Fc}$ に対応する射を $\eta_c: c \rightarrow GFc$ とおき、全ての対象について同様の射を考えると自然変換 $\eta: {\rm 1}_C \rightarrow GF$ を定義することができます。実際に $\eta$ が自然変換であることは前提となっている自然同型を注意深く追えば分かります。同様に圏 $D$ の各対象 $d$ について

{\rm Hom}_D\left(FGd, d\right) \cong {\rm Hom}_C\left(Gd, Gd\right)

という同型を考えて恒等射 ${\rm 1}_{Gd}$ に対応する射を考えることで、自然変換 $\epsilon: FG \rightarrow {\rm 1}_D$ を定義することができます。

このように定めた $\eta, \epsilon$ が三角等式を満たすことを確認しましょう。

1つ目の三角等式

{\rm 1}_F = \epsilon F \circ F\eta

を示すために圏 $C$ の各対象 $c$ について以下の図式を考えます。

この図式は自然同型であることより可換になります。

左上の ${\rm Hom}_C(GFc, GFc)$ に属する射 ${\rm 1}_{GFc}$ を、まず左下を経由して右下に移すと

{\rm 1}_{GFc} \mapsto {\rm 1}_{GFc} \circ \eta_c = \eta_c \mapsto {\rm 1}_{Fc}

となり、反対に右上を経由して右下に移すと

{\rm 1}_{GFc} \mapsto \epsilon_{Fc} \mapsto \epsilon_{Fc} \circ F\eta_c

となり図式が可換であることより

{\rm 1}_{Fc} = \epsilon_{Fc} \circ F\eta_c

が分かります。これは任意の対象について成り立つので1つ目の三角等式が成り立つことが分かりました。2つ目の三角等式も同様に示すことができます。

さて、ここからはHaskellの実装に戻りましょう。随伴の別の定義を知ったのでAdjunctionの実装に反映してみましょう。

class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where
  unit :: a -> g (f a)
  counit :: f (g a) -> a

  leftAdjunct :: (f a -> b) -> a -> g b
  rightAdjunct :: (a -> g b) -> f a -> b

  unit = leftAdjunct id
  counit = rightAdjunct id

leftAdjunctとrightAdjunctは自然同型における全単射を表しています。これらに恒等射idを与えて評価することでunit, counitが出てくるのは上述した証明の流れと対応していてとても綺麗ですね！

随伴から導かれるモナド

実は随伴関手が与えられると、そこからモナドを構成することができます。
まずはモナドの定義を思い出しておきましょう。

圏 $C$ と自己関手 $T: C \rightarrow C$ があり、さらに以下の図式を可換にする自然変換 $\eta: {\rm 1}_C \rightarrow T, \mu: T^2 \rightarrow T$ が存在する時 $T, \eta, \mu$ の組をモナドと呼びます。

結論から言えば随伴関手 $F\dashv G$ が与えられたときに圏 $C$ 上の自己関手 $GF$ を考えると、これがモナドになります。自然変換 $\eta$ は随伴のcounit（つまり $\eta$ ）であり、 $\mu$ は

\mu = G\epsilon F

と定めます。

これらがちゃんとモナドになっていることを確認してみましょう。

まず1つ目の可換図式は

\begin{matrix} && \mu \circ T\mu &=& \mu \circ \mu T \\ &\Leftrightarrow& G\epsilon F \circ GFG\epsilon F &=& G\epsilon F \circ G\epsilon FGF \\ \end{matrix}

となりますが $\epsilon$ が $FG$ から $1_D$ への自然変換であるので圏 $C$ の各対象 $a$ について以下の図式が可換となり

この可換図式を $G$ で写せば等式が成り立つことが分かります。

また2つ目の可換図式は

となり、随伴の三角等式を関手 $F$ , $G$ でうまく写したものに対応していて、成立することが分かります。

それでは随伴からモナドを構成する方法をHaskellで実装していきましょう。

HaskellでFunctorを合成する方法はData.Functor.Composeで提供されていますが、インスタンス定義が重複してエラーになってしまうので今回は自分で作ります。

newtype (.) g f a = Compose { getCompose :: g (f a) }

. をFunctorの合成を表すType Operatorとして使うことでFunctor gとfの合成を g . fと分かりやすく書くことができます^[2]。

HaskellでMonadのインスタンスを作るためにはFunctorとApplicativeのインスタンスにする必要があります。

まずFunctorの実装は簡単です。

instance (Functor f, Functor g) => Functor (g . f) where
  fmap f (Compose gf) = Compose $ fmap (fmap f) gf

次にApplicativeの実装ですが、その前にモナドであることを先取りして自然変換 $\mu$ に対応する関数joinを定義しておきましょう。

join :: Adjunction f g => g (f (g (f a))) -> g (f a)
join = fmap counit

join' :: Adjunction f g => (g . f) ((g . f) a) -> (g . f) a
join' (Compose gfgf) = Compose . join $ fmap (fmap getCompose) gfgf

join' は実装の詳細を吸収して複雑になってますが、実態はjoinです。これはcounit、すなわち $\epsilon$ を $G$ についてfmapする実装になっており、圏論で随伴からモナドを導くときの構成と同じになっていることが分かります。

これを使えばApplicativeは以下のように実装できます。

instance Adjunction f g => Applicative (g . f) where
  pure = Compose . unit
  f <*> k = join' $ fmap (\a -> fmap ($ a) f) k

pure、つまりモナドにおける自然変換 $\eta$ も随伴における $\eta$ つまりunitがそのまま対応しています。

最後にMonadのインスタンスを実装しましょう。

instance Adjunction f g => Monad (g . f) where
  f >>= m = join' $ fmap m f

これで完成です！

随伴Adjunctionであることを利用してモナドMonadの実装を行うことができました👏

Stateモナド

さて、いよいよ本題であるStateモナドの実装を見ていきましょう。
そのためにもちろん随伴になっている関手を使います。

実は圏論ではよく知られた積とべき対象の随伴から導かれるモナドがStateモナドに対応しています。Haskellの言葉で言えばタプル(a, b)と関数a -> bです。WriterとReaderと言っても良いでしょう。

そしてこれらの随伴を定めるleftAdjunctとrightAdjunctがカリー化とその逆に対応しているのです。

実際に実装を見てみましょう。

curry' :: ((b, a) -> c) -> a -> b -> c
curry' f a b = f (b, a)

uncurry' :: (a -> b -> c) -> (b, a) -> c
uncurry' f (b, a) = f a b

instance Adjunction ((,) b) ((->) b) where
  leftAdjunct = curry'
  rightAdjunct = uncurry'

Haskellではタプルの右側だけ型を適応した型を手軽に作れないので、引数の順番が少し違うcurryやuncurryを再実装していますが本質は変わりません^[3]。

ところでもうStateモナドの実装が終わっていることにお気づきでしょうか？
随伴関手が定まればモナドは自動的に手に入るので、

type State s = ((->) s) . ((,) s)

これで終わりです！

前回定義したStateモナドの型が

newtype State s a = State { runState :: s -> (s, a) }

であったことを思い出すと確かに対応していますね。

もちろんgetやsetを定義して普通のStateモナドのように使うことも可能です。

最後に等式論証を使って随伴を使ったモナドの実装が手続き的な実装と対応していることを確認して終わりましょう。少し長いですが丁寧に展開していきます。

f >>= m = join' $ fmap m f

<=> {- join' を展開 -}

f >>= m = (\(Compose gfgf) -> Compose . join $ fmap (fmap getCompose) gfgf) $ fmap m f

<=> {- ラムダ式を適用 -}

f >>= m = Compose . join $ fmap (fmap getCompose) (getCompose $ fmap m f)

<=> {- f = Compose $ \s -> getCompose f s -}

f >>= m = Compose . join $ fmap (fmap getCompose)
  (getCompose $ fmap m (Compose $ \s -> getCompose f s))

<=> {- getCompose f s = let (s', a) = getCompose f s in (s', a) -}

f >>= m = Compose . join $ fmap (fmap getCompose)
  (getCompose $ fmap m (Compose $ \s -> let (s', a) = getCompose f s in (s', a)))

<=> {- fmap m を評価 -}

f >>= m = Compose . join $ fmap (fmap getCompose)
  (getCompose $ (Compose $ \s -> let (s', a) = getCompose f s in (s', m a)))

<=> {- getCompose . Compose = id -}

f >>= m = Compose . join $ fmap (fmap getCompose)
  (\s -> let (s', a) = getCompose f s in (s', m a))

<=> {- join = fmap counit = fmap (rightAdjunct id) = fmap (uncurry' id) = fmap (\(b, f) -> f b) -}

f >>= m = Compose . fmap (\(b, f) -> f b) $ fmap (fmap getCompose)
  (\s -> let (s', a) = getCompose f s in (s', m a))

<=> {- fmap 融合則 -}

f >>= m = Compose $ fmap ((\(b, f) -> f b) . (fmap getCompose))
  (\s -> let (s', a) = getCompose f s in (s', m a))

<=> {- fmap 適用 -}

f >>= m = Compose $ \s ->
  let (s', a) = getCompose f s
  in (\(b, f) -> f b) . (fmap getCompose) $ (s', m a)

<=> {- inの中を評価 -}

f >>= m = Compose $ \s ->
  let (s', a) = getCompose f s
  in getCompose (m a) s'

前回のモナドの実装と比較してみると見事に対応していることが分かりますね👏

instance Monad (State s) where
  f >>= m = State $ \s ->
    let (s', a) = runState f s
     in runState (m a) s'

あとがき

随伴を使ってStateモナドが定義できることを確認し、手続き的な実装とちゃんと対応することを見てきました。随伴に纏わる面白い話はまだまだあるので更に知りたい人は以下のリンクからたどると良いでしょう。

From Adjunctions to Monads 随伴からモナドの導出をストリング図など交えて解説されています
随伴がモテないのはどう考えてもモナドが悪い！（モナドとコモナドの関係が分かる話）実は随伴関手を反対向きに組み合わせるとコモナドを導出することができます。Stateモナドの反対はStoreコモナド
Haskellと随伴タプルと関数以外にも興味深い随伴が紹介されています

＼読んでいただきありがとうございました！／
この記事が面白かったらいいね♡ をいただけると嬉しいです☺️
バッジを贈っていただければ次の記事を書くため励みになります🙌

脚注

定義が同値であることを見るには反対向きの証明も必要ですが、長くなるので気になる人はWikipediaを参照して下さい（4.2 余単位-単位随伴がhom集合随伴を導くこと）。 ↩︎
. がType Operatorとして使えるようになったのはGHC8.8.1からのようです（Haskell-jpもくもく会で教えてもらいました） ↩︎
前回の記事でもStateモナドの型がtransformersとズレたのはこれが原因です😅 ↩︎

随伴

随伴から導かれるモナド

Stateモナド

あとがき

Discussion