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

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

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

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

概要[編集]

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

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

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

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

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

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

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

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

計算の概念と計算効果(notions of computation and computational effects)[編集]

Moggi の理論の骨子は、『型 A の値(values of type A)』と『計算によって得られた型 A の値(computations of type A)』を明確に区別することにある[13]。すなわち、副作用、例外処理、非決定計算などの計算方式でその計算効果(computational effects)を伴いつつ計算によって得られた型 A の値は、型を引数にとる型構築子 T を型 A に適用した新たな型 T A の値として表現するのである(Moggiの原理)[14]

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

なお、このときこの型構築子 T を計算の概念(a notion of computation)と呼ぶ[16]

プログラムの概念とその合成に関する問題点(a notion of programs and the problem of composition)[編集]

計算の概念の導入により、引数を取りつつ計算効果を伴った上で計算した値を返すものであるプログラム(program)の概念は次のように特徴付けることができるようになる。

Moggi が(暗黙的に)主張するプログラムの概念
型 A の引数を取り T の計算効果を伴いつつ計算をした型 B の値を返すプログラム(program)とは、A → T B の型を持つものである[17]

このように特徴付けることによって計算効果を伴うプログラムとなんら計算効果を持たない単なる集合写像(関数)を分類することが可能となる。しかしながら、プログラムをこのように定式化すると大きな問題が発生することがわかる。すなわち、2つのプログラムの合成を単純に行うことができなくなってしまうのである

例えば、program1 :: A → T Bprogram2 :: B → T C が与えられたとき、その合成を行おうと思っても、型 B というデータの型としての共通性はあっても計算の概念の分だけ型に違いがあるため、実際にプログラムの合成を行うことはできない。

program2 :: B → T C × program1 :: A → T B (合成不可)

この致命的な問題点を解消するために導入されるのがクライスリトリプル(Kleisli triple)である。

直感的な記法となるが、クライスリトリプル(T,η, _*)が与えられれば、「_*」演算子の機能からprogram2* :: T B → T C となり

program2* . program1 :: A → T C (合成可能)

という形でプログラムの合成が可能となる。おおよそこのような理由から Moggi はクライスリ圏の射とプログラム(program)とは対応するものだとした[18]

関連項目[編集]

脚注[編集]

  1. ^ 佐伯(2001) p.11
  2. ^ 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)
  3. ^ 尾上(2006) p.306
  4. ^ つまり、Set もしくは Ens の普通の射ではない
  5. ^ Moggi(1989) p.17
  6. ^ Moggi(1989) p.17
    3.2.1 A justification for monads
    In order to justify the use of monads for modelling notions of computations we adopt the following intuitive understanding of programs: a program is a function from values to computations.
  7. ^ Moggi(1989) p.18
  8. ^ 計算効果(computational effects)と呼ばれる。Filinski(1994)勝股(2011)
  9. ^ メタ言語としては、プラトン主義的にしか存在し得ない完全な言語としての数学でなければならないかのような説明が一部でされることもあるが、そのような必然性は特に無く、対象言語を意味づけるに十分な形式言語(プログラミング言語)であればよい。
  10. ^ Liang,Hudak pp.1-2
  11. ^ このモジュールのことをモナド(monad)、計算(computation)などと呼ぶこともある。
  12. ^ Wadler(1992), Espinosa(1995)
  13. ^ 参照
    1 A categorical semantics of computations
    The basic idea behind the categorical semantics below is that, in order to interpret a programming language in a category C, we distinguish the object A of values (of type A) from the object TA of computations (of type A), and take as denotations of programs (of type A) the elements of TA. In particular, we identify the type A with the object of values (of type A) and obtain the object of computations (of type A) by applying an unary type-constructor T to A. We call T a notion of computation, since it abstracts away from the type of values computations may produce. There are many choices for TA corresponding to different notions of computations.
    Moggi(1991) pp.2-3
  14. ^ なお、Moggi はプログラミング言語のML(MetaLanguage)のような型システムを持つ言語を前提に理論を展開している。
  15. ^ Filinski(1994) p.447
  16. ^ Moggi(1991) p.3
  17. ^ これは例えば入出力の効果をもたらす計算(入出力の計算効果)では、一例として、文字列 String 型の値を取り単位型 () を返し入出力の計算効果をもたらすプログラム putStrLn の型は(その計算効果を表す型名を T ではなく IO とすれば)
    putStrLn :: String -> IO ()
    となることを意味する。すなわち、
    putStrLnプログラム:文字列の値 -> 入出力(IO)"計算した" 単位型の値
    と把握されるものであるということである。 なお、例えばプログラミング言語のHaskellにおいては、他にも、例外処理の計算効果であれば Error、継続(continuation)の計算効果であれば Cont などの型名が与えられている。
  18. ^ Moggi(1989) pp.17-18

参考文献[編集]

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