Haskellの二重コロン「::」とバインド記号「>>=」の説明

圏論はある程度知っているけど、Haskellの記号との対応がよく分からない人のための説明です。

内容：

二重コロン

Haskell風構文で f::A -> B と書かれていたら、二重コロンは単一コロンにして f:A → B と解釈すればいい -- と、そういう説明もアリでしょう。実際、「蒸し返し： アドホック多相 vs パラメトリック多相」で僕はそう説明しています。

上記のような解釈と翻訳「二重コロン は 単一コロン」で、だいたい問題はないですし、精神衛生上も良いと思います。が、もう少し精密な話が必要なことがたまにあります。そのときは、f::A -> B を次のように解釈します。

• f:1 → [A, B] in C

ここで、Cはデカルト閉圏で、1は終対象、[-, -] は内部ホム〈指数〉です。

以下、精密化した解釈の説明をしますが、とりあえず、Cは集合圏の部分圏になっていると仮定します。

f::A -> B の二重コロンを集合の所属関係に置き換えると：

• f∈A -> B

丸括弧を付けて分かりやすくすると：

• f∈(A -> B)

(A -> B) が何かというと、集合Aから集合Bへの関数〈写像〉の集合です*1。圏論で（比較的）よく使われる記法では、関数の集合（より一般に内部ホム）は [A, B] ですから、

• f∈[A, B]

です。これが二重コロンの解釈です。

もっと複雑な例 f::(A -> B) -> C -> D を考えてみましょう。まずは二重コロンを所属記号に置き換えて丸括弧を足すと：

• f∈(​(A -> B) -> (C -> D))

関数の集合を表すブラケットに直せば：

• f∈[​[A, B], [C, D]]

一般に、集合Xの要素と、その要素をポイントする写像 1 → X は1：1に対応するので、f∈[A, B] は f:1 → [A, B] と考えてもかまいません。集合圏の部分圏では要素が使えるので、f:1 → [A, B] としても特に嬉しくないですが、要素概念を持たないデカルト閉圏Cでも次のプロファイル宣言は意味を持ちます。

• f:1 → [A, B] in C

もうひとつの射

• x:1 → A in C

があると、評価射 ev_A,B:[A, B]×A → B により、

• ev_A,B<f, x>:1 → B in C

が作れます（<-, -> はデカルトペア*2）。この ev_A,B<f, x> を、Haskellでは単に f x と書きます。単なる併置で表される評価演算がすべての基礎になります。

バインド記号

モナドの表現として、'>>='という記号が使われます。「バインド」と呼ばれるこの記号は、「クライスリ拡張を表すに過ぎない」とも言えます（後述）が、プログラマーのメンタルモデルはクライスリ拡張とちょっと違うのかも知れません。

僕がそう思ったのは、'>>='をじょうごに比喩した絵・説明を見たからです。

*3

なるほどなー。確かに'>>='はじょうごに形が似てます。m >>= f と書いたとき、そのままではfに入りにくいmを、じょうご'>>='を使ってfに注ぎ入れる感じらしいです。面白くて印象的な比喩です。

モナドの定義の仕方はモノイド・スタイル〈代数スタイル〉と拡張スタイルがあります。モノイド・スタイルのモナドを (F, μ, η) 、拡張スタイルのモナドを (T, η, (-)^#) と書いたとき*4、与えられたモノイド・スタイルのモナドから拡張スタイルのモナドを定義するには次のようにします。

• T := F_obj （F_obj は、関手Fの対象パート）
• η := η （同じ）
• For f:X → T(Y), f^# := F(f);μ_Y

先に拡張スタイルのモナドがあるとき、モノイド・スタイルのモナドを定義することもできます。このへんのことは、古い記事に書いています。

• モナドの定義とか （2006年）
• モナドにおける「拡張」とは何なのか？ 色々と計算してみる （2013年）

モナドのクライスリ圏については、今年（2020年）の夏の記事：

• モナド、クライスリ圏、随伴 の落ち穂拾い

2006年の記事のコメント欄で、酒井さんに教えていただいたことですが、>>= f または f =<< は f^# とまったく同義だとみなせます。つまり、(f =<<) x は f^#(x) のことであり、'>>=' は同じことを逆順で書く記号です。

しかし、こう言い切ってしまうと、じょうごのモデルとの繋がりが薄くなり、なぜ「逆順で書く」のかも分かりません。次節で、ここらへんを少し詮索します。

適用と結合

バインド記号以外は、Haskell構文ではなくて一般的な記法を使います。集合圏の部分圏Cのなかで考えることにして、適用（引数を渡す、評価する）と結合（関数の合成）の記号は次のように決めましょう。

	反図式順	図式順
適用	f(x)	x.f
結合	gf	f;g

適用と結合のあいだの関係で、次は基本的です。

• 反図式順： (gf)(x) = g(f(x))
• 図式順： x.(f;g) = x.f.g

より一般には：

• 反図式順： (f_n ... f₂f₁)(x) = f_n(... (f₂(f₁(x)))...)
• 図式順： x.(f₁;f₂; ... ;f_n) = x.f₁.f₂. ... .f_n

適用を表すドットは左結合的な演算子だとして括弧を省略しています。こうして見ると、図式順記法が簡潔で自然な気がしますよね。オブジェクト指向言語だとメソッドチェーンと呼んで、この形を好む人もけっこういます。僕も図式順記法が好きです。ここから先は、主に図式順記法を使います。

圏C上のモナド (T, η, (-)^#) があると、モナドのクライスリ圏を構成できます。クライスリ圏の結合〈クライスリ結合〉の図式順記号を';;'で表すことにします。

Haskellのバインド記号'>>='は、いわば“クライスリ適用”*5の図式順記号になっています。先の表を拡張してみると：

	反図式順	図式順
適用	f(x)	x.f
結合	gf	f;g
クライスリ適用	f=<<x	x>>=f
クライスリ結合	(使わない)	f;;g

通常の（Cの）適用／結合とモナドの構成素を使って、クライスリ適用／クライスリ結合を定義できます。

• x>>=f := x.f^#
• f;;g := f;g^#

クライスリ適用とクライスリ結合のあいだの関係は次のようです。

• x>>=(f;;g) = x>>=f>>=g

次の計算で示せます。拡張スタイルのモナド法則*6を使います。

  x>>=(f;;g)
// クライスリ適用の定義
= x.(f;;g)#
// クライスリ結合の定義
= x.(f;g#)#
// 拡張スタイルのモナド法則から
= x.(f#;g#)
// 通常の適用と結合の関係から
= x.f#.g#
// 左結合的演算子だから
= (x.f#).g#
// クライスリ適用の定義
= (x>>=f)>>=g
// 左結合的演算子だから
= x>>=f>>=g

通常の適用／結合の場合と同じように次も成立します。

• x>>=(f₁;;f₂;; ... ;;f_n) = x>>=f₁>>=f₂>>= ... >>=f_n

';;'も'>>='も左から右への方向なので、手続き型プログラミング言語の順次実行のように読めます。モナドが副作用を表現する場合などは、手続き的順次実行のメンタルモデルは悪いものではありません。順次実行であれば、左から右、上から下が自然な記述方向であり、右から左、下から上は辛い。おそらく（僕の憶測ですが）、そんな理由で左から右へ読める記号'>>='が採用されたのでしょう。

これで、「何であんな記号なんだろう」という疑問は解消したでしょうか。

Haskellにおけるバインドのプロファイルは次のようです。

• (>>=) :: m a -> (a -> m b) -> m b

最初の節で説明した方法で一般的記法に翻訳すると：

• (>>=) ∈ [ T(A), [ [A, T(B)], T(B) ] ]

カリー化／反カリー化と直積の対称性で変形すると、

[ T(A), [ [A, T(B)], T(B) ] ]
// 反カリー化
[ T(A)×[A, T(B)], T(B) ]
// 直積の対称性
[ [A, T(B)]×T(A), T(B) ]
// カリー化
[ [A, T(B)], [T(A), T(B)] ]

つまり、(>>=) ∈ [ [A, T(B)], [T(A), T(B)] ] であったとしても事実上同じことです。内部ホム〈指数〉から外部ホムに移れば*7：

• (>>=):C(A, T(B)) → C(T(A), T(B)) in Set

と解釈できます。これは、域がAである射を、域がT(A)である射に“拡張”しています。「左から右へと読めるクライスリ適用」にすると、(>>=):T(A)×C(A, T(B)) → T(B) in Set ですね。

*1:すべての関数の集合である必要はありません。（A -> B)⊆Set(A, B) ならいいです。

*2:f:X → A, g:X → B に対して、デカルトペア <f, g> は X → A×B という射です。

*3:画像： https://www.monotaro.com/p/3578/6974/

*4:クライスリ拡張は右肩に星印で表すことが多いですが、星印はあまりに多用されるのでナンバー記号にします。

*5:「クライスリ適用」という言葉は聞いたことがないです（思いつきです）が、バインド記号の説明にはピッタリなのではないかと思います。

*6:拡張スタイルのモナド法則は、(1) η_X;f^# = f (2) (η_X)^# = id_T(X) (3) (f;g^#)^# = f^#;g^# の3つの等式的法則です。それぞれ、モノイド・スタイルの単位律（左右の別は書き方に依存する）、結合律に対応します。

*7:「何で移れるんだ？」「どうやって移るんだ？」という疑問はあるでしょうが、割愛。