【訂正記事】（プログラミングの）モナドは何が嬉しいの？

はじめに

YouTubeでムーザルちゃんねるなるyoutuberの圏論解説動画が上がっているのを見つけた。モナドは何が嬉しいの？という話題が解説されていた。説明されているムーさんはワドラー論文を読んだようではあるけれど、解説が回りくどいように思った。

なぜモナドが嬉しいのか？という解説はあんまり見かけたことがない。なんでかというと（わかってみると簡単なのだが）話の構造がややこしいからだ。実際、自分も過去になんで嬉しいのかということを歴史的経緯を交えたかのように見せかけて解説してみたことがある。

ここで謝罪しますとこの記事の内容は間違いです。 モナドとモナド変換子の導入動機を混同していて、モナド変換子の導入の理由のようなところとモナドの導入の動機の部分が混在しているような記事になってしまっている。
というわけで、数年経て到達した何でモナドは嬉しいのか？ということを敷衍してみます。

最初に結論

モナドがなぜ嬉しいのか？というと、

• ①モナドによってインターフェースが統一されて（モジュール性が持たされて）表示的意味論の意味関数がきれいなるし汎用性が出るから。
• ②言語の機能である各フィーチャー（feature）を、型構築子の形で計算効果として統一的に定義できるようになるから。

全く聞いたこともないので嘘だと思われるかもしれないが、ワドラー論文は大体①のような趣旨の話である。また、②はMoggiの論文の言っていることであるが、説明するのが難しいので今回割愛。動画のようにプログラマー向けに説明するメリットとしては①である。

以下は、①を敷衍していく。

表示的意味論とは？

プログラミングと数学は直観的には似ているが、異なる活動である。しかし、「厳密に定義された概念を操作し、論理的な結論を導き出す」という点においては共通している。
プログラミングは戦後に誕生した歴史の浅い分野であり、長らくその正当性を担保する明確な土台を持たなかった。一方、数学は千年単位の歴史を持ち、厳格な証明によって高い信頼性を築き上げてきた学問である。
プログラミングには「基礎理論の強度に対する明確な根拠がない」という弱点があった。そこで、この不安定なプログラムの振る舞いに、信頼性の高い数学的対象（関数や集合など）を当てはめることで強固な根拠を与えようとするアプローチが生まれた。このような目的で構築された理論を 表示的意味論（denotational semantics） と呼ぶ。
この表示的意味論において、中心的役割を担うのが、プログラムのソースコードを抽象構文木として数学的対象に割り当てていく 意味関数（semantic function） である。プログラミング言語でいうとeval関数（ワドラー論文ではinterp関数）にあたる。

表示的意味論は1970年代の理論なので、プログラミング言語に実装されている特徴的機能（フィーチャー；feature）については、既に数学的対象に割り当てる意味関数の定義が知られている。例えば、ワドラーが論文で挙げたフィーチャーは以下のようなものである。

• 基本（フィーチャなし）
• 例外（error message）
• 状態（state）
• 出力（output）
• 非決定的選択（non-deterministic choice）
• ...

これら様々なフィーチャーを持つプログラミング言語の構文（AST）については、理論計算機科学的に数学的対象に割り当てる意味関数の定義（eval関数、interp関数など）が知られている。定義をそのまま書くのは冗長なのでシグネチャ（型付け）だけを書くと、
基本:eval_b :: Term -> Value
例外:eval_e :: Term -> (Value | Error) （値かエラーを返す）
状態:eval_s :: Term -> State -> (Value, State) （状態を受け取り、値と新状態を返す）
出力:eval_o :: Term -> (Value, Output) （値と出力ログを返す）
...
これらフィーチャのプログラムについては、それぞれ対応するシグネチャの異なる意味関数（eval_b,e,s,o）を適用させることで数学的対象にすることができる。これが、表示的意味論の成果であり、なんとプログラムを数学的対象として取り扱うことができ、プログラミングという活動は、 やろうとおもえば、 数学と言う活動に還元できるということが示されたのである。
ただし、ここに表示的意味論の最大の弱点（モジュール性の欠如）がある。見ればわかるように、 プログラムを数学的対象に対応させる意味関数（eval関数）がフィーチャーごとに違うシグネチャ（型）になってしまうのである。

シグネチャ（型）が変わるということは、例えば、単純な n :: int を引数として取り n+1 を返すプログラム succ であっても実現するフィーチャが異なるというだけで、ソースコードの取り回しの共通性が失われてしまうのである。
以下は、nを引数としてとり、n+1を返すsuccのフィーチャーごとの定義である。おんなじことをやっているのにフィーチャーが違うだけで全然違うコードを書かないということにストレスを感じる。
これが表示的意味論にはモジュール性が欠如していると言われるゆえんであった（以前の記事で微妙に勘違いしていた点）。

-- 【基本】（値だけが返ってくるので、そのまま1を足せる）
eval_b (Succ t) = 
    let n = eval_b t 
    in n + 1

-- 【例外】（エラーかもしれないので、case文で分岐する配管が必要）
eval_e (Succ t) = 
    case eval_e t of
        Error msg -> Error msg       -- エラーならそのまま素通りさせる
        Value n   -> Value (n + 1)   -- 成功時のみ1を足してValueで包み直す

-- 【状態】（状態 s0 を受け取り、s1 として引き回す配管が必要）
eval_s (Succ t) s0 = 
    let (n, s1) = eval_s t s0
    in (n + 1, s1)

-- 【出力】（出力されたログ out を捨てずに引き回す配管が必要）
eval_o (Succ t) = 
    let (n, out) = eval_o t
    in (n + 1, out)

モナドは何で嬉しいか？

この表示的意味論のモジュール性の欠如を解決するために導入されるのがモナド（monad）である。
ここまで書けばもう大体わかると思うが、モナドを既知とすれば、表示的意味論の意味関数（eval関数）は各フィーチャ毎に次のように書けるようになる。
基本:eval_b :: Term -> I Value
例外:eval_e :: Term -> Maybe Value
状態:eval_s :: Term -> State Value
出力:eval_o :: Term -> Output Value (Outputモナドの定義は知らないがあるとして)

つまり、シグネチャ（型）だけに着目すれば、
eval_f :: Term -> M Value
と書けるようになるのである。すると、フィーチャーごとに意味関数（eval関数）を分ける必要がなくなり、

eval :: Term -> M Value

と、表示的意味論の意味関数が非常にシンプルになる。これがモナドの効用である。
そしてこれから導かれる嬉しい点として、上記のsucc関数のフィーチャーごとの共通化である。モナドを用いて意味関数をシンプルにしたことで、フィーチャーごとの分岐が不要になり succ は、以下のように非常にシンプルかつ、フィーチャーごとに共通して使えるようになってしまう。これがモナドの嬉しい点①である

-- モナド化された eval 関数
eval (Succ t) = 
    eval t >>= \n -> return (n + 1)

-- （※ do 構文を使うとさらに分かりやすい）
eval (Succ t) = do
    n <- eval t
    return (n + 1)

概念図

再度結論

表示的意味論を踏まえないとモナドの利点は納得できない。