読者です 読者をやめる 読者になる 読者になる

bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

オペレーショナル・モナドで天国と地獄を行ったり来たり(4)

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

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

プログラム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)))で返す。

:2.プログラムを実行する

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

{-# 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})

実行結果は次のようになる。
f:id:bitterharvest:20140922163205p:plain