オペレーショナル・モナドで天国と地獄を行ったり来たり（４）

:１．リストの要素をキーボードから入力する

「Haskellで分野向けの機械を開発する（３）」で行ったように、オペレーショナル・モナドの拡張版(モナド変換子）を用い、キーボードからリストの要素を入力できるようにする。

プログラムListPは命令実行結果aがモナドとなるように次のように変更する。

type ListP s n m a = ProgramT (ListI s n) m a

現実世界での命令の戻り値がモナドなどであることを示すために、次のように変更する。

nil :: (Monad m) => ListP s n m ()
nil = singleton Nil
cons :: (Monad m) => s -> ListP s n m ()
cons = singleton . Cons

プログラムを解釈するinterpretも、モナドのリストを返すので、型シグネチャを次のように変更する。

interpret :: (Monad m) => ListP s (Nat n) m a -> List s (Nat n) -> m (List s (Nat n))

次に、interpretの関数を修正する。

interpret is list = (\v -> eval v list) =<< (viewT is)
  where
    eval :: (Monad m) => ProgramViewT (ListI s (Nat n)) m a -> List s (Nat n) -> m (List s (Nat n))
    eval (Nil    :>>= is) _                                = interpret (is ()) List {content = [], length' = Z}
    eval (Cons x :>>= is) List {content = xs, length' = n} = interpret (is ()) List {content = (x:xs), length' = (S n)}
    eval (Return _      ) list                             = return list

interpretは引数にisとlistを有する。isは前の命令での実行結果であり、listは命令列を表している。これは、命令列と、viewTから前の命令の実行結果を得て、evalでプログラムを実行する。

evalは、命令列の最初の命令(ProgramViewT (ListI s (Nat n)) m a)を取り出し、現在のリスト(List s (Nat n))に対して論理の世界でその命令を実行し、その結果をモナドでのリスト(m (List s (Nat n)))で返す。

:２．プログラムを実行する

プログラムの全体を示す。

{-# LANGUAGE GADTs #-}
import Control.Monad
import Control.Monad.Operational
import Control.Applicative
import Control.Monad.Trans

data Nat n = Z | S (Nat n) deriving Show

toInt :: Nat n -> Int
toInt Z = 0
toInt (S n) = 1 + (toInt n)
  
data List s n = List {content :: [s], length' :: n} deriving Show
displayList x = show (content x, toInt $ length' x) ++ "\n"

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

type ListP s n m a = ProgramT (ListI s n) m a

nil :: (Monad m) => ListP s n m ()
nil = singleton Nil

cons :: (Monad m) => s -> ListP s n m ()
cons = singleton . Cons

interpret :: (Monad m) => ListP s (Nat n) m a -> List s (Nat n) -> m (List s (Nat n))
interpret is list = (\v -> eval v list) =<< (viewT is)
  where
    eval :: (Monad m) => ProgramViewT (ListI s (Nat n)) m a -> List s (Nat n) -> m (List s (Nat n))
    eval (Nil    :>>= is) _                                = interpret (is ()) List {content = [], length' = Z}
    eval (Cons x :>>= is) List {content = xs, length' = n} = interpret (is ()) List {content = (x:xs), length' = (S n)}
    eval (Return _      ) list                             = return list

このプログラムを動かしてみる。関数makeListは、リストを作るために、文字を三つ入力できるようになっている（整数のリストを作りたければ、LispPの後のCharをIntに変える）。makeListを用いてmain関数を以下のように定義する。

makeList :: ListP Char n IO ()
makeList = do
  nil
  (liftIO . putStrLn) "Input an element."
  cons =<< read <$> liftIO getLine
  (liftIO . putStrLn) "Input an element."
  cons =<< read <$> liftIO getLine
  (liftIO . putStrLn) "Input an element."
  cons =<< read <$> liftIO getLine

main :: IO ()
main = do
  (putStrLn . displayList) =<< interpret makeList (List {content = [], length' = Z})

実行結果は次のようになる。