トップ «前の日記(2003-11-25) 最新 次の日記(2003-11-28)» 月表示 編集

日々の流転


2003-11-27 [長年日記]

λ. HaskellのMonad

Haskellのモナドの話になって、原さんは「私にわからんのは(Haskellが)おかしい」と言っていた。原さんにわからないなら、私にわかるわけがないな。

原さんがわからないってのは、ちょっと信じられないです。Monadの数学的定義を知っているならば、Haskellのは単に「各種の計算体系のモデルを、適当な strong monad の Kleisli category として作れる」ということに過ぎないと思うので。

例えば、Computational lambda-calculus and monadsにも載っている例をいくつか取り上げると……

(例1) 非決定性計算
  • T: C→C
    T(X)=℘(X) (℘はべき集合関手)
  • ηA: A→℘(A)
    ηA(x) = {x}
  • μA: P2(A)→℘(A)
    μA(S) = ⋃S

で定義される Monad (T,η,μ) の Kleisli category は非決定性計算のモデルと考えられる。非決定的な関数 A→B は決定的な関数 A→℘(B) として解釈される。

(ちなみに、amb演算子 amb: P(A)→A も決定的な関数 Id℘(A): ℘(A)→℘(A) で解釈できる)

(例2) 副作用
  • T: C→C
    T(X)=(X×State)State
  • ηA: A→(A×State)State
    ηA(x) = λs.<x,s>
  • μA: ((A×State)State×State)State→(A×State)State
    μA(x) = λs. eval(x(s)) (ただし eval: YX×X →Y)

で定義される Monad (T,η,μ) の Kleisli category は、(State型の状態に対する)副作用をもつ計算体系のモデルと考えられる。副作用をもつ関数 A→B は副作用を持たない関数 A→(B×State)State として解釈される。(A→(B×State)State は A×State→B×State をカリー化した型になってる)

【2006-04-13 追記】このエントリの記述について、[教えて!goo] モナド、Kleisli triple で質問されているみたい。 とりあえず意味を理解するには http://www.ipsj.or.jp/07editj/promenade/4703.pdf でも読めばよいのではないかと。

本日のツッコミ(全4件) [ツッコミを入れる]
ψ はら (2003-12-03 19:10)

どひゃー、読者が著者に突っ込まれるとは!<br>モナドの定義もわかるし、例がモナドになることの証明もできるんだけど、それが「計算体系のモデル」になることと、Haskell の >>= とどう関係してるかということがぴんと来ないんですよ。

ψ はら (2003-12-04 02:31)

あ、ちょっと分かった気がします。つまり Haskell のモナドは、モナドそのものではなく、(m, return, <<=) が Kleisli triple なんだ。よって<br><br>関手: (a -> b) -> (m a -> m b)<br> : \f -> (>>= (return . f))<br>乗法: m (m a) -> m a<br> : \x -> (x >>= (\y -> y))<br>単位: a -> ma<br> : m のデータ構築子<br><br>と定義して初めて数学的なモナドになる、、、のかな?

ψ さかい (2003-12-04 14:28)

そうです。<br>でも単位はmのデータ構築子じゃなくてreturnですよ。

ψ はら (2003-12-04 16:26)

そですね。(^^; でもやっとすっきりしました。ありがとう。