間脳の第3脳室の上壁最後部から後上方に突出する0.2グラムほどの小体。7歳くらいまではよく発達し，内部に松果細胞という腺細胞様のものが集まる。年齢が進むと石灰化が起こり脳砂というクワの実状の凝固物が多数現われる。松果体の分泌物は生殖器の成熟を抑制するという説もあり，内分泌腺の一つに数えられ，松果腺とも呼ばれたが，その機能は不明な点が多い。下等脊椎動物(魚類，トカゲなど)では色素細胞を収縮させる作用をもつ。

（平凡社マイペディア百科辞典より）

現代の計算機科学における心と体の問題

仮想的な存在であるソフトウェアはどのように実世界と相互作用するか？

¨ 初期には計算機は、各種の計算を行うような「心」の延長部分であった。

¨ 現在では計算機は、各種の操作を行うような「体」の延長部分である。

古典的な計算モデル

¨ 古典的な計算モデル(Turing機械やλ計算)は体を持たない心のようなもの。

(テープからテープ、λ項から正規形)

これらのモデルでは、計算の最初に入力(テープや項)を受け取り、計算の終了後に出力(テープや項)を出すので、バッチ処理には適合している。

Turing機械やフローチャートは命令型ではあるが、これら古典的モデルではプログラムは入力から出力への関数と考えられており、本質的には宣言的だった。

近年の計算モデル

相互作用を含む計算のモデルが発達してきた。(体の中にある心に類似)

¨ petri net：トークンを受け取り、(発火した)位置を返す。

¨ MacQueen's stream：データはコルーチンの間を巡る。

¨ process calculi：チャネルの間でメッセージがやり取りされる。

これらでは入力/出力に特別な配慮はいらず、各々についてトークンの源と行き先、追加のストリーム、追加のチャンネルを増せばよい。

これらの理論により、単一入力―単一出力から時間及び空間的に分布した多重入力―多重出力になり、実際的な相互作用のある計算に適合するようになった。

monad

ここでは、相互作用を扱うための解法として、関数型プログラミングで知られるようになった、monad（単子）という概念を紹介。

¨ 圏論（category theory）で見出された。

¨ あらゆる言語について非停止性（non-termination）、状態（state）、例外（exception）、continuation、相互作用（interaction）といった特徴を扱える。

¨ pureでlazyな関数型言語HaskellについてGlasgow版で導入され、Chalmers版、Yale版、標準にも取り入れられた。

¨ 1万行以上の長いプログラムやGUIを含む様々な分野のアプリケーションで試されている。

¨ 宣言型プログラミング言語Escherで論理型と関数型プログラミングの統合に利用された。

ここで説明すること

¨ pure関数型言語に相互作用を追加するものとしてmonadを紹介。

¨ lazyな関数型言語であるHaskellの標準にmonadを導入した結果、何が簡単になったかを他方式（synchronized stream、continuations、linear logicやside effect）との比較によって紹介。

¨ 逐次的で決定的な事例について述べ、相互作用としばしば関連付けられる並列性（concurrency）、非決定性（non-determinism）についてはポインタを提示するに留める。

読者についての前提

¨ Haskellのような純粋な関数型言語とSMLのような純粋でない関数型言語でのプログラミングの基本。

¨ 圏論に関する理解は不要。

2.相互作用へのmonadアプローチ

基本的な命令

IO()型の項は作用を示すが、（lazyな関数型言語では）その実行が保証されているわけではない（まだ「心」の領域にある）。

この動作の意図とその実行の区別は重要。

IOの後に続く()の意味は後述。

表 2.1：基本命令（主として出力に関する）

名	型	説明
putc	Char->IO()	文字の出力意図を示す関数。
done	IO()	何もせずに正常終了する意図を示す定数。
>>	IO()->IO() ->IO()	動作の逐次的な実行意図を示す2項結合演算子。（Haskellの流儀に従いcurry化されている）
puts	String ->IO()	文字列の出力意図を示す関数。以下のようにしてputc、doneと>>で記述できる。 puts [] = done puts (c:s) = put c >>puts s
main	IO()	一連の項が返す実行意図を示す値が、このトップ・レベルにある変数に束縛されて初めて実行が保証される。（「松果体」）例： main::IO() main = puts "!?"

実行意図を実行に結びつけるmainという「狭い」インターフェースがボトルネックに見えるが、実は相互作用と計算を任意に混合できるほどに表現力がある。

Equational reasoning

重要な原則であるequational reasoningには「参照の透過性」（referential transparency）、「ライプニッツの規則」（the rule of Leibniz）など多くの別名がある。

ここで述べるアプローチでは命令は単純なequational reasoningを可能にするよう、副作用を持たないようにする。

例（副作用で出力するＳＭＬ）

putcML #'h'; putcML #'a';

の出力は"haha"だが、

let val

x = (putcML #'h'; putcML #'a')

in x; x end

としてequational reasoningが行われると出力は"ha"（xに束縛したときだけ）となって意図したものと異なる。

let fun

f() = (putcML #'h'; putcML #'a')

in f(); f() end

のようにダミー引数を持つ関数として「行為」を定義すれば意図通り動くが、値と行為は異なったものとして抽象化せねばならなくなる。

例（monadを利用したHaskell）

putc 'h' >> putc 'a'>>

putc 'h' >> putc 'a'

と

let

x = (putc 'h' >> putc 'a')

in x >> x

の出力はどちらも同じ"haha"となる。（関数の返すIO()型の値そのものは「出力の意図」を示しているだけで副作用はない。）

値を受け入れる命令

IO aは型aの値を受け入れるという動作意図を示す。

表 2.2：入力に関する基本命令

名	型	説明
getc	IO char	文字の入力意図を示す関数。
return	a -> IO a	型aの値から型aの入力意図を示す項を作る関数。
>>*	IO a -> IO b -> IO (a,b)	入力動作の逐次的な実行と、入力値の組の作成意図を示す2項結合演算子。（Haskellの流儀に従いcurry化されている）
>>@	IO a -> (a -> b) -> IO b	入力意図を示す値とフィルタを示す関数を取って、入力をフィルタリングする意図を示す2項演算子。（Haskellの流儀に従いcurry化されている）
gets	Int -> IO String	文字列の入力意図を示す関数。以下のようにreturn、getc、>>、>>@を使って定義できる。 gets 0 = return [] gets (i+1) = (getc >> gets i) >>@ \(c,s)-> c:s

getsは指定された個数の文字をgetcで読みこむまで、>>*で入力を結合しながら再帰的にgetsを呼び出し、各段でgetcが返した文字をgetsが返した文字列からなる組を（>>@に渡されたフィルタ関数を使って）文字列に変換する（という意図を示す）。

letの類似物

前節の>>*と>>@の組み合わせは自然ではあるが、読み易いとは言えない。

（￥はバックスラッシュです。Haskellでバックスラッシュはλ抽象を表わします。）

表 2.3：束縛（bind）演算子

名

型

説明

>>=

IO a -> (a -> IO b)

-> IO b

束縛（bind）と呼ばれる2項演算子。入力意図を示す項、とその入力値を受けとって次の入力意図を示す項を返す関数を受け取って結合し、逐次的な入力動作を示す。（Haskellの流儀に従いcurry化されている）

let式の型推論式

>>=式の型推論式

この2者を見比べると似ている。そこからこの>>=式の意味を考える。

>>=とλ形式の関数が利用されている場合、この式が実行されれば、入力動作mの入力値をxに束縛して次の入力動作nを行なうと解釈できる。

これは入力をletでの束縛時に副作用として行なうSMLの場合と似ているが、>>=利用の場合はequational reasoningが可能。

>>=を使って幾つかの命令は記述できるほか、重複した機能の命令が幾つか削減できる。

表 2.4：命令の整理

式	代替記述
m >>* n	m >>= \x-> n >>= \y-> return (x,y)
m >>@ f	m >>= \x-> return (f x)
done	return ()
m >> n	m >>= \() -> n

以下は書き換えたgetsの定義

gets 0 = return []

gets (i+1) = getc >>= \c ->

gets i >>= \s ->

return (c:s)

これは先ほどより読みやすい（通常の命令型プログラミングの形式に近くなっている）。

表 2.5：最終的に生き残った基本入出力命令

名	型
return	a -> IO a
>>=	IO a -> (a -> IO b) -> IO b
putc	Char -> IO ()
getc	IO Char

これらの命令はIO aという抽象データ型に属する操作。（これらによって作られた項が変数mainに束縛されると実行が確定する。）

monadの満たす法則

done >> m = m

m >> done = m

m >> (n >> o) = (m >> n) >> o

以上のように>>という演算は結合則が成り立ち、doneを単位元とするモノイド（単位的半群：単位元を持つ半群、可換でなく逆元の存在も保証されない）を構成する。同様に、

return v >>= \x->m = m[x := v]

m >>= \x-> return x = m

m >>= \x -> ( n >>= \y -> o)

= (m >>= \x-> n) >>= \y-> o

>>=演算にも結合則が成り立ち、returnを単位元としてモノイドを形成する。

Kantから借用したcategoryという語自身を始めとして、圏論（category）が哲学から用語を拝借していることはあまり有名ではない。上記のような構造に対してLeibnizから借用したmonadは、monoidに触発された洒落である。（Leibnizの場合、神と同様に各魂はmonadであったのでmonadは心と体の問題の中心であった。）

（本文より）

ここで入出力でなく型構成子についても以下のように定義すると同様の性質を満たす。

表 2.6：一般の型構成子monad

名	型
return	a -> M a
>>=	M a -> (a -> M b) -> M b

同様にして多くのことがmonadとして表わせるが、それについては後述。

　またこのような関係は

(let x=v in m) = m[x:=v]

(let x=m in x) = m

(let y=(let x=m in n) in o)

= (let x=m in (let y=n in o))

のように、letについても成り立つが、SMLの場合は副作用の存在により部分的に成立しなくなる。（例：最初の法則が成り立つにはvは任意の項ではなく副作用なく評価可能な値でなければならない。）

副作用のないHaskellではより強い法則が成り立つ(変数に限られていたvが任意の項nになる。)：

(let x=m in n) = n[x:=m]

monadの法則を使ってプログラムの挙動を証明できる。

例：

puts r >> puts s = puts (r++s)

と

gets i >>= \r ->

gets j >>= \s ->

return(r++s)

ただし、

[]++s = s

(c:r)++s = c:(r++s)

（証明は省略：順に式を展開して、単位元との演算を簡約してから帰納法）

monadと命令型プログラミング

echo: Haskell（monad）版

echo :: IO()

echo = getc >>= \c ->

if (c== '\n') then

return ()

else

putc >>

echo

echo: C版

echo () {

int c;

loop: c = getchar()

if (c == '\n') {

return

} else {

putchar (c);

goto loop;

}

この両者は良く似ている。関数型言語でmonadを使って命令型プログラミングを模倣する意味はあるのか？

¨ ある。ある種の相互作用は命令型で書いた方が素直に表わせる。

¨ ない。既に関数型独自のテクニックが知られていて、それを使えば良い。

両者は同じ位に無駄がなく、コンパイルすれば似通ったコードになるだろう。（Glasgow Haskellコンパイラではequational reasoningを活用した最適化により、そういう結果を得ている。）

ただ、monadを利用している場合、両者を混合して利用できる。

例：

prod :: [IO a] -> IO [a]

prod [] = return []

prod (m:ms) = m >>= \x->

prod ms >>= \xs->

return (x:xs)

高階関数を用いた版のputs、getsでこの関数を利用できる。

puts = prod (map putc s) >>= \_->

return ()

gets i = prod (take i (repeat getc))

prodのような働きの高階関数を書き上げる能力は命令型言語に新たな特別目的の構文を定義する能力に近いものがある。

C関数の直接呼び出し

ここまでの仕組みを拡張すればHaskellから任意のCの関数（ライブラリ関数も含めて）を直接呼び出せる。（理論的には入出力と見なせるから。）

ccall proc e1 e2 ... en

procはCの関数名、e1～enそれぞれはChar、Int、Floatのいずれかの型を持つ式で式全体はIO Char、IO Int、IO Floatのいずれかの型を持つ。（Haskellにおいてこれら以外の型をCで特殊な関数を書かずにやり取りする方法は将来の課題）

put c = ccall putchar c

getc = ccall getchar

　上のようにputc、getcも簡単に定義できる。

3.相互作用に対するその他のやり方

相互作用を表現するために用いられる幾つかの方法をmonadと比較する。

¨ monadを表現

¨ monadで表現（可能ならば）

同期されたストリーム（synchronized stream）

入出力に関するstreamモデルは関数言語のそのほかの機能同様、宣言的な意味論に関する研究から興った。

以前の版のHaskellでも使われていた。

synchronized streamによる相互作用

表 3.1：synchronized streamの基本データ型

data Request = Getq | Putq Char

data Response = Getp Char | Putp

ストリームはプログラムが作成する要求（GetqかPutq c）のリストとプログラムが得る応答（Getp cかPutp）のリストであらわされる。

type Dialogue = [Response] -> [Request]

トップレベルの関数は応答リストから要求リストへの関数。

プログラムからの各要求（入力に応じて行なわれた動作）は対応する反応（実際に入力された列）に先立って出されなければならないように、入出力に対するこのアプローチはlazyな評価に依存する。

例echoD：synchronized stream版

echoD :: Dialogue

echoD p =

Getq :

case p of Getp c : p' ->

if (C == '\n') then

[]

else

Putq c :

case p' of Putp : p'' ->

echoD p''

:はリストの連結演算子。case v of p ->はパターンマッチング。

入出力例：

echoD [Getp'A',Putp ,Getp'B',Putp ,Getp'\n']

= [Getq ,Putq'A',Getq ,Putq'B',Getq ]

synchronized streamによるmonadの表現

IO a ::([Response],[Request])

->(a,[Response],[Request])

IO aを関数で表わす。この関数は[Response]の項を消費した分だけ[Request]の項を作成する。

表 3.2： synchronized streamで表わしたmonadの基本命令

名	型	定義
putc c	Char->IO ()	\(p,q)->let q = Putq c : q' Putp : p' = p in ((),p',q)
getc	IO Char	\(p,q)->let q = Getq : q' Getp c : p' = p in (c,p',q)
return x	a -> IO a	\(p,q)->(x,p,q)
m >>= k	IO a ->(a->IO b) ->IO b	\(p,q'')->let (x,p',q)=m(p,q') (y,p'',q')=k x (p',q'') in (y,p'',q)

こうして定義されたmonadは前述の法則を満たす（証明略）。

monad によるsynchronized streamの表現

可能ではあるが大変効率が悪いことがわかっている。

monadをstreamで表現することは比較的容易だが、逆は容易でない。

synchronized stream対monad

しばしば入出力に関するセマンティクスとして利用されるので、monadをstreamの観点から定義したものは、入出力monadのセマンティクスと見なせる。

しかし要求と応答という２つのストリームに注意を払わねばならず煩雑。

monad版のように連結することも難しく、モジュラリティが達成しづらい。

continuation

continuationは入出力に関するstreamモデルを生で見せないで包むためにmonad同様に利用されている。

continuationは初期のHaskellで使われていた。さらにHopeでは抽象データ型を用意して使っていた。歴史的にはmonadの先輩に当たり、monad同様流れの制御のモデルとして見出された。

ここでは抽象データ型を介したcontinuationを考える。

continuationによる相互作用

作用を行なう関数は引き続いて行なうべき操作を示すAnswer型の引数が追加されている。

トップレベルの変数はAnswer型[1]。

表 3.3：continuationの基本命令

名	型
putcK	Char->Answer ->Answer
getcK	(Char->Answer) ->Answer
doneK	Answer

例echoK'：continuation版

echoK' :: Answer->Answer

echoK' k = getcK(\c->

if (C == '\n') then

else

putcK c (echoK' k)

)

例：continuation版の連結

mainK = echoK' (echoK' doneK)

しかし関数の定義が以下のように

例echoK：continuation版（物忘れ版）

echoK :: Answer

echoK k = getcK(\c->

if (C == '\n') then

doneK

else

putcK c echoK

)

なっている場合は、Answerを受け入れるように作っていないので連結できない。

continuationによるmonadの表現

IO a ::(a->Answer)->Answer

IO aを関数で表わす。この関数は現在の動作で得られる入力（空()かも知れない）を受けとって次の処理を行なう関数をcontinuationとして取る。

表 3.4： continuationで表わしたmonadの基本命令

式	型	定義
putc c	Char->IO ()	\j->putcK c (j ())
getc	IO Char	\j->getcK j
return x	a -> IO a	\j->j x
m >>= k	IO a ->(a->IO b) ->IO b	\j-> m(\x->k x(\y->j y))

こうして定義されたmonadは前述の法則を満たす（証明略）。

monad によるcontinuationの表現

簡単に可能。

表 3.5：monadで表わしたcontinuationの基本命令

式	型	定義
Answer	IO () \| IO c
putcK c a	Char->Answer ->Answer	putc c >>= a
getcK a	(Char->Answer) ->Answer	getc >>= a

　モデルとしては同等。

continuation対monad

プログラムの構造は殆ど同一。概念的にも類似している。

continuationは>>=のような結合演算の機能を関数に含めている。

それだけに物忘れ版echoKのように定義するときにcontinuationを受け入れるように作るのを忘れると、後から直接に結合できない。

continuation用の変数がソース内に散らばっていて混乱し易いので若干monadの方が抽象的。

ただ、エラー時の分岐ほか、フローの制御が直接にサポートできる利点がある。

線形論理（linear logic）

Giraldによって提唱されたlinear logicは論理を拡張して項の数を保存する推論規則を備えたもの。Curry-Howard同型を介して、論理→プログラム、命題→型（複製が発生しない）と写像してプログラムの動作の証明に用いられた。

linear logicはCleanで相互作用の表現に使われ、Machintoshのグラフィックス・ツールと同等の表現力を備えた高度なインターフェースを持つアプリケーションが作成されている。

ここでは「状態」の複製を防ぐ目的で線形論理に基づく特別に洗練された型システムを利用する。

linear logicによる相互作用

作用によって変化する外界の状態を表わす*World型を利用する。状態の合流、分岐について考えずに済ますため、状態*Worldは複製できない型とする。

トップレベルの関数mainLは*Worldから*Worldへの関数。

表 3.6：linear logicの基本命令

名	型
putcL	Char->World ->World
getcL	World ->(Char,*World)
mainL	World->World

*が先頭についている型は丸ごとは複製できない型を表わす。*(Char,*World)では*(Char,*World)や*Worldは複製できないが、Charは複製可能で取り出して利用できる。

例echoL：linear logic版

echoL :: *World->*World

echoL w = let

(c,w') = getcL w

if (C == '\n') then

else

let

w'' = putcL c w'

echoL w''

例：linear logic版の連結

mainL = echoL (echoL w)

linear logicによるmonadの表現

IO a ::*World->(a,*World)

IO aを関数で表わす。この関数は作用前の状態を表わす引数を受けとり、入力された値と作用後の状態との対を返す。

表 3.7： linear logicで表わしたmonadの基本命令

式	型	定義
putc c	Char->IO ()	\w->((),putcL c w)
getc	IO Char	\w->getcL w
return x	a -> IO a	\w->(x,w)
m >>= k	IO a ->(a->IO b) ->IO b	\w->let (x,w')=m w (y,w'')=k x w' in (y,w'')

こうして定義されたmonadは前述の法則を満たす（証明略）。

例： mainLにmainを埋め込む

mainL::*World->*World

mainL = \w->let

((),w')=main w

ここでmain::IO ()は初期状態を取って()と最終状態との対を返す関数になる。

monad によるlinear logicの表現

定義する方法は明らかでない。

linear logic対monad

linear logicは洗練された型システムを必要とする。

状態変数がソース内に散らばっていて混乱し易い。（その上、取り違えると劇的に意味が変わる。）しかしlinear logic上にmonadを定義すればこの混乱は抑えられる。

状態を具体的な(例：スクリーンの状態やファイルの保存状態など)複数の状態からなる状態に分割できるならば、状態が明示できる利点がある。

バランスがどのあたりに落ち着くかは今後の課題。

副作用（side effect）

side effectはLISPやIswimからSchemeやSMLに至るまでが利用している伝統的な方法。

HaskellとSMLの表記法

表 3.8：表記対照表

Haskell	SML
()::()	():unit
'\n'::Char	#"\n":char
(\x->x)::a->a	(fn x=>x):'a->'a
型変数は小文字始まり	型変数は'で始まる
型構成子の後に引数	型構成子の前に引数
―	型signaureはvalで始まり、プログラム中のあちこちにある。
―	定義はvalかfunで始まり、慣習的にグループにまとめる
―	定義の直後にsignatureを置かないのが無難

side effectによる相互作用

表 3.9：side effectの基本命令

名	型
putcML	char->unit
getcML	unit->char

これらの関数は適用されたときに相互作用を実行します。

表 3.10：side effectにおける心と体

「考え」	「行為」
abstraction	application
(fn c => putcML c; putcML c)	f #"!"

副作用による場合は、他の全ての例とは異なり特別なトップ・レベルの変数は必要ない。

例echoML：SML表記 side effect版

val echoML : unit->unit

fun echoML () = let

val c = getcML ()

if (c = #"\n") then

()

else

(putcML c; echoML())

付録：基本命令の定義

fun putcML c = TextIO.output1(TextIO.stdOut,c);

fun putcML c = TextIO.input1(TextIO.stdIn);

side effectによるmonadの表現

side effectをmonadの内に閉じこめる事ができる。そうして相互作用に対するmonad式のやり方と副作用を完全に混合できる。

type 'a io :unit->'a

IO aこと'a ioを関数で表わす。この関数は引数なしに副作用として相互作用を行ない、入力された値（空かもしれない）を返す。

表 3.11： side effectで表わしたmonadの基本命令（SML表記）

式	型	定義
putc c	char->unit io	fn()=>putcML c
getc	char io	fn()=>getcML ()
return x	'a -> 'a io	fn() => x
m >>= k	'a io * ('a-<'b io) ->'b io	fn()=>let val x=m () val y=k x () in y end
done	unit io	return ()
m >> n	unit io * unit io -> unit io	m>>=(fn()=>n)
fix h	('a io->'a io) ->'a io	let fun f() = h f() in f end
SMLでは再帰定義は関数についてだけ可能なので、抽象データ型'a ioを利用するためには不動点演算子fixを定義する。これは抽象データ型'a ioがunit->'aと事実上同一であることに依存。しかしいったん関数が定義されれば'a ioは抽象データ型としてのスコープにある。こうして val execute : unit io -> unit fun execute m = m() により「松果体」で関数として実行できる値が得られる

例： side effectで定義したmonadの使用（SML版）

val echo : unit io

val echo = fix(

fn echo =>

getc >>= (

fn c =>

if (c=#"\n") then

done

else

putc c >> echo

)

fix演算子など文法上の都合からくるマイナーな差異以外はHaskell版と同一のコード。

こうして定義されたmonadは前述の法則を満たす（証明略）。

ただし第1に

return v >>= fn x=>m = m[x:=v]

は項vは任意でなく、値でなければならない。

第２にSMLのようなstrictな言語はHaskellのようなlazyな言語とは違うrestriction reasoningを行なう。

通常の値呼び出し（call-by-value）λ_v計算はこれらの法則を証明するには十分ではない。より強力なλ_c計算（Moggiによる）を利用するべき。

monad によるside effectの表現

定義できない。

4.関連研究

（省略）

5.結論

monadは宣言的なプログラミングにおいて強調的な相互作用の開発に適した手法

連携

プログラミング言語は孤立して用いられることはない、他言語や様々な要素（ネットワーク、データベース、・・・）との協調性、再利用性が必要。

したがって本文中のC言語との連携の例が重要になってくる。他にも複雑なデータのやり取りのし方、メモリ管理、並列性、GUI・・・についてmonadは有効。

将来の課題

¨ 深部まで書いてからmonadを使おうとすると書き換えが必要。（オール・オア・ナッシング）

¨ 二つの相互作用が必要な際に１つのmonadで二つを扱う傾向がある。

monadなしからmonad１つ、複数monadの利用までを滑らかに移行できる必要がある。

一階と高階

>>=が高階だからといって、prologのような一階の言語でmonadの概念が利用できないわけではない。（Moggiは当初から、高階言語とは独立に、一階の言語に対して適用できるように骨を折ってきた。）

高階の(\x->n)mは一階のlet x=m in nに似ているから、高階のm>>=\x->nは本質的には一階であるlet構文に似ている。これをlet x<-m in nとして提案している。

したがって、一階の型付き言語にmonadを追加しても問題はない。以下を追加すれば良い。

¨ 型構成子IO

¨ 構文return v

¨ 構文let x<-m in n

（v、m、nは項、xは変数）

¨ 型推論規則：

¨ 「松果体」

として、プログラムの作用を示す（Haskellのmainに当たる）IO型の値。

以上は型のない言語でも同様。ただコンパイル時の検査を省いて実行時の検査で置きかえる必要がある。

ただ、高階言語ならば一階の言語では構文を追加しなければならないような束縛が、構文の追加なしに可能。（例：ChurchのΠ(λx.A)）

monadの利用はHaskellのような高階言語のほうが楽だが、一階の論理型言語でも拡張すれば可能。詳細については今後の課題。

バック・トラック

論理型プログラミング言語へ入出力を追加するには最後の障害としてバック・トラック時の相互作用がある。試行は簡単に戻せるが、動作を戻すこと（undo）は簡単ではない。

関数型言語ではしばしば、可能な解のリスト（あるいは集合）としてモデル化される。言語がもしlazyであれば、挙動はまさにバック・トラックになる。（このようなリストの使い方はまさにmonadを利用する動機。）

構文解析は、バック・トラックの応用として論理型言語のプログラマが、またリストやmonadの応用として関数型言語のプログラマが関心を持っている。

課題

monadは相互作用の理解を助けるだけでなく、バック・トラックの理解助けるか？あるいは両者に関係があるか？

[1] 古い版のHaskellでは前節のDialogue型の役割を持つ型がAnswerと呼ばれていた。