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

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

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

［参照用 記事］

僕は嫌いなのだが、バイダイレクショナルな自然変換計算はこうする

雑記／備忘

モナドはどこに棲んでいるのか？ というと、Cを圏としてその自己関手の圏 End(C) のなかにモナドがいるわけです。D = End(C) と置けば、Dがモナドを定義する舞台となります。

(F, η, μ) がモナドであるとき、F∈|D|、η:I→F in D、μ:FF→F in D となります。D = End(C) は関手圏なので、Dの対象とは関手であり、Dの射とは自然変換です。IはCの恒等関手（I = IdC）、FFはFを2回繰り返した関手です。自然変換を記号「::」と「⇒」を使って表すなら： F:C→C、η::I⇒F:C→C、μ::FF⇒I:C→C となります。

モナドに関する計算とは、D内で計算することであり、つまりは自然変換の計算です。モナドを理解する／作る立場（「再びモナドへ」参照）では、自然変換の計算ができないとオハナシになりません。

ところが、自然変換の計算は面倒くさい／鬱陶しい。その理由のひとつは、「左から右」と「右から左」が混じったバイダイレクショナルな点だと思います。僕にとっては、バイダイレクショナルな記法はものすごいストレスです。それで、左から右の一方向の図式順記法とか、そもそもテキスト記号をまったく使わない絵算＜えざん／えさん＞とかを使っています。

図式順記法とか絵算を使ってモナド関係の説明をしたエントリーは：

絵算（ストリング図）は一般的にかなり使われていますが、徹底して左から右の図式順記法はあんまり使われていません（ユーザーは僕だけかも ^^;）。致し方ないので、バイダイレクショナルな記法を説明します。しかし、次の点は譲れないです。

  1. 射の結合（composition）は、左から右に f;g と書く。気になる人は、f;g が出てきたら g・f に置き換えてください。
  2. 自然変換αのA成分は、αA と下付き添字が普通です。が、テキストエディタで書くときに負担なので、ブラケットによるインデックス記法 α[A] を採用する。
  3. Aの恒等射 idA も下付きなので、id[A] とする。混乱の心配がなければ、id[A] を単にAとも書く。

僕が（個人的に）使っている図式順記法では、

  • 射の結合 f;g
  • 関手の結合 F;;G
  • 自然変換の縦結合 α|β

と区別するのですが、バイダイレクショナルな記法では、

  • 射の結合 f;g （気になるなら g・f）
  • 関手の結合 GF （単に併置する）
  • 自然変換の縦結合 α;β （射の結合と同じ）
  • 自然変換の横結合 βα （関手の結合と同じ）

関手の結合に関しては妥協して GF と「右から左」とします。これだと、GF(A) = G(F(A)) となる点は便利です。自然変換では、縦結合が左から右、横結合は右から左と、ほんとに両方向混在となります（ウゲーッ）。

今定義したバイダイレクショナルな記法で計算を進めるときの注意点：

  1. 関手Fに対する恒等自然変換を ιF とする。「ι」は小文字のイオタ。
  2. だが、ιF はほとんど使わずFで代用する。恒等射と対象を混同する流儀。
  3. (ιF)[A] = id[F(A)] と展開できるので、F[A] = id[F(A)] としてよい。
  4. Fμ のように、関手と自然変換が併置されたら、ιFμ だと思う。
  5. (α;β)[A] = α[A];β[A] と、ブラケットインデックスは縦結合に関して分配できる。
  6. (βα)[A] を展開する公式はあるが、複雑だしあまり使わないので憶えなくてよい。
  7. (Gα)[A] = G(α[A]) と (βF)[A] = β[F(A)] はよく使う。（これは憶えやすいでしょ。）
  8. (βα)[A] を展開する必要があるときは、α::F⇒G、β::H⇒K に関する βα = (Hα);(βG) という公式（交替律）を使う。
  9. バイダイレクショナル記法が耐えがたいと思ったら、図式順記法の採用をご検討ください（宣伝）。

これらの計算法を使うと、次のような自然変換の成分を取る計算ができます。

  • (Fμ;μ)[A] = (Fμ)[A];μ[A] = F(μ[A]);μ[A]
  • (μF;μ)[A] = (μF)[A];μ[A] = μ[F(A)];μ[A]

モナドの結合法則は、自然変換のレベルでは Fμ;μ = μF;μ なので、成分を取れば ∀A.( F(μ[A]);μ[A] = μ[F(A)];μ[A] ) と表現できます。この等式の左右は、FFF(A)→F(A) という射なので、FFF(A) が集合だとすれば、x∈FFF(A) に関して、

  • (F(μ[A]);μ[A])(x) = (μ[F(A)];μ[A])(x)

バイダイレクショナルである点を考慮しながら（ストレスに耐えながら）変形すると、

  • μ[A](F(μ[A])(x)) = μ[A](μ[F(A)](x))

ふえー、ストレスで疲れる。

実例としてListモナドを考えて、次のように具体化しましょう。

  • 対象の関手による値 F(A) → 型構成子 List<A>
  • 射の関手による値 F(f) → 高階関数 List.map{f}
  • 自然変換の成分 → 総称関数 List.flatten<A>

型パラメータは山形括弧、関数引数は波括弧で囲むことにします。すると、モナドの結合律をListモナドに関して書き下した形は、

  • List.flatten<A>(List.map{List.flatten<A>}(lislislis)) = List.flatten<A>(List.flatten<List<A>>(lislislis))

これは、「僕が使っている計算法：絵算と図式順記法」でも出した例です。

と、まー、こんな感じで計算を進めます。記号計算だけでは辛いので、全体の様子を確認するには絵算（ストリング図）を併用するのがいいでしょう。