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

１．長さを帰納的に表現した注釈つきリスト

元に戻って、リストの長さを整数ではなく帰納的表現でのリストの生成法を考える。最初に自然数Natを代数的データ型で定義する。

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

ここで、Zは自然数の始まりを示し、S (Nat n)は自然数(Nat n)の次の自然数を表す。Natは型コンストラクタ、nは型引数、ZとSは値コンストラクタである。

次に、自然数を実際の整数に対応させるために関数toIntを用意する。

toInt :: Nat n -> Int
toInt Z = 0
toInt (S n) = 1 + (toInt n)

論理の世界でのリストは次のように定義する。(長さを整数で表したときは、length'をIntとしたが、今回は型引数そのものを用いた。)

data List s n = List {content :: [s], length' :: n} deriving Show

また、リストの内容を表示する関数displayListを用意する。これには、帰納的に表現された長さを整数に変換する必要がある。displayListは次のようになる。

displayList x = show (content x, toInt $ length' x) ++ "\n"

論理の世界での命令、現実の世界でのプログラム、命令は長さを整数で表した時と同じである。
評価evalでは、整数の長さに代わって、帰納的な表現の長さを用いるので、次のようになる。

    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 _      ) lst                              = lst

２．プログラムを使ってみる。

プログラムの全体は次のようになる。

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

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 a = Program (ListI s n) a

nil = singleton Nil

cons = singleton . Cons

interpret :: ListP s (Nat n) a -> List s (Nat n) -> List s (Nat n)
interpret = eval . view
  where
    eval :: ProgramView (ListI s (Nat n)) a -> List s (Nat n) -> 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 _      ) lst                              = lst