最近Haskellerの間で人気になりつつある(？)Operational Monadというものについての記事です。

サンプルプログラム

Operational Monadは http://hackage.haskell.org/package/free-operational で定義されています。後でも説明しますがこれはFree Monadの構造をもったモナドになります。

以下のコードはhttps://gist.github.com/myuon/5737483に載せておきました。

{-# LANGUAGE GADTs #-}
import Control.Monad
import Control.Monad.Operational.Simple

data Simple a where
  End :: Simple a  
  Put :: String -> Simple ()
  Get :: Int -> Simple String

ここではGADT拡張を使います。上ではSimpleというデータ型のコンストラクタの宣言を、型クラスの函数宣言のようにして作っています。

Free Monadの記事(Free Monadを使ってみよう！ - みょんさんの。とFree Monadを使ってみよう！(2) - みょんさんの。)のところでもやりましたが、Free Monadとして使うために、必要な値を受け取ってSimple型を返す函数を作ってあげなければいけません。
それが以下です。

put :: String -> Program Simple ()
put = singleton . Put
 
end :: Program Simple a
end = singleton End
 
get :: Int -> Program Simple String
get = singleton . Get

最後に、これをrunするためのものが必要ですね。ここで使われているinterpretという函数はControl.Monad.Operational.Simpleで定義されています。

run :: Program Simple a -> IO a
run = interpret step
  where
    step :: Simple x -> IO x
    step (Put a) = putStrLn a
    step End = putStrLn "End" >> undefined
    step (Get n) = replicateM n getChar

これでおしまいです。あとは適当なプログラムを書いて走らせましょう。

tinyProgram = do
  put "hello, world!"
  end
  
main = run tinyProgram

実行結果

hello, world!
End
Operational.hs: Prelude.undefined

Operational Monad

上で作ったtinyProgramはdo記法を使っていることからも、Simple型がモナドとして機能していることは分かります。しかし、私達はSimple型をMonadはおろかFunctorにすらしていません。しかしなぜこんなことができるのでしょうか？結論から言ってしまえば、Simple型はOperatinal Monadの力によってFunctorを経てFree Monadの構造が与えられているのです。

どういうことでしょうか。Operational Monadの定義から考えてみましょう。

-- http://hackage.haskell.org/packages/archive/free-operational/0.3.0.0/doc/html/src/Control-Monad-Operational-Simple.html#Program

newtype Program instr a = Program { toFree :: Free (Yoneda instr) a }

実は、重要なのはここだけです。FreeというのはFree Monadですが、その中にYonedaというものが見えると思います。これはつまり、


inst	ただのデータ型
Yoneda instr	Functor
Free (Yoneda instr) a	Free Monad

という関係になっているのです！

次に出てくる疑問は、ではただのデータ型をFunctorにしているYonedaというのは何？ということでしょう。これは圏論で登場する米田の補題という有名な補題に関係があります。

(Yoneda f) functor

米田の補題を理解するためには少しだけ準備が必要ですが、ここに書ききれるものではないので簡単に説明だけして終わることにします。
興味がある方は補足のところを読んで下さい。

米田の補題で重要なのは、普通の集合と函手の集合には全単射の関係があるということです。つまり、ある集合から1つ元を取り出すと、函手が1つ作れる、あるいはその逆も可能という対応関係です。

つまり、自分でデータ型を、函手に対応づけすることができる = データ型から函手を作ることができるという対応です。

以下に定義を示します。

-- http://hackage.haskell.org/packages/archive/kan-extensions/3.1.1/doc/html/src/Data-Functor-Yoneda-Contravariant.html#Yoneda

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

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

ご覧の通り、(Yoneda f)はFunctorになっていますね！これは、与えられたfというデータ型を使って、(Yoneda f)というFunctorを創りだすことができるということを示しています。まさに魔法のようですね！

何度も言いますが、与えられたデータ型を使って、(Yoneda f)というFunctorを創りだすことができることが「米田の補題」によって保障されているわけです。

(補足)Yoneda lemma

米田の補題は圏論では非常に有名な補題(というか定理)で、ここから色々な定理を示すことができる強力な定理です。
補題のステートメントは単純で、
$F:\mathscr{C} \to Set$ が函手(functor)のとき、 $\Phi:Set^{\mathscr{C}^{op}}(\mathscr{C}(-,c), F) \simeq F(c)$ なる写像が存在する(つまり上の写像 $\Phi$ が全単射となる)ということです。
ここで、 $\Phi(\alpha) = \alpha_c 1_c$ 、つまり $\alpha:F \to \mathscr{C}(-,c)$ という自然変換を $\alpha_c 1_c$ という元に対応させています。

上で出てきた函手 $\mathscr{C}(-,c)$ を、Yoneda函手 $Y_c$ と言います。

これは函手圏 $Set^{\mathscr{C}^{op}}$ の射である自然変換の集合と、集合圏の対象である集合との間に全単射の関係があるということを意味しています。

これによって、自然変換と集合の元を対応させることができます。これが、Haskellでは一体どういった意味を持つのでしょうか？

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

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

Yonedaは射(b -> a)と対象(f b)を受け取ってYoneda f aなるデータ型を返します。f(に対して定義されたfmap)を上で出てきた函手Fだと思いましょう。

圏論	Haskell
$\mathscr{C}$ の射	(b -> a)
$F:\mathscr{C} \to Set$	fmap :: (b -> a) -> f b -> f a
$Y_c:\mathscr{C} \to Set$	fmap :: (b -> a) -> (Yoneda f) b -> (Yoneda f) a
$\alpha:F \to Y_c$	nat1 :: forall2 b. f b -> (Yoneda f) b
$\alpha_c:F(c) \to Y_c(c)$	Yoneda (b -> a) :: f b -> (Yoneda f) a
$\alpha_c(1_c) \in Y_c(c)$	Yoneda (b -> a) (f b) :: (Yoneda f) a

米田の補題が言っているのは、(Yoneda f) a と nat :: forall b. f b -> (Yoneda f) b とが確かに対応すること、つまりこの意味でのYonedaが

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

と定義することができる(このような写像が常に存在する)ことを言っていたのです。

参考文献

Freeモナドを超えた！？operationalモナドを使ってみよう - モナドとわたしとコモナド Operational Monadの存在をここで知りました
http://hackage.haskell.org/package/free-operational YonedaとFree Monadを使ったOperational Monadの実装
http://hackage.haskell.org/package/kan-extensions Yoneda等が定義されているパッケージ
Understanding Yoneda | Bartosz Milewski's Programming Cafe 自然変換をHaskellで表現するとはどういうことか、などに興味があれば読んでみて下さい。補足のところで説明もなく使ったforallの扱いなどが丁寧に解説されています。

*1:プログラム中には直接は出て来ませんが、forallを取り除いたバージョンが liftYoneda = Yoneda id として定義されています。

*2:圏論でいう``natural in d"に対応するのがHaskellでのforall d.に対応すると考えてよいみたいです。詳しくは参考文献の4を参照。

Just $ A sandbox

プログラミングと計算機科学とかわいさ

Yoneda lemmaとOperational Monad

サンプルプログラム

Operational Monad

(Yoneda f) functor

(補足)Yoneda lemma

参考文献