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

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

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

モナドの名称は、圏論のモナド（モノイド＋トライアド）に基づいており、ライプニッツのモナド（単子論）とは無関係である。

目次

概要 [編集]

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

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

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

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

集合写像（関数）：値　→　　　　　　　値
プログラム　　　：値　→　"計算した"　値

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

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

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

関連項目 [編集]

脚注 [編集]

  1. ^ つまり、Set もしくは Ens の普通の射ではない。
  2. ^ メタ言語としては、プラトン主義的にしか存在し得ない完全な言語としての数学でなければならないかのような説明が一部でされることもあるが、そのような必然性は特に無く、対象言語を意味づけるに十分な形式言語（プログラミング言語）であればよい。
  3. ^ このモジュールのことをモナド（monad）、計算（computation）などと呼ぶこともある。

参考文献 [編集]

第５章３節『関数とはなにか』において、圏Set（もしくは Ens） の普通の射に計算（computation）概念は全く含まれていないことが確認できる。
モナドを用いたモジュラーな意味論を採用することでレゴブロックを組み立てるように言語を組み立てることができることを実証した。
「http://ja.wikipedia.org/w/index.php?title=モナド_(プログラミング)&oldid=47420735」から取得