米田の補題とオペレーショナル・モナド

１．復習：米田の補題

米田の補題をHaskellで記述する方法については、Haskellの真髄に迫る-一般化代数的データで論じた。

米田の補題は次のように定義されていた。
\({\mathcal C}\)を圏とした時、任意の\({\mathcal C}\)の対象\(A\)と関手\(F: {\mathcal C} \rightarrow {\bf Sets}\)に対して
\({\rm Nat}({\rm Hom_{\mathcal C}}(A,-),F) \cong F(A)\)
である。この時、可換図式は次の通りである。

この補題は、

(forall x . (a -> x) -> f x)) ~ f a

をHaskellでの記述で表せばよい。前の記事では、Newtypeで表したが、代数的データ型を用いて表すと次のようになる。

data Yoneda f x where
  Yoneda :: (a -> x) -> f x -> Yoneda f a

２．双対

米田の補題(covariant)には双対の補題(contravariant)がある。それは、\({\mathcal C}\)の射をすべて逆向きにした\({\mathcal C}^{op}\)である。この時、米田の双対の補題は次のように定義される。
\({\mathcal C}\)を圏とした時、任意の\({\mathcal C}\)の対象\(A\)と関手\(F: {\mathcal C^{op}} \rightarrow {\bf Sets}\)に対して
\({\rm Nat}({\rm Hom_{\mathcal C}}(-,A),F) \cong F(A)\)
である。この時、可換図式は次の通りである。

オペレーショナル・モナドは双対の補題を用いて実現される。そこで、ここでは、米田の双対の補題とオペレーショナルモナドが結びつくようにする。

双対の補題は矢印の方向をすべて逆にすればよいので、次のものをHaskellで表せばよい。

(forall x . (x -> a) -> f x ~ f a

これを代数的データ型で表すこととする。(なお、米田の定理を実装したEdward Kmettが補題と双対の補題をYonedaとCoyonedaとそれぞれ名づけているので、ここではそれを用いる。統一されているわけではなく、異なる名前が用いられている場合もある。)

ここで、次のようにCoyonedaを型として定義する（前の記事は、newtypeを用いた）。

data Coyoneda f a where
  Coyoneda :: (b -> a) -> f b -> Coyoneda f a

また、証明の時に得られる式を\(\phi(\vartheta)=\vartheta_A(1_A)\)と\(\psi(u)_X(f)=F(f)(u)\)を用いると次が得られる（前の記事では、liftCoyonedaをfw:\(\phi\)で、lowerCoyonedaをbw:\(\psi\)で表した）。

liftCoyoneda :: f a -> Coyoneda f a 
liftCoyoneda = Coyoneda id
lowerCoyoneda :: Functor f =>Coyoneda f a -> f a
lowerCoyoneda (Coyoneda f m) = fmap f m

もちろん次が成り立つ。

liftCoyoneda lowerCoyoneda = id
lowerCoyoneda liftCoyoneda = id

ここで、長さ注釈つきのリストに再度登場してもらう。リストの構造については次のようになっていた。

data List s n = List {content :: [s], length' :: Int} deriving Show

また、リストを生成する命令は次のようになっていた。

data ListI s n a where
  Nil  :: ListI s n ()
  Cons :: s -> ListI s n ()

型Coyonedaにおいて、型引数fを(ListI s n a)とし、型引数aを(List s n)にすると、Coyonedaに対して具体的なイメージが湧くようになる。ここで、(List s n)に対して、関手(ListI s n a)を適用すると新たなリストが作成される。具体的には、Nilを適用すると今までのリストは無視されて空のリストが作成され。また、Cons aを与えると要素aが加わった新たなリストが作成される。

Coyonedaの使われ方のイメージを湧かせるためには上記の説明でいいのだが、オペレーショナル・モナドでは、もう少し工夫をして、Coyonedaを用いてる。プログラムを命令の並びとし、ある対象に対してプログラムが施されるとする（長さ注釈つきのリストの場合、次のようになる。プログラムは、論理の世界ではNilやCons aであり、現実の世界ではnilやconsである。対象はリストである）。プログラムは最初の命令と残りの命令の列に分けることができる。オペレーショナル・モナドでは、(Coyoneda f a)を、aを命令の先頭、fを残りの命令の列にして用いている。プログラムの実行が始まると、最初の命令が対象に対して施され、新しい対象を得る。この時、(Coyoneda f a）はプログラムが２番目の命令の列になったので、aを二番目の命令、fをそのあとの命令列にする。この操作が繰り返し行われ、すべての命令が実行された時、プログラムは終了となる。プログラムは現実の世界のものだが、命令の実行は論理の世界で実行されることに注意しないといけない（長さ注釈つきのリストの場合、プログラムはnilやcons aの並びとなるが、命令の実行ではNilやCons aが用いられる）。

今見たように、Coyonedaの型引数のfは関手であるので、Coyonedaを型クラスFunctorのインスタンスとすることができる。これは次のようになる。

instance Functor (Coyoneda f) where
  fmap f (Coyoneda g v) = Coyoneda (f . g) v

これにより、データ型ListI、即ち、対象の集合が、米田の補題を利用して、ファンクタという射の集合に移ったことになる。なお、この集合間の写像は全単射である。

命令は副作用を伴うのでファンクタをモナドに変換する必要がある。ここではフリー・モナドと呼ばれるものを利用する。プログラムは次のようになる。

data Free f a = Pure a | Free (f (Free f a))

instance Functor f => Monad (Free f) where
    return = Pure
    Pure a >>= k = k a
    Free fm >>= k = Free (fmap (>>=k) fm)

論理の世界での命令を、米田の補題を用いてファンクタとし、それをさらにモナド化したものを現実の世界での命令ということにすると、命令の集まりであるプログラムは次のように定義できる。

type Program f a = Free (Coyoneda f) a

また、論理の世界での命令を現実の世界の命令に変換するための種を用意する。Coyoneda idをモナド化した関数で、singletonと呼ばれる。

liftF :: Functor f => f a -> Free f a
liftF =  cmd = Free (fmap Pure cmd)

singleton :: f a -> Program f a
singleton = liftF . liftCoyoneda

論理的な命令はsingletonとの間で合成関数を作成することで現実の世界での命令となる。長さ注釈つきのリストの命令に対しては次のようになる。

nil = singleton Nil
cons = singleton . Cons

また、全体のプログラムは次のように定義できる。

type ListP s n a = Program (ListI s n) a

後は、前の記事でみたように、interpretを定義し、実行すればよい。