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

公開:2020/09/21
更新:2020/10/04
11 min読了の目安(約10000字TECH技術記事
Likes19

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

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

この記事では

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

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

この記事には圏論が使われているので、まだ履修していない方はご注意ください。

随伴

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

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

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

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

これらの関係を満たす時、FFGG左随伴GGFF右随伴と呼ばれ

FG F \dashv G

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

そろそろ抽象的な話にも疲れてきたので、ここで随伴をHaskellで実装することにしましょう。2つの関手(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,DC, Dの間の随伴とは2つの関手F:CD,G:DCF: C \rightarrow D, G: D \rightarrow Cが存在して、これらが定めるCop×DC^{op}\times DからSets{\rm Sets}への2つの関手が以下のように自然同型であるものを言います。

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

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

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

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

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

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

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

1つ目の三角等式

1F=ϵFFη {\rm 1}_F = \epsilon F \circ F\eta

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

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

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

1GFc1GFcηc=ηc1Fc {\rm 1}_{GFc} \mapsto {\rm 1}_{GFc} \circ \eta_c = \eta_c \mapsto {\rm 1}_{Fc}

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

1GFcϵFcϵFcFηc {\rm 1}_{GFc} \mapsto \epsilon_{Fc} \mapsto \epsilon_{Fc} \circ F\eta_c

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

1Fc=ϵFcFη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

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

随伴から導かれるモナド

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

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

結論から言えば随伴関手 FGF\dashv G が与えられたときに圏CC上の自己関手GFGFを考えると、これがモナドになります。自然変換η\etaは随伴のcounit(つまりη\eta)であり、μ\mu

μ=GϵF \mu = G\epsilon F

と定めます。

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

まず1つ目の可換図式は

μTμ=μμTGϵFGFGϵF=GϵFGϵFGF \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}

となりますがϵ\epsilonFGFGから1D1_Dへの自然変換であるので圏CCの各対象aaについて以下の図式が可換となり

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

また2つ目の可換図式は

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

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

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

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

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

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

まず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、すなわちϵ\epsilonGGについて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です。WriterReaderと言っても良いでしょう。

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

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

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ではタプルの右側だけ型を適応した型を手軽に作れないので、引数の順番が少し違うcurryuncurryを再実装していますが本質は変わりません[3]

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

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

これで終わりです!

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

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

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

もちろんgetsetを定義して普通の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モナドが定義できることを確認し、手続き的な実装とちゃんと対応することを見てきました。随伴に纏わる面白い話はまだまだあるので更に知りたい人は以下のリンクからたどると良いでしょう。


\読んでいただきありがとうございました!/
この記事が面白かったら いいね♡ をいただけると嬉しいです☺️
100円からでも サポート¥ をいただければ次の記事を書くため励みになります🙌

脚注
  1. 定義が同値であることを見るには反対向きの証明も必要ですが、長くなるので気になる人はWikipediaを参照して下さい(4.2 余単位-単位随伴がhom集合随伴を導くこと)。 ↩︎

  2. . がType Operatorとして使えるようになったのはGHC8.8.1からのようです(Haskell-jpもくもく会で教えてもらいました↩︎

  3. 前回の記事でもStateモナドの型がtransformersとズレたのはこれが原因です😅 ↩︎