1.長さが整数のプログラムを作成
長さ注釈つきリストの構造がはっきりと分かるようにするために、前回の説明とは異なるが、長さを整数で直截に表したリストを用いる。
そこで、リストをあるものの並びと並んでいるものの数(長さ)で表すこととし、リストをレコードで記述する。この時、ある物の並びをcontent、その長さをlength'というフィールド名で表すことにすると以下のようになる。
data List s n = List {content :: [s], length' :: Int} deriving Show
次に、リストの内容を表示できるようにするために、関数displayListを用意する。
displayList x = show (content x, length' x) ++ "\n"
次に、リストに対する論理の世界での命令を用意する。リストには、空のリストを作成するためのNilとリストに新たな要素を加えるConsという命令が必要なので、それは以下のようにする。
data ListI s n a where Nil :: ListI s n () Cons :: s -> ListI s n ()
これで、論理の世界の側の準備が整ったので、現実の世界の側の準備に入る。まず、プログラムが必要となる。これは定型的な作業で、次のようにする。
type ListP s n a = Program (ListI s n) a
現実の世界での命令も必要であるが、これも論理の世界で定義した命令にsingletonという関数を適応するだけなので、次のようにする。
nil = singleton Nil cons = singleton . Cons
最後に、現実の世界と論理の世界を橋渡ししてくれるプログラムの実行部分interpretを定義する。これは、プログラムとリストを受け取り、新たなリストを生成するので、interpretの型シグネチャは次のようになる。
interpret :: ListP s n a -> List s n -> List s n
interpretは、受け取ったプログラムから、その先頭を得て、それを評価し、その結果を受けて残りのプログラムを再帰的に評価する。評価するプログラムをevalとすると、interpretは次のようになる。ここで、viewはプログラムを最初の命令とそれに続くプログラムに分解する。evalはその先頭に対して評価を行う。
interpret = eval . view
次にevalを作成する。evalは命令とリストを得て新たなリストを作り出すので、その型シグネチャは次のようになる
eval :: ProgramView (ListI s n) a -> List s n -> List s n
関数の中身はそれぞれの命令の解釈の仕方を示す。そこで、次のように記述する。
eval (Nil :>>= is) _ = interpret (is ()) List {content = [], length' = 0} eval (Cons x :>>= is) List {content = xs, length' = n} = interpret (is ()) List {content = (x:xs), length' = ((+1) n)} eval (Return _ ) lst = lst
Nilは、入力されたリストにかかわらず、長さ0の空のリストを作成し、残りの命令の実行をする。
Consは、入力されたリストに、入力された要素xを挿入し、長さが一つ大きくなったリストを作成し、残りの命令の実行をする。
Returnは、プログラムが尽きたとき、実行されるもので、この時点で生成されているリストを返す。
1.プログラムを実行する
プログラムの全体を示すと以下のようになる。
{-# LANGUAGE GADTs #-} import Control.Monad import Control.Monad.Operational data List s n = List {content :: [s], length' :: Int} deriving Show displayList x = show (content x, length' x) ++ "\n" data ListI s n a where Nil :: ListI s n () Cons :: s -> ListI s n () type ListP s n a = Program (ListI s n) a nil = singleton Nil cons = singleton . Cons interpret :: ListP s n a -> List s n -> List s n interpret = eval . view where eval :: ProgramView (ListI s n) a -> List s n -> List s n eval (Nil :>>= is) _ = interpret (is ()) List {content = [], length' = 0} eval (Cons x :>>= is) List {content = xs, length' = n} = interpret (is ()) List {content = (x:xs), length' = ((+1) n)} eval (Return _ ) lst = lst
それでは、このプログラムが正しく実行されることを示すためにテスト用のデータ(これはリストを作成するためのプログラム)を用意する。一つは、文字列を入力しストリングを作成するもの、もう一つは、数字を挿入し数のリストを作成するものである。
list1 :: ListP Char Int () list1 = do nil cons 'a' cons 'b' cons 'c' main1 :: IO () main1 = putStrLn $ displayList $ interpret list1 (List {content = [], length' = 0}) list2 :: ListP Int Int () list2 = do nil cons 1 cons 2 cons 3 main2 :: IO () main2 = putStrLn $ displayList $ interpret list2 (List {content = [], length' = 0})
main1とmain2を実行した結果は次のようになる。