オペレーショナル・モナドを解剖する（３）

１．現実の世界へ

プログラムとプログラムをつないだらプログラムだという世界を作るために、これまでの論理の世界から、一気に、現実の世界へ移行することとする。

プログラムと命令の境目を明確にするために、現実世界での命令を定義する。そのベースになるのが、singletonでそれは以下のように定義する。

singleton :: instr a -> Program instr a
singleton i = i `Then` Return

型シグネチャは、前の結果aと命令instrを入力とし、出力がプログランであるといってる。その実装は2行目に書かれているが、型引数iの命令を実行し、その結果を次に渡して、Returnを実行するとなっている。これは命令の原型である。現実の世界の命令はこのsingletonを用いて定義さする。

論理世界での命令Nilに対する現実世界での命令nilは次のようになる。

nil :: instr a -> ListProgram s n ()
nil = singleton Nil

これは、以下と同じである。

nil :: instr a -> ListProgram s n ()
nil = Nil `Then` Return

Nilは何も返さないので、上記は、Nilを実行した後、Returnを実行するとなる。また、Consは次のようになる。

cons :: s -> ListProgram s n Int
cons = singleton . Cons

これは以下と同じである。

cons :: s -> ListProgram s n Int
cons = Cons a `Then` Return

これはCons aを実行し、その結果(ここではリストの長さ)をRetunrに渡し、そして、Returnを実行するとなる。

つぎにプログラム同士をつなぐ必要があるが、そのコンストラクタは>>=で定義する。命令とプログラムを接続したコンストラクタ`Then`と似ているが、次のようになる。

(>>=) :: Program i a -> (a -> Program i b) -> Program i b
(Return a)    >>= js  = js a
(i `Then` is) >>= js  = i `Then` (\a -> is a >>= js)

上記は、二つのプログラム(i:is)と(j:js)をつなぐ。(Return a)は最初のプログラムが終了する局面を表し、(i `Then` is)は最初のプログラムの途中を実行しているときの局面を表す。

前者の方は、最初のプログラムからの結果をもらって、次のプログラム(j:js)を実行するとなっている。後者の方は、最初のプログラムで、実行しようとしている命令iから、その実行結果を受け取り、それを残りの部分isに渡してあげ、残りを実行するとなっている。

また、現実世界での命令returnは論理の世界での命令Returnとする。即ち、

Return = Return

これらは以下のように三つの法則を満足することが分かる。

return a >>= is     = is a                        -- 左単位元
is >>= return       = is                          -- 右単位元
(is >>= js) >>= ks  = is >>= (\a -> js a >>= ks)  -- 結合律

この三つの法則を満たすのはモナドである。そこで、Programをモナド化する。

instance Monad (Program instr) where
  Return a >>= js = js a
  i `Then` is >>= js = i `Then` (\a -> is a >>= js)
  return = Return

２．プログラムの実行

プログラムの全体を示すと以下のようになる。

{-# LANGUAGE GADTs #-}

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

data Program instr a where
  Then :: instr a -> (a -> Program instr b) -> Program instr b
  Return :: a -> Program instr a

type ListProgram s n a = Program (ListInstruction s n) a

data List s n = List {content :: [s], length' :: Int} deriving Show
displayList x = show (content x, length' x) ++ "\n"

interpret :: ListProgram s n a -> (List s n -> a)
interpret (Nil    `Then` is) _                                = interpret (is ()      ) List {content = [], length' = 0}
interpret (Cons x `Then` is) List {content = xs, length' = n} = interpret (is ((+1) n)) List {content = (x:xs), length' = ((+1) n)}
interpret (Return c        ) _                                = c

example1 = Cons 5 `Then` (\a -> Cons 3 `Then` (\b -> Cons 1 `Then` (\c -> Return(a + b + c))))
main1 :: IO ()
main1 = (putStrLn . show) $ interpret example1 (List {content = [4,2], length' = 2})

singleton :: instr a -> Program instr a
singleton i = i `Then` Return

nil :: ListProgram s n ()
nil = singleton Nil
cons :: s -> ListProgram s n Int
cons = singleton . Cons

instance Monad (Program instr) where
  Return a >>= js = js a
  i `Then` is >>= js = i `Then` (\a -> is a >>= js)
  return = Return

次にこのプログラムを実行する。まず三つのプログラムを用意し、それぞれは、出来上がったリストの長さを出力するものとする。

program2 = do
  nil
  cons 3
  cons 8
  x <- cons 9
  return x

program3 = do
  nil
  cons 4
  cons 6
  cons 1
  x <- cons 8
  return x

program4 = do
  nil
  cons 3
  cons 6
  x <- cons 6
  return x

三つのプログラムをつなぎ、得られた三つのリストの総和を求める。

program = do
  a <- program2
  b <- program3
  c <- program4
  return (a + b + c)
 
main :: IO ()
main = (putStrLn . show) $ interpret program (List {content = [1,2], length' = 2})

得られた結果は10となり、期待通りの値が得られたことが分かる。

３．米田の補遺との関係

今回の説明では、米田の補題を用いることなく説明した。前の記事で書いた米田の補題との関わり合いを最後に述べておく。「オペレーショナル・モナドで天国と地獄を行ったり来たり」の説明で、Monadを作成した。しかし、米田の補題でのCoyonedaを用いれば、Coyonedaがファンクタであることから、Monadの値コンストラクタが自動的に得られえる。従って、Monadの値コンストラクタを定義することなく、利用できることが米田の補題の利点であったことが分かる。