このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

総称高階関数計算の練習：積モナドの乗法を書き下す

雑記／備忘

2007年5月のエントリー「ベックの法則と複合モナド」のコメント欄で、[1..100]>>=pen さんと次のようなやり取りがありました。

[1..100]>>=pen (2009/10/23 22:34)
el_flatten(elel) := e_map(l_flatten, e_flatten(e_map(combinations, elel)))
ではないですか。

m-hiyama (2009/10/24 14:19)
[1..100]>>=penさん、
んっ、また間違いをしでかしたかな？ 鼻水が止まったら見ておきます。

m-hiyama (2009/10/27 10:07)
どっちでも同じようですね、自然変換なので。

[1..100]>>=pen (2009/10/27 13:19)
e_map(combinations, elel) の結果は EELL になると思いますが
そこに l_flatten できますか？

m-hiyama (2009/10/28 08:16)
[1..100]>>=pen さん、
あっ、そうか。l_flattenじゃなくて、e_map(e_map(l_flatten))) か。ご指摘ありがとうございます。

古いエントリーを丁寧に読んでくれる人がいるのはありがたいことです。

さて、もともとの僕の記述は次のよう。

  • el_flatten(elel) := e_flatten(l_flatten(e_map(combinations, elel)))

これには間違い（抜け）があって、実際は（[追記]って、まーだ間違っているじゃん。直した。）[/追記]

  • el_flatten(elel) := e_flatten(e_map(e_map(l_flatten(e_map(combinations, elel)))))
    el_flatten(elel) := e_flatten(e_map(e_map(l_flatten), e_map(combinations, elel)))

です。ここで、マップ関数e_mapは、2引数と1引数（カリー化済み）の両方で使っています。

[1..100]>>=pen さんが提示されていた代替の定義：

  • el_flatten(elel) := e_map(l_flatten, e_flatten(e_map(combinations, elel)))

でも同じことです。

なんでこういう結果になるかを説明します。

内容：

まずは絵算で考えてみる

僕は、（ご存知の人もいるでしょうが^^;）記号的／等式的計算があんまり出来ないので、絵を描いて計算します。コミュニケーションの必要があれば、結果の絵を通常の記号的記法に書き下します。今回話題にしている等式は、計算結果ではなくて定義なのですが、次の絵で表現できます。

 L   E    L   E
｜    ＼／    ｜
｜    ／＼    ｜
 L   L   E    E
  ＼／   ＼ ／
   ・     ・
   ｜     ｜
   L      E

これは、横方向が左から右、縦方向は上から下の絵になっています。記号的記法でよく使われている反図式順（右から左）にあわせるなら次の図。

 E   L    E   L
｜    ＼／    ｜
｜    ／＼    ｜
 E   E   L    L
  ＼／   ＼ ／
   ・     ・
   ｜     ｜
   E      L

(L, μ, η)がリスト（List）モナド、(E, ν, ρ)が列挙（Enum）モナド、γがcombinationsの自然変換だとして、絵の脇に記号的表現を添えると次のようになります。

 E   L    E   L
｜    ＼／    ｜
｜    ／＼    ｜ … E*γ*L
 E   E   L    L
｜  ｜    ＼ ／
｜  ｜     ・ …… EE*μ
｜  ｜     ｜
 E   E     L
  ＼／     ｜
   ・      ｜ …… ν*L
   ｜      ｜
   E       L

[1..100]>>=pen さんが出していた定義は次です。

 E   L    E   L
｜    ＼／    ｜
｜    ／＼    ｜ … E*γ*L
 E   E   L    L
  ＼／   ｜   ｜
   ・    ｜   ｜ …… ν*LL
   ｜    ｜   ｜
   ｜     ＼ ／
   ｜      ・ …… E*μ
   ｜      ｜
   E       L

星印「*」は、反図式順のスター積（横結合）です。反図式順縦結合を「・」で表すと次の表記になります。

  • (ν*L)・(EE*μ)・(E*γ*L)
  • (E*μ)・(ν*LL)・(E*γ*L)

いちおうこれで、圏論の（割と標準的な）記法で絵を書き下したことになっています。これを、さらに具体的・露骨に書き下すには、若干の一般論が必要です。

反図式順記法による関手・自然変換の計算

僕自身は使ってないのですが、世間ではおそらく多数派を占めると思われる反図式順記法を紹介します。メジャーな記法を知ってないとマズイこともあるので。

Cを圏として、これから考える関手はすべてC上の自己関手だとします。F, G, H, K を関手、関手Fと関手Gのこの順の結合（合成）を GF と書きます（FGではない！）。X, YをCの対象、f:X→Y in C だとして、Ff:FX→FY のように書きます。GFX と書くと、対象Xに関手GFを適用した結果です。これはまた、対象FXに関手Gを適用した結果でもあります。

自然変換は、ギリシャ小文字α、βなどで表すことにして、α::F⇒G と書きます。この記法は、自然変換は次元が2の射（膜のようなもの）だという雰囲気を出したものです。自然変換αのX成分を αX と下付き添字で書きます。α::F⇒G ならば、αX:FX→GX ですね。

α::F⇒G と β::G⇒H の縦結合を β・α と書きます（反図式順なので、α・βではない！）。β・α::F⇒H、(β・α)X::FX→HX で、縦結合（Vertical Composition）の具体的定義は次のとおり。右辺の並置は射の反図式順結合です。

  • (β・α)X := βXαX ……[VC]

関手の結合と射の結合を、並置（演算子記号が空である二項演算）で表すことにより、記述は極端に簡潔になります。しかし、並置のオーバーロードは慣れないとすごく混乱します。注意してくださいね。

α::F⇒G, β::H⇒K として（βの仕様がすぐ上と変わったので注意）、関手と自然変換の反図式順横結合（スター積）は次で与えられます。これらの横結合の結果は自然変換です。

  • (β*F)X := βFX, (β*F)::GF⇒HF
  • (K*α)X := KαX, (K*α)::KF⇒KG

自然変換どおしの横結合（Horizontal Composition） β*α は、(K*α)・(β*F) または (β*G)・(H*α) で定義されます。(K*α)・(β*F) = (β*G)・(H*α) なので（練習問題）、どちらも同じになります。具体的な表示は次のとおり。

  • (β*α)X := KαXβFX ……[HC-1]
  • (β*α)X := βGXHαX ……[HC-2]

積モナドの乗法を書き下してみる

最初の状況に戻って、(L, μ, η), (E, ν, ρ), γのプロファイルを書き下すと：

  • L:C→C
  • μ::LL⇒L
  • E:C→C
  • ν::EE⇒E
  • γ::LE⇒EL

ηとρは使わないので省略。

問題の積モナド（複合モナド）ELの積τは次の式で与えられます。

  • τ := (ν*μ)・(E*γ*L) ::ELEL⇒EL

ここで、(ν*μ) = (ν*L)・(EE*μ) を使えば、

  • τ := (ν*L)・(EE*μ)・(E*γ*L)

一方、(ν*μ) = (E*μ)・(ν*LL) を使えば、

  • τ := (E*μ)・(ν*LL)・(E*γ*L)

です。

圏論と総称高階関数計算

ここで、もとになる圏Cの対象が型であり、射が関数である状況を考えます。圏論の概念と総称高階関数の概念のあいだの対応は次のようになります。

圏論 総称高階関数
対象 型
射 関数
域 引数（入力）の型
余域 戻り値（出力）の型
恒等 恒等総称関数
結合 関数結合
関手の対象パート 型構成子
関手の射パート 特別な高階関数
自然変換 特別な総称関数

表のなかの「特別な」とは、「一定の法則を満たす」という意味です。

X, Yなどは圏の対象（つまり型）、f, gなどは圏の射（つまり関数）だとします。圏論では、関手の対象パートと射パートに同じ記号を使い、FX, Ff などとしますが、総称高階関数計算では、対象パートが F<X>, 射パートは f_map(f) のような、一貫性のない記法が使われます。今さらしょうがないので伝統に従いますが、F<X> ではなくて、F X と書くことにします。例：List X, Enum X 。

自然変換は総称関数で表現されますが、自然変換αに対応する総称関数がaのとき、αのX成分は a[X] と書くことにします。ブラケット内が型パラメータです。ブラケットと型パラメータはしばしば省略されます。ここだけ、ほんとにここだけの話ですが、反図式順の関数結合は # を使って表します。関数結合も並置にすると、ちょっと辛すぎるので。

  • (g#f)(x) = g(f(x))

恒等を id[X] と書くと：

  • h#(g#f) = (h#g)#f
  • f#id[X] = f
  • id[Y]#f = f

などが成立します。

先ほどの縦結合／横結合の定義 [VC], [HC-1], [HC-2] の右辺を、# を使って書くと次のようです。

等式番号 右辺 # を使うと
VC βXαX b[X] # a[X]
HC-1 KαXβFX k_map(a[X]) # b[F X]
HC-2 βGXHαX b[G X] # h_map(a[X])

最後の計算

圏論の関手・自然変換の反図式順記法と、「ベックの法則と複合モナド」における総称高階関数の対応をまとめます。

反図式順圏論記法 総称高階関数記法
LX List X
Lf:LX→LY l_map(f):List X → List Y
μX:LLX→LX l_flatten[X]:List List X → List X
EX Enum X
Ef:EX→EY e_map(f):Enum X → Enum Y
νX:EEX→EX e_flatten[X]:Enum Enum X → Enum X
γX:LEX→ELX combinations[X]:List Enum X → Enum List X

さーて、これで必要な公式（計算法則）と素材はすべて出揃いました。次の定義を総称高階関数計算の記法に翻訳しましょう。

  • τ := (ν*L)・(EE*μ)・(E*γ*L)
  • τ := (E*μ)・(ν*LL)・(E*γ*L)

いや、これは宿題にしよう、っと。計算練習にやってみてください。解答はたぶん来週。