日々の流転

λ. そうだ、レコンキスタにいこう

笑った。

λ. 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: P²(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: Y^X×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 でも読めばよいのではないかと。