モナド (プログラミング)

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索

計算機科学におけるモナド: Monad)とは、計算機科学者のEugenio Moggiによって提案されたモジュール性を持たせた表示的意味論の枠組みを言う。プログラムとはクライスリ圏の射である(a program is an arrow of a Kleisli category)、という要請[1]から合成規則としてクライスリトリプル(Kleisli triple)というモナドと等価なものが用いられる。型システムへの適用であるプログラミング言語Haskellで用いられるものがよく知られている。

モナドの名称は、圏論モナド(モノイド+トライアド)に基づく。なお、圏論のモナドはライプニッツモナド(単子論)から命名された。

概要[編集]

"プログラム"の圏とクライスリ圏(categories of "programs" and Kleisli categories)[編集]

プログラミングの教則として、引数と返り値をもつことからプログラム(program)とは数学の関数、すなわち集合写像(mapping)であると教えられることがある。
しかしながらこの喩えは

  • 入出力等をもたらすプログラム
  • 例外を返すプログラム
  • 引数に対して値を返さない(停止しない)プログラム
  • 同じ引数でも返り値が異なる可能性のあるプログラム

などを説明することができない。つまり、プログラムは集合写像ではない(a program is NOT a mapping)[2]
プログラム(program)の数学的モデルを見つけ出す過程において、Moggi は圏論と表示的意味論の観点からプログラムは圏の射、型は圏の対象とみなすことができ、さらに直感的解釈として、関数が値を取り値を返すものであるのに対しプログラムが値を取り計算した 値を返す、すなわち引数の型と返り値の型の間にはなにか違いがあり単純な射の合成ができない、と考えた。

集合写像(関数):値 →       値
プログラム   :値 → "計算した" 値

Moggi はこのような射としてのプログラムの数学的モデルとしてクライスリ圏(Kleisli category)の射が妥当であると主張し実際に副作用、例外処理、非決定計算などの効果[3]をうまくクライスリ圏の枠組みで統一的に定式化できることを示した。さらにプログラムの直感的解釈として返り値が"計算した 値"であると考えられることから、強モナド(strong monad)が計算のモデル(computational model)になるという主張を行った。
そういった壮大な背景をもつ理論であるが、実用上重要であるのは『引数と返り値の型がデータとして同一であっても合成することができず、クライスリトリプルに由来した合成規則を用いなくてはならない』という点である。

モジュール性を持たせた表示的意味論(modular denotational semantics)[編集]

対象言語の各項の意味をその対象言語を語るメタ言語[4]の値に割り当てる表示的意味論はプログラミング言語の理論の中でも重要な手法の一つであるが、伝統的な表示的意味論は言語機能のモジュール性と拡張性が欠如しており、実際の実装及び実装したプログラミング言語の機能追加を行う際に既存コードの大幅な修正・設計の大幅なやり直しなどの困難をもたらす。Moggi のプログラムをクライスリ圏の射とみなすモナドの理論は、言語の一つの特徴的機能を自由に組合せ可能な一つのモジュールとする実装方式[5]を与え、分割統治不可能であった言語の実装を分割統治可能なものにする。

計算効果(computational effects)[編集]

副作用、例外処理、非決定計算などの計算(computations)の効果、計算効果(computational effects)、は次の原理に基づいて解釈される。

Moggi の原理(Moggi's principle)[6]
型 α の計算(computations)は、型 T α の値に対応する
(Computations of type α correspond to values of type T α.)

これは例えば入出力の効果をもたらす計算(入出力の計算効果)では、一例として、文字列 String 型の値を取り単位型 () を返し入出力の計算効果をもたらすプログラム putStrLn の型は(その計算効果を表す型名を T ではなく IO とすれば)

putStrLn :: String -> IO ()

となることを意味する[7][8]

関連項目[編集]

脚注[編集]

  1. ^ Moggi(1991) p.3
    In order to justify the axioms for a Kleisli triple we have first to introduce a category CT whose morphisms correspond to programs.
    ※ここで圏 CT はクライスリ圏(定義1.3)
    蓮尾(2011)
  2. ^ つまり、Set もしくは Ens の普通の射ではない
  3. ^ 計算効果(computational effects)と呼ばれる。Filinski(1994)勝股(2011)
  4. ^ メタ言語としては、プラトン主義的にしか存在し得ない完全な言語としての数学でなければならないかのような説明が一部でされることもあるが、そのような必然性は特に無く、対象言語を意味づけるに十分な形式言語(プログラミング言語)であればよい。
  5. ^ このモジュールのことをモナド(monad)、計算(computation)などと呼ぶこともある。
  6. ^ Filinski(1994) p.447
  7. ^ すなわち、
    putStrLnプログラム:文字列の値 -> 入出力(IO)"計算した" 単位型の値
    と把握されるものであるということである。
  8. ^ 例えばプログラミング言語のHaskellにおいては、他にも、例外処理の計算効果であれば Error、継続(continuation)の計算効果であれば Cont などの型名が与えられている。

参考文献[編集]

第5章3節『関数とはなにか』において、圏Set(もしくは Ens) の普通の射に計算(computation)概念は全く含まれていないことが確認できる。
モナドを用いたモジュラーな意味論を採用することでレゴブロックを組み立てるように言語を組み立てることができることを実証した。