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

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

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

［参照用 記事］

絵算で見る、拡張スタイルのモナドとモノイド・スタイルのモナド

雑記／備忘

「Haskellの二重コロン「::」とバインド記号「>>=」の説明」で、拡張スタイルのモナドとモノイド・スタイルのモナドの話題が出ました。この話題はだいぶ昔に書いたことがありますが、絵算の応用として「拡張スタイル ←→ モノイド・スタイル」の相互変換をしてみます。

内容：

絵算の技法

モナドの二種類の定義を行ったり来たりする、つまり「拡張スタイルのモナド ←→ モノイド・スタイルのモナド」の相互変換をするために、次の技法を使いましょう。

  1. 圏の圏における絵算〈{graphical | pictorial | diagrammatic} {calculation | computation}〉
  2. 図式順記法〈diagrammatic order notation〉
  3. 射の格上げ〈bump up | promotion〉
  4. オペレーターボックス〈operator box〉

これらの技法を使う実例としてモナドの定義を扱う、と言ったほうがいいかも知れません。この記事は絵算の練習問題と捉えましょう。

絵算、図式順記法、格上げについては、次の記事と、そこから参照されている記事を見てください。

オペレーターボックスは、関手ボックスを、関手とは限らないオペレーター〈コンビネータ〉にまで拡大して利用する手法です。アイディアは関手ボックスと同じです。関手ボックスについては、「絵算のススメ 2015 年末版 // 絵算のテクニック もっと：等号ノード、関手ボックス」で触れています（触れてるだけだな）。ストライプ図は関手ボックスの変種です -- 「モノイド関手／ラックス・モノイド関手とその実例 // マッカーディのストライプ図」に説明があります。

射のプロファイルとin記法もよく使うので、必要があれば次も参照してください。

モノイド・スタイルのモナドの定義

テキスト記法は図式順記法を使うので、必要があれば演算子記号の一覧表を確認してください。

モノイド・スタイルのモナドを (F, μ, η)/C と書いたとき、基礎となる圏Cと3つの構成素は（必ずしも小さくない）圏の圏CAT内で次のプロファイルを持ちます。

  1. C in CAT （基礎圏）
  2. F:C → C in CAT （台関手）
  3. μ::F＊F ⇒ F:C → C in CAT （乗法）
  4. η::C^ ⇒ F:C → C in CAT （単位）（C^ は IdC と同じ）

モノイド・スタイルのモナド法則は次の等式で書けます。

  1. assoc ::: μ＊F^ ; μ = F^＊μ ; μ :: F＊F＊F ⇒ F : C → C in CAT （結合律）
  2. lunit ::: η＊F^ ; μ = F :: C^＊F ⇒ F : C → C in CAT （左単位律）
  3. runit ::: F^＊η ; μ = F :: F＊C^ ⇒ F : C → C in CAT （右単位律）

左単位律、右単位律における左右の別は書き方・描き方に依存するので左右に絶対的意味はありません。

CATは2-圏〈厳密2-圏〉ですが、等式は2-圏の3-射です*1。次のように書いたほうが3-射であることが伝わるでしょう。

  • assoc ::: μ＊F^ ; μ ≡> F^＊μ ; μ :: F＊F＊F ⇒ F : C → C in CAT

等式＝3-射は、ストリング図の変形として表現されます。モナド法則（結合律と2つの単位律）がどのような変形かは後で出てくるので、絵は省略します。

拡張スタイルのモナドの定義

拡張スタイルのモナドを (T, η, (-)#)/C とします。Cは圏ですが、Tは関手ではないし、ηの自然性も仮定せず、(-)# は関手でも自然変換でもないオペレーターです。(-)# をExtとも書くことにします。T, η, Ext は、次のような形で定義します。

  1. For A∈|C|, T(A) in C （対象構成子*2）
  2. For A∈|C|, ηA:A → T(A) in C （単位）
  3. For A, B∈|C|, ExtA,B:C(A, T(B)) → C(T(A), T(B)) in Set （拡張オペレーター）

次の方針で図示します。描画方向は、縦結合が上から下、横結合が左から右です。

  1. T(A) を図式順で A.T と書いて、A T の順で横に並んだ2本のワイヤーにする。
  2. ηA を図式順で A.ηと書いて、A η の順で横に並んだワイヤーとノードにする。ηのノード形状は三角（'△'）にする。
  3. f;A → T(B) に対する f# = ExtA,B(f) は、fを表すノード＆ワイヤーを囲むボックスで描く。

上段の絵では、エリア、ワイヤー、ノードにすべてラベルを付けています。

  1. エリア☆は、自明圏（単一対象と恒等射だけの圏）
  2. エリアCは、基礎圏
  3. ワイヤーAは、Cの対象の格上げ
  4. ワイヤーTは、対象構成子〈型構成子〉（関手ではないが、関手の対象パートになる）
  5. ノードηは、左に対象（の格上げ）があると射（の格上げ）になる射の族
  6. ノードfは、Cの射 f:A → B in C の格上げ
  7. 箱は、Extを表すオペレーターボックス

下段の絵では、ラベルがほぼ省略されています。実際の計算では、この程度の省略が行われます。

注意すべきは、この描画法は「正面からではなくて横から見て描いている」ことです。横が何を意味するかというと、「絵算をはじめた人への注意 // 3次元ビュー」のBさんからの視点です。通常の関手ボックスやストライプ図は正面（Aさん）から見ての絵です。

さて、拡張スタイルのモナド法則は次の等式で書けます。A, B, C は基礎圏Cの対象で、図式順記法を使います。

  1. A.η ; (f:A → B.T)# = (f:A → B.T)
  2. (A.η:A → A.T)# = (A.T)^ （(A.T)^ は idA.T と同じ）
  3. [(f:A → B.T);(g:B → C.T)#]# = (f:A → B.T)#;(g:B → C.T)#

それぞれの等式は次のように図示されます。格上げを使って、絵はCAT内で解釈します。

絵の印象から、3つの等式をそれぞれ、

  1. 外単位律〈outer unit law〉
  2. 内単位律〈inner unit law〉
  3. 入れ子律〈nest law〉

と呼ぶことにします。

  1. ボックスの右上に接合された単位（△）はボックスごと消せる。
  2. ボックスに入れられた単位（△）はボックスごと消せる。
  3. ボックスの入れ子を、並んだ2個のボックスに変形できる。

逆向きの変形もできます。

モノイド・スタイルから拡張スタイルへ

モノイド・スタイルのモナド (F, μ, η)/C の構成素は次の方針で図示します。

  1. F:C → C はワイヤーで描く。
  2. μ::F＊F ⇒ F は黒丸（●）で描く。
  3. η::C^ ⇒ F は三角（△）で描く。

与えられたモノイド・スタイルのモナド (F, μ, η)/C から、拡張スタイルのモナド (T, η, (-)#)/C を構成するには、次のように定義します。

  1. A.T := A.F
  2. A.η := A.η
  3. (f:A → B.T)# := (f:A → B.T).F ; B.μ

この定義のもとで、拡張スタイルのモナド法則（外単位律、内単位律、入れ子律）を示せばいいのですが、図の変形として比較的容易に示せます。

赤で描いているのは、モノイド・スタイルのモナドの右単位律、左単位律、結合律による変形です。（結合律による変形に、交替律によるノードの移動も混じってしまってますね。絵算あるある*3。）

拡張スタイルからモノイド・スタイルへ 素材の準備

与えられた拡張スタイルのモナド (T, η, (-)#)/C から、モノイド・スタイルのモナド (F, μ, η)/C を構成するには、まずFを次のように定義します。

  • A.F := A.T （Fの対象パート）
  • (f:A → B).F := [(f:A → B) ; B.η]# （Fの射パート）

Fの射パートは、実線のワイヤーではなくて波線（グニグニ）にします*4。対象パートは F = T なので実線のままです。

定義したFが関手であることは証明する必要があります。関手性は次のとおりです。

  • (f;g).F = f.F ; g.F （結合の保存）
  • A^.F = (A.F)^ （恒等射の保存）

絵算で示しましょう。

絵の変形に使っているのは、F（波線）の定義、入れ子律、外単位律、内単位律です。

ηはそのまま使いますが、拡張スタイルのηでは自然性を仮定してなかったので、自然性の証明が必要です。（下の図式で、あえて対象にはT、射にはFを使っています。）

\require{AMScd} \begin{CD} A @>{A.\eta}>> A.T \\ @V{f}VV @VV{f.F}V \\ B @>{B.\eta}>> B.T \end{CD}\\ \mbox{commutative in }\mathcal{C}

ストリング図における自然性は、エレベータ法則になります。以下のように示せます。

モノイド・スタイルのモナド乗法μは次のように定義します。

  • A.μ := [(A.T)^]# （対象に対しては T = F）

「定義されたモナド乗法」であることを強調するために、二重丸にしました。

μの自然性も証明が必要です。

\begin{CD} A.(T\ast T) @>{A.\mu}>> A.T \\ @V{f.(F\ast F)}VV @VV{f.F}V \\ B.(T\ast T) @>{B.\mu}>> B.T \end{CD}\\ \mbox{commutative in }\mathcal{C}

絵算でエレベータ法則を示します。使うのは（当然ながら）、μの定義、F（射パート）の定義、拡張スタイルのモナド法則だけです。

拡張スタイルからモノイド・スタイルへ 法則の証明

拡張スタイルのモナド (T, η, (-)#)/C から構成された F, μ, η からなるモノイド・スタイルのモナド (F, μ, η)/C が、結合法則、右単位律、左単位律を満たすことを示す必要があります。それを示せれば、構成された (F, μ, η)/C は間違いなくモノイド・スタイルのモナドになります。

モノイド・スタイルのモナド法則は次のように示せます。煩雑になるので（それとめんどうなので）、ラベルは省略してますが、ラベルを補って解読してみてください。



おわりに

モノイド・スタイルはモノイドと同様に扱えるので、モナドの代数的な扱いには有利です。拡張スタイルはプログラミングではよく使われているし、モナド法則の証明がモノイド・スタイルより容易になる場合があります。それぞれ一長一短があるので、どちらか一方だけというわけにはいきません。

モノイド・スタイルと拡張スタイルは、可逆な翻訳で行き来できるという意味で同値です。この記事で、その同値性が成立することを実際に確認しました*5。細部まで観測することにより、両方のスタイルの定義が非常に巧みにできてるなーと感得できたのではないでしょうか。

*1:2-圏にも3次元以上の射が存在します。ただし、3次元以上には自明な射＝恒等射しかありません。

*2:プログラミングでは型構成子ですが、型を圏論の言葉で言えば対象です。

*3:交替律によるノードの移動は、無意識にできる（やってしまう）ので、テキスト計算だと2ステップ・3ステップを一度にやってしまうことが多いのです。

*4:以前、口頭で「絵算使えば簡単」とか言って計算し始めてうまくいかなかった事があります。グニグニを使わなかったせいだと思います。

*5:実は、行って返ってきたら元と同じである証明が欠けてますが、補ってくださいませ。

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

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

  • evA,B\circ<f, x>:1 → B in C

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

バインド記号

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

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

*3

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

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

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

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

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

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

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

適用と結合

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

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

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

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

より一般には：

  • 反図式順： (fn\circ ... \circf2\circf1)(x) = fn(... (f2(f1(x)))...)
  • 図式順： x.(f1;f2; ... ;fn) = x.f1.f2. ... .fn

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

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

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

反図式順 図式順
適用 f(x) x.f
結合 g\circf 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>>=(f1;;f2;; ... ;;fn) = x>>=f1>>=f2>>= ... >>=fn

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

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

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

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

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

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

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

[ T(A), [ [A, T(B)], T(B) ] ]
// 反カリー化
\cong [ T(A)×[A, T(B)], T(B) ]
// 直積の対称性
\cong [ [A, T(B)]×T(A), T(B) ]
// カリー化
\cong [ [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)# = idT(X) (3) (f;g#)# = f#;g# の3つの等式的法則です。それぞれ、モノイド・スタイルの単位律（左右の別は書き方に依存する）、結合律に対応します。

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

ひょっとして？ Excelシートに画像貼り付けの理由

日常

エラーやバグの報告で、画面ショットを添付することがあります。GUIアプリケーションではそれが当然でしょうし、画面ショットを付けてくれないと困ることも多いでしょう。

ですが、コンソールに出力されたテキストメッセージの画面ショットを何枚かとって、それをExcelシートにきれいに貼り付けるのは、僕には意味不明でした。「何のためにこんな事するのだろう？」と。画面ショットはとれるけど、テキストコピーは出来ない状況でしょうか？ でも、コンソールウィンドウをスクロールして何枚か画面ショットしているので、テキストコピーも出来そう。（[追記]←これは過去の経験[/追記]）

今日、画像付きExcelシートを（Googleスプレッドシートで）眺めたとき、「あっ」と思ったことがあります。行番号と列番号（列名か？）が画像の座標として使えるんですよね。「13行H列」とかで参照できます。これは、例えば電話で確認とかのとき便利です。

生の画像ファイルではなくて、それをExcelシートに貼るのは、参照用座標系を確保するため -- と仮説を立てたのだけど、真偽のほどはまったく分かりません。

[追記 date="翌日"]
長年の謎が解けた気分が先立って、書き忘れてしまいましたが； テキストメッセージはやはりテキストコピーしましょう。テキストメッセージの一部をGoogle検索したり、テキストデータとして利用したいことは多いのです。そのとき、画像を目視してキーボードで写し取るのは情けなくて、はなはだ気分が下がる作業なんです。

参照用座標系が実際に必要なときはExcelシートに貼るのも意味あるでしょうが、そうでないなら時間・労力の無駄です。誰も得しないどころか、誰もが損する作業になるので、無意味な画像貼り付けはやめましょう。テキストデータちょうだい。
[/追記]

測定と尺度

雑記／備忘

長めのCha話会の記録用メモ（1トピックのみ）。

内容：

アフィン空間の圏

圏の定義と、著名な幾つかの圏（例えば↓）については知っているものとします。

  • Set（集合と写像の圏）
  • Ord（順序集合と単調写像の圏）
  • Vect（ベクトル空間と線形写像の圏）
  • Monoid〈モノイドと準同型写像の圏）

これらよりはやや知名度が落ちる圏としてアフィン空間の圏Affを紹介します。アフィン空間はベクトル空間と密接に関係するので、係数体〈スカラー体 | 基礎体〉の指定が必要ですが、ここでは係数体をRに固定します。

アフィン空間は、集合A（点の集合）とベクトル空間Vと、写像 d:A×A → V *1の組 (A, V, d) で、まずは次の条件（他の条件は後述）を満たすものです。

  • a∈A を固定したとき、A∋ x \mapsto d(x, a) ∈V は双射〈全単射〉になる。

d(x, a) = x - a と引き算の形に書くのが便利です。関数〈写像〉 λx∈A.(x - a) : A → V は双射なので逆 V → A があります。これは足し算 a + v の形に書くと便利です。一旦は止めて考えていた a も動かしてやると、(a, v) \mapsto a + v は A×V → V という関数になります。

この足し算に関して次の条件を仮定します。

  • ∀a∈A.( a + 0 = a )
  • ∀a∈A. ∀v, w∈V.( a + (v + w) = (a + v) + w )

点とベクトルの足し算と、ベクトルとベクトルの足し算の両方に記号'+'をオーバーロードしているので注意してください。一時的に、点とベクトルの足し算を'▷'とでもすれば、

  • ∀a∈A.( a ▷ 0 = a )
  • ∀a∈A. ∀v, w∈V.( a ▷ (v + w) = (a ▷ v) ▷ w )

今まで述べた条件を満たす (A, V, d) がアフィン空間〈affine space〉です。

アフィン空間 (A, V, d), (B, W, d) （dはオーバーロード）のあいだの準同型写像は、点のあいだの写像 f:A → B とベクトルのあいだの線形写像 φ:V → W のペアで、次を満たすものです。

  • ∀a, b∈A.( φ(d(b, a)) = d(f(b), f(a)) )

あるいは引き算で書けば：

  • ∀a, b∈A.( φ(b - a) = f(b) - f(a) )

アフィン空間を対象として、そのあいだの準同型写像を射とする圏が構成できるので、それをAffとします。

群の主等質空間

アフィン空間の定義では、ベクトル空間のスカラー倍はなくてもいいので、ベクトル空間の代わりに単なる可換群でもかまいません。可換の仮定も実は不要なので、群Gが作用する集合Aに d:A×A → G があればアフィン空間と同様な構造を定義できます（dを引き算で書くのは適切じゃなくなるかも知れません）。

そのような構造は、群Gの主等質空間〈principal homogeneous space〉と呼びます。Aが単なる集合なら主等質集合が適切だと思いますが、あまりそう言わないので、「空間」を使っておきます。群の主等質空間については：

ベクトル空間の加法群に関する主等質空間が前節のアフィン空間です。群が非可換のときは、群作用が左か右かで事情がちょっと違うので注意してください。圏の名前を次のように約束します（標準的名前はないようです）。

  • 左主等質空間の圏を LPrincHomog
  • 右主等質空間の圏を RPrincHomog

測定の分類

とりあえず、測定を次のように定義しましょう； 測定対象物の集合Xと、測定値の集合Yがあるとき、関数 f:X → Y が測定〈measurement〉だと。

測定対象物の集合Xは、なんらかの圏Cの対象になっているとします。この条件は、特に制約にはなりません。極端なケースとして、対象がXだけで射がidXだけの圏をCと置けばいいので。ただし、Cは具象圏とします。つまり、Cの対象は集合に構造が載ったもので、射は適当な条件が付いた写像です。同様に、測定値の集合Yもなんらかの具象圏Dの対象になっているとします。C = D である必要はありません。

X∈C, Y∈D に対する測定 f:X → Y は、正確に書けば f:U(X) → U(Y) in Set です。ここで、Uは忘却関手です（Cの忘却関手とDの忘却関手を同じ'U'で表しています）。

ホムセット Set(U(X), U(Y)) が考えられるすべての測定の集合です。が、U(X) → U(Y) なら何でもいいってわけでもないでしょう。例えば、X, Y に足し算があれば、足し算を保存する測定（加法性を持つ測定）に限るとかするかも知れません。よって、Xに対する“Y値の測定”〈Y-valued measurement〉の全体 M(X, Y) は、

  • M(X, Y) ⊆ Set(U(X), U(Y))

測定対象物の集合Xと測定値の集合Yを許容される範囲内で動かした総体は、プロ関手〈profunctor〉

  • M:Cop×D → Set

と考えるといいかも知れません（たいしてよくないかも知らんが）。

個々の測定ではなくて、あらゆる測定の総体をMで表すとして、Mの定義には、観測値の集合達が所属する圏Dが関与しています。圏Dの対象達の特徴、あるいは圏Dの特徴が、測定Mの特徴として反映されるのは当然でしょう。

測定値（の集合）が持つ構造による分類は、次のように呼ぶのだそうです。

  • 名義尺度
  • 順序尺度
  • 間隔尺度
  • 比例尺度

これらのよく知られた（なのか？）分類は、たぶん、圏Dの取り方に対応しているでしょう。

  • 名義尺度 -- D ⊆ Set としたとき。
  • 順序尺度 -- D ⊆ Ord としたとき。
  • 間隔尺度 -- D ⊆ Aff としたとき。
  • 比例尺度 -- D ⊆ LPrincHomog または RPrincHomog としたとき。

比例尺度は、主等質空間の群として正実数の乗法群を取る場合が多いでしょう。

*1:正確に言えば、Vの台集合をU(V)として、d:A×A → U(V) in Set です。

恒等射の書き方

雑記／備忘

圏論の基本的な記法に、dom, cod, id があります。f \mapsto dom(f), f \mapsto cod(f), A \mapsto idA、idだけ引数〈argument〉が下付きで入るんですよね。id(A)としなかったのは、id(A)が関数のとき、関数の引数を渡すと id(A)(x) となるからでしょう。丸括弧で囲まれた引数が続く形は何故か嫌われていて、この形を避けるために下付き添字にされることは多いです（意味ね－けど）。

下付きにされると困るのは、入れ子にすると読み書きが困難になることです。

  • HTMLの'sub'使用： idididA
  • TeXの'_'使用： \mathrm{id}_{\mathrm{id}_{\mathrm{id}_A} }

丸括弧を使えば id(id(id(A))) とするだけです。DOTN二号記法では'^'〈サーカムフレックス | ハット | カレット〉で恒等射を示すので、A^^^ です。

idに下付き添字を使うなら、id0, id1, id2, … と番号にして欲しかった。高次圏まで考えると、そのほうが便利。“圏の圏”は2-圏なので、高次圏は無縁と言ってはいられません。

高次圏Cの構成素を次元ごとに分けて：

  • 0-Mor(C) = Obj(C) = |C| は、対象＝0-射 の（大きいかも知れない）集合
  • 1-Mor(C) = Mor(C) は、射＝1-射 の（大きいかも知れない）集合
  • 2-Mor(C) は、2-射の（大きいかも知れない）集合
  • 以下同様

idは、k-射に(k + 1)-射を対応させる写像なので、

  • id0:0-Mor(C) → 1-Mor(C)
  • id1:1-Mor(C) → 2-Mor(C)
  • id2:2-Mor(C) → 3-Mor(C)
  • 以下同様

A∈|C| ならば、入れ子 id(id(id(A))) は、id2(id1(id0(A))) です。

異なる圏〈高次圏〉のidを識別するために圏の名前を上付きにすると、

  • idC0:0-Mor(C) → 1-Mor(C)
  • idC1:1-Mor(C) → 2-Mor(C)
  • idC2:2-Mor(C) → 3-Mor(C)
  • 以下同様

圏の圏（ただし、小さい圏の圏とする）Catを考えると：

  • Catの対象Cごとに、idC0, idC1, idC2, … がある。
  • idCat0, idCat1, idCat2, … がある。

idC0 はあるが、idC1, idC2 なんて無いだろう？ って -- いや、あります。Cの1-射fに対して、idC1(f) は f = f という等式に相当します。idC2(f = f) は、(f = f)⇔(f = f) という、等式のあいだの論理的同値関係に相当します。

idCk という書き方は、どの圏〈高次圏〉の何次元の恒等射構成（k-射から(k + 1)-射を作り出す写像）かが明らかになりますが、煩雑なのも確かです。僕は次のような省略規則を採用しています。

  • Catの対象Cの idC0 は単にidと書く。
  • idCat0 はIdと書く。
  • idCat1 はIDと書く。

以前は、IDの代わりにギリシャ小文字ι〈イオタ〉を使ってましたが、手書きで'i'〈ラテン小文字アイ〉や'1'〈イチ〉と区別するのが難しいのでやめました。視認性が悪いと、コミュニケーションが阻害されトラブルを引き起こします。

C, D∈|Cat| に対して、Cat(C, D) は圏（関手を対象とする圏）になるので、この圏（ホム圏といいます）のidがあります。

  • Cat(C, D)ごとに、idCat(C, D)0, idCat(C, D)1, idCat(C, D)2, … がある。

idCat(C, D)0を略記するとき、idにするかIdにするか、はたまた他の記号にするか？ -- 僕は決めてなかったので、気まぐれに色々変わってましたね。

ともかく、単なる英字2文字'id'とか、漢字3文字「恒等射」とかで片付けないで、その英字2文字／漢字3文字がどれほど多様な意味と用法を持っているかも把握しておきましょう。

高次圏を考慮した指標の書き方

雑記／備忘

多相関数の話はもうしません（一段落ついた）。ですが、「多相関数と型クラス // 指標：いつもの事例で」で、指標の例を出したので、指標の話を続けようかな。高次圏論を考慮して指標の構文を決めるとどうなるか、という話です。

内容：

指標：いつもとチョットだけ違う事例

「多相関数と型クラス」にて：

毎度毎度同じ事例で恐縮ですが、モノイドの例を使います。
...[snip]...
等式的法則として、左単位律だけ書いてあって、右単位律と結合律は省略しています。面倒だからです。

今回は、「省略はしませんがモノイドではない事例」を使います。次の例です。

signature LUnitalPointedMagma in Set {
  type U
  function m:U×U -> U
  function e:1 -> U

  equation lunit :: (λU)-1;(e×idU);m = idU
  /* 省略はしてない。これでオシマイ */
}

この指標内に登場する記号 1, ×, λU, (λU)-1 の意味は「多相関数と型クラス // 指標：いつもの事例で」を見てください。

この指標で定義される代数構造は左単位的付点マグマ〈left unital pointed magma〉と呼びましょう。マグマ → 付点マグマ → 左単位的マグマ の順でだんだん複雑になります。マグマ〈magma〉と付点マグマ〈pointed magma〉の指標も再掲しておくと：

signature Magma in Set {
  type U
  function m:U×U -> U
}

signature PointedMagma in Set {
  type U
  function m:U×U -> U
  function e:1 -> U
}

指標のモデルの圏は Model[-] と書くことにします。ブラケット内には指標名か、指標そのものを書きます。例えば：

  • Model[PointedMagma]
  • Model[signature {type U function m:U×U -> U}]

二番目は Model[Magma] と同じです。ごく短い指標以外は、指標名を使うのが普通です。

指標のモデルの圏は、指標名を太字にした名前にするというルールを使います（別に破ってもいいルールですが）。

  • Magma := Model[Magma]
  • PointedMagma := Model[PointedMagma]
  • LUnitalPointedMagma := Model[LUnitalPointedMagma]

モデルの圏の射〈準同型写像〉の定義は、指標から自動的に決まります。それを説明するためには、記法の約束が必要です。Xが指標PointedMagmaのモデル（つまり、PointedMagmaの対象）だとして：

  • Xの台集合は、X.U と書く。
  • Xの二項演算は、X.m と書く。
  • Xの特定要素をポイントする写像は、X.e と書く。

より詳しくは「構造とその素材の書き表し方」参照。

この約束で、モデルの圏PointedMagmaの射〈準同型写像〉f:X → Y in PointedMagma は、次の図式を可換にするような台集合のあいだの写像 f:X.U → Y.U in Set のことです。

\require{AMScd} \begin{CD} X.U\times X.U @>{X.a}>> X.U \\ @V{f\times f}VV @VV{f}V \\ Y.U\times Y.U @>{Y.a}>> Y.U \end{CD} \\ \:\\ \begin{CD} {\bf 1} @>{X.e}>> X.U \\ @| @VV{f}V \\ {\bf 1} @>{Y.e}>> Y.U \end{CD}\\ \:\\ \mbox{commutative in }{\bf Set}

圏LUnitalPointedMagmaの射の定義も同じです。左単位的付点マグマを特徴づける左単位律（の等式）は、準同型写像の定義には影響を与えません。また、圏Magmaの射は、一番目の図式の可換性だけを要求します。

インスティチューション理論（そういう理論がある）では、左単位律のような条件〈公理〉は指標とは切り離しますが、「何を条件として切り離すか？」の基準がハッキリしないので（「指標と仕様」参照）、ここでは条件〈公理〉も指標内に記述します*1。

指標内のキーワードを変える

「多相関数の「パラメトリック性 vs 満足性」」にて：

標準的なキーワードは、type, function ではなくて、sort, operation ですが、キーワードに違和感を持つ人が多いので type, function にします。

というわけで、より伝統的なキーワードに戻せば：

signature LUnitalPointedMagma in Set {
  sort U
  operation m:U×U -> U
  operation e:1 -> U

  equation lunit :: (λU)-1;(e×idU);m = idU
}

キーワードがどうであれ、Uは集合圏Setの対象で、m, e は集合圏Setの射です。圏論用語をキーワードに使うならば：

signature LUnitalPointedMagma in Set {
  object U
  morphism m:U×U -> U
  morphism e:1 -> U

  equation lunit :: (λU)-1;(e×idU);m = idU
}

さらに一歩進めて、高次圏論〈n-圏論〉の用語をキーワードにしてしまいましょう。高次圏〈n-圏〉入門には次の記事があります。

過去記事の冒頭に注記がありますが、当時と今とでは記法が変わっています。現在僕が使っている記法については次の記事を。

さて、高次圏フレンドリーにした指標の構文は：

signature LUnitalPointedMagma in Set {
  0-morphism U
  1-morphism m:U×U -> U
  1-morphism e:1 -> U

  2-morphism lunit :: (λU)-1;(e×idU);m => idU
}

対象は0-射（0次元の射）で、通常の射は1-射（1次元の射）です。等式が2-射になってますが、これはどういうことでしょう？ 集合圏Setは1-圏、つまり、0-射と1-射を持つ圏ですが、実は2-射も（それどころか、任意のk-射を）持つのです。集合圏の2-射とは、1-射のあいだの恒等2-射です。恒等2-射は、1-射のあいだのイコールと同じことです。1-圏における2次元以上の射はすべて恒等射（イコール）になってしまうのです。

  • 1-圏において、k ＞ 1 であるk-射は、すべて恒等k-射（(k - 1)-射のあいだのイコール）である。
  • 一般のn-圏において、k ＞ n であるk-射は、すべて恒等k-射（(k - 1)-射のあいだのイコール）である。

したがって、1-指標の equation を 2-morphism とするのは理にかなっています。2-射（射のあいだのイコール）の宣言を丁寧に書くと次のようです。

  • 2-morphism lunit :: (λU)-1;(e×idU);m => idU:U -> U

一般に、k-射の宣言〈プロファイル宣言〉は次のパターンになります。◯の所には名前や式が入ります。

  • 0-射の宣言 0-morphism ◯
  • 1-射の宣言 1-morphism ◯:◯ -> ◯
  • 2-射の宣言 2-morphism ◯::◯ => ◯:◯ -> ◯
  • 3-射の宣言 3-morphism ◯:::◯ ≡> ◯::◯ => ◯:◯ -> ◯

より一般的で詳しい話は：

n-指標とターゲットn-圏

今まで出てきた指標は、通常の圏、つまり1-圏で解釈する前提です。実際、指標を解釈する圏は集合圏Setだとしてきました。1-圏での解釈が前提の指標を1-指標〈1-signature〉と呼びます。1-指標の解釈の場となる1-圏を（その指標の）ターゲット1-圏〈target 1-category〉と呼びます。集合圏とは限らない圏Cをターゲット1-圏とする1-指標は次の書式になります。

1-signature ◯◯◯ in C {
  /* 0-射、1-射、2-射のプロファイル宣言 */
}

我々の事例である 1-signature LUnitalPointedMagma が任意の圏Cで解釈できるかというと、そうはいきません。LUnitalPointedMagma には次の記号が含まれました。

  • 1
  • ×
  • λ

集合圏ではこれらの記号を解釈できますが、どんな圏でも意味を持つ記号ではありません。だからといって、集合圏Set以外では絶対に解釈できないわけでもありません。'1'を1次元ベクトル空間とみなしたR、'×'をベクトル空間のテンソル積、λをテンソル積の左単位律子〈left unitor〉とみなせば、実係数ベクトル空間の圏VectR内の左単位的付点マグマを考えることができます。

それらしくなるように、'1'を'I'に、'×'を'⊗'に置き換えて、VectR内の左単位的付点マグマの指標を書くと：

1-signature LUnitalPointedMagma in VectR {
  0-morphism U
  1-morphism m:U⊗U -> U
  1-morphism e:I -> U

  2-morphism lunit :: (λU)-1;(e⊗idU);m => idU
}

それらしいかどうかは心理的な問題で、まったく本質的ではないので、もちろん元の記号でもかまいません。

1-signature LUnitalPointedMagma in VectR {
  0-morphism U
  1-morphism m:U×U -> U
  1-morphism e:1 -> U

  2-morphism lunit :: (λU)-1;(e×idU);m => idU
}

記号は決まっていれば何でもいいですが、LUnitalPointedMagmaの1-指標は、モノイド圏で解釈する必要はあります。集合圏Setもベクトル空間の圏VectRも、モノイド圏だからLUnitalPointedMagmaのターゲット圏となり得るのです。

モノイド圏を定義する指標は2-指標となります。次のような形をしているでしょう。

2-signature MonCAT in CAT {
  /* なにやらかにやら */
}

「なにやらかにやら」の部分を実際に書き下そうと思うと、なかなかに難しい問題にぶち当たります。それについては：

とりあえずは難しいことは考えないことにして、次のような2-指標が存在すると信じましょう。

  1. 2-signature MonCAT in CAT ： モノイド圏を定義する2-指標
  2. 2-signature SymMonCAT in CAT ： 対称モノイド圏を定義する2-指標
  3. 2-signature CartMonCAT in CAT ： デカルトモノイド圏を定義する2-指標

これらの指標のなかで、各種の圏を構成する関手や自然変換を表す記号が定義されます。使う記号に強い標準はありませんが目安としては：

  1. '⊗', '×' ： モノイド圏のモノイド積、'×'はデカルト積
  2. I, 1 ： モノイド圏のモノイド単位、'1'はモノイド単位兼終対象
  3. α, λ, ρ ： モノイド積の結合律子〈associator〉、左単位律子〈left unitor〉、右単位律子〈right unitor〉
  4. σ ： 対称モノイド圏の対称
  5. Δ ： デカルトモノイド圏の対角
  6. ! ： デカルトモノイド圏の終射（終対象への唯一の射）
  7. π1, π2 ： デカルトモノイド圏の射影

これらの記号は、適切な2-指標で定義されているとします。射の結合記号';'、恒等射を表す記号'id'、逆射を表す記号'-1'は、2-指標で定義されるのではなくて組み込み〈builtin〉の記号だとします。

1-指標、2-指標があるなら、0-指標もあるのか？ あります。例を出せば：

0-signature abc in X {
  0-morphism a
  0-morphism b
  0-morphism c

  1-morphism bc_eq : b -> c
}

0-指標は、0-圏、つまり集合をターゲットとします。ターゲットXは集合です。0-圏〈集合〉の0-射とは要素です。したがって、指標で3つの要素 a, b, c を宣言しています。ここまでなら、集合Xの3つの要素を意味する指標です。が、0-指標に1-射が出来ています。これは、0-圏の1-射、つまり集合の要素のイコールです。bとcは等しいことを意味します。

それらしいキーワードで書き直すならば：

0-signature abc in X {
  element a
  element b
  element c

  equation bc_eq : b -> c
}

0-指標はあまり面白いものではありません。しかし、もう少し複雑な構文を許すと、0-指標もけっこう面白いものになります（今日は述べない）。

ここで、n-指標のk-射を宣言する“それらしいキーワード”をまとめておきましょう。確かに“それらしい”のですが、ゴチャゴチャとして統一性を欠き、俯瞰的な理解を阻害している要因だとも言えます。

0-指標 1-指標 2-指標
0-射 element sort, type, object sort, kind, object
1-射 equation operation, function, morphism operation, morphism
2-射 equation 2-operation, 2-morphism
3-射 equation

心理的な“それらしさ”を取るか、理論的な整合的性を取るか？ 一概には判断できませんが、統一的・俯瞰的な理解を目指すなら、“それらしさ”は犠牲にするしかありません -- キーワードは味気ない番号（次元）で区別することになります。

指標のメタ指標とusing

1-指標のなかで、0-射〈対象〉Xに対する恒等射 idX と、2つの射〈1-射〉 f, g の結合 f;g は自由に使ってかまいません。なぜなら、1-指標のターゲットは1-圏〈通常圏〉なので、恒等射も射の結合も備えているからです。しかし、モノイド積（双関手）やモノイド単位、なにか特別な対象（例：始対象、終対象）、なにか特別な自然変換（例：対角や射影）を使いたいときは、それらの関手や自然変換を表す記号がどこかで宣言されている必要があります。

関手や自然変換を表す記号を宣言するのが2-指標です。具体的には、2-signature MonCAT in CAT, 2-signature SymMonCAT in CAT, 2-signature CartMonCAT in CAT などです。1-指標を書くときは、その1-指標の親玉となる2-指標を選択する必要があります。1-指標のメタ指標〈meta signature〉と言ってもいいでしょう。

メタ指標の指定には using というキーワードを使うことにします。

using 2-signature CartMonCAT
1-signature LUnitalPointedMagma {
  0-morphism U
  1-morphism m:U×U -> U
  1-morphism e:1 -> U

  2-morphism lunit :: (λU)-1;(e×idU);m => idU
}

この1-指標で使われている名前・記号を色分けしてみます。

  • 任意の圏で使える組み込みの記号は赤色
  • メタ指標で宣言されている記号はオレンジ色（メタ指標の名前もオレンジ色）
  • この指標で宣言されている記号は水色（この指標の名前も水色）
using 2-signature CartMonCAT
1-signature LUnitalPointedMagma {
  0-morphism U
  1-morphism m:U×U -> U
  1-morphism e:1 -> U

  2-morphism lunit :: (λU)-1;(e×idU);m => idU
}

こうして見ると、出現しているすべての名前・記号は、どこかで宣言されていることが分かります。組み込みの記号か、メタ指標で宣言済みか、当該の指標で宣言されているかです。正体不明の記号はありません。正体不明の記号をなくすことで、指標による記述の精密さを担保したいのです。

この 1-signature LUnitalPointedMagma には、ターゲット1-圏が指定されていません。指標にターゲット圏が指定されてないときは、モデルの圏を作るときにターゲット圏を指定します。Model[LUnitalPointedMagma, Set] のように。ここで、ターゲット圏は何でもいいわけではありません。指標（1-指標）のメタ指標（2-指標）のモデルである圏に限られます。今の例では、1-signature LUnitalPointedMagma のメタ指標は 2-signature CartMonCAT なので、ターゲット圏はデカルトモノイド圏である必要があります。

1-指標のメタ指標である2-指標は、1-指標で使う記号を提供するだけではなく、1-指標のターゲット圏の種類も規定します。メタ指標（である2-指標）は、1-指標と、それに関連する構文論／意味論のすべての部分に影響します。2-指標をドクトリン〈doctrine〉と呼ぶこともあります。実際、2-指標＝ドクトリンは、構文論と意味論が絡み合った組織体を統制する教義〈基本原理〉になっています。

他の指標の利用とimport

指標（単に指標と言えば1-指標）を書くときに、既にある他の指標を利用したいことがあります。例えば、1-signature LUnitalPointedMagma は、1-signature PointedMagma に等式〈2-射の宣言〉を付け加えただけです。付け加える差分だけ記述できれば便利です（いわゆる“継承”のような書き方）。

他の指標を利用可能とするためのキーワードは import にします。次が import の使用例です。

using 2-signature CartMonCAT

1-signature PointedMagma {
  0-morphism U
  1-morphism m:U×U -> U
  1-morphism e:1 -> U
}

1-signature LUnitalPointedMagma {
  import 1-signature PointedMagma

  2-morphism lunit :: (λU)-1;(e×idU);m => idU
}

import 1-signature PointedMagma の部分に、1-signature PointedMagma の内部がそのまま展開されると思えばいいです。複数の指標をインポートするときは、名前のバッティングの問題を処理する必要がありますが、今日は触れません。

おわりに

高次圏を考慮した指標の書き方を紹介しました。実際のところ、指標について調べるには、高次圏は避けられないでしょう。1-指標の構文と、意味論のためのターゲット1-圏は、メタ指標である2-指標によって支配されます。その2-指標の構文と、意味論のためのターゲット2-圏は、さらにメタ指標でである3-指標により支配されます。その3-指標の‥‥ 無限に続きます。

この無限に続く構文論・意味論のタワーは、僕をずっと悩ませてきました。精神安定のために、有限階で安定的に循環するのだ、と信じています（例えば「デカルト・タワーを求めて」参照）。有限階を考えれば十分だと保証できれば、安心できます。

特に、2-指標と2-圏まで考えれば十分な状況が作れれば、特定の2-指標をメタ指標として固定して、そのメタ指標で支配される1-指標達の議論ができます。無限タワーの2階までを自由に使いこなせれば、それだけでも、かなりの程度の構文論・意味論が展開できます。そのとっかかりは「指標とは何か？」をハッキリさせることです。

*1:構成素と条件の境界線が恣意的になってしまう気がします。必然的な境界線が存在するのでしょうか？ わかりません。

ツリーデータ型のモナド

雑記／備忘

ある種のツリーデータ型はモナドにできます。

[追記]この記事は十何年か前に書いておくべきだったのかも知れません。当時は、ツリーデータ型のモナドは自明な事実に見えてました（ツリーばっかりいじっていたからなー）。が、「えっ、そうだったの」と思う人もいそうなので、思い出して記した次第。[/追記]

内容：

自由モノイド＝クリーネスター

集合Xに対して、Xから生成される自由モノイド (M, #, ε) を定義しましょう。

  • モノイドの台集合Mは、Xの要素を並べた列の集合。List型構成子を知っているなら、M := List(X) 。
  • モノイドの演算#は、列〈リスト〉の連接〈concatenation〉。
  • モノイドの単位元は、空列〈空リスト〉ε 。

台集合MをX*とも書きます。また、いつもの記号の乱用（悪習）により、

  • X* = (X*, #, ε)

写像 f:X → Y in Set に対して、モノイド準同型写像 X* → Y* in Monoid を構成できるので、関手 FreeMonoid:Set → Monoid を構成できます。これは、グラフからの自由圏構成 FreeCat:Graph → Cat の特別なものだとみなすこともできます -- 興味があれば、次の記事を参照してください。

X* の右肩の星はクリーネスター〈Kleene star〉と呼ばれ、自由モノイドの台集合、自由モノイド、自由モノイド生成関手などの意味で使われます。

ファイルシステム風パス記法

具体例として次の3つの集合を考えます。

  1. A = {a}
  2. B = {1, 2, 3}
  3. C = {foo, bar}

Aの要素は「文字 a」そのものなので 'a' と書いたほうがいいでしょう。同じ理由で、Cの要素は "foo", "bar" と書いたほうがいいでしょう。しかし、めんどくさいので、a, foo, bar にします。

A*, B*, C* の要素をどう表しましょうか？ a, aaa∈A*、3, 3231∈B* とかはいいでしょうが、C* の要素を foobarbar とか書くと区切りがわかりません。スラッシュを区切り記号に使うことにします。そうすると、ファイルシステムのパスに似ているので、行きがかり上、先頭（左端）にもスラッシュを置きます。

単なる併置 スラッシュ区切り
a /a
aaa /a/a/a
3 /3
3231 /3/2/3/1
foobarbar /foo/bar/bar

空列εは単一のスラッシュ / で表します。連接演算はホントに並べるだけですが、空列との連接では余分なスラッシュを削除します。

  • /a # /a/a/a = /a/a/a/a
  • / # /a/a/a = /a/a/a
  • / # / = /

ツリー形状とリーフ値付きツリー

ツリー形状〈tree shape〉がどんな形であるかは説明しません。皆さんの直感的理解で十分です。一例を挙げれば、次の図形はツリー形状です。

ツリー形状は、何の装飾もない“裸のツリー”のことです。ツリー形状は、ルートからリーフ〈葉〉へと向かう方向を考えて有向グラフになります。ツリー形状への修飾として、すべての辺にラベルを付けます。辺ラベルの集合をXとします。

ツリーのすべてのノードが辺ラベルの列で一意的に表現できるように、次の制限を付けます。

  • ひとつのノードから出る辺の本数は、集合Xの基数〈cardinarity〉を超えてはならない。

そして、ラベリングは実際にノードが一意的に表現できるものに限ります。兄弟辺に同じラベルが付くのはダメです。

辺ラベルの集合Xが無限集合なら、上記の基数に関する制限は常に満たされます。辺ラベルの集合に、A = {a} や C = {foo, bar} を使うと、上の例のツリー形状にラベリングできません。辺ラベルの集合に B = {1, 2, 3} を使えばOKです。上のツリー形状のすてのノードをラベル {1, 2, 3} を使ったパスで表現してみましょう。

  1. /
  2. /1
  3. /1/1
  4. /1/2
  5. /1/2/1
  6. /1/2/2
  7. /1/2/3
  8. /2
  9. /2/1

このなかでリーフノードは次の5個です。

  1. /1/1
  2. /1/2/1
  3. /1/2/2
  4. /1/2/3
  5. /2/1

リーフノードの意味は明らかでしょうが、ルートノードしかないツリーでは、ルートノードはリーフノードになります。

辺ラベルの集合とは別に（同じ集合でもかまわないが）集合Yを考えます。リーフノードにだけYの値を割り当てたツリーを、リーフ値付きツリー〈leaf-velued tree〉と呼びましょう。辺ラベルの集合がXであり、リーフ値の集合がYであるリーフ値付きツリー全体の集合を LVTreeX(Y) とします。

上記の例で、リーフ値の集合を C = {foo, bar} とすると、LVTreeB(C) ができます。その要素の一例は、リーフノードのパスに foo か bar に割り当てればいいので、例えば次のように書けます。

  1. /1/1 \mapsto foo
  2. /1/2/1 \mapsto foo
  3. /1/2/2 \mapsto bar
  4. /1/2/3 \mapsto foo
  5. /2/1 \mapsto bar

入れ子のリスト（囲み括弧をブラケットにする）として次のように書いてもかまいません。

  • [ [foo, [foo, bar, foo]], [bar] ]

[追記]↑が間違っていたので修正しました。2次元的なレイアウトを使うと間違えないかな。

          [ ]
   [ ],           [ ]
foo,   [ ]        bar
   foo, bar, foo

[/追記]

リーフ値付きツリーデータ型のモナド

ツリーの辺ラベルの集合Kを固定します。Kの要素は“キー”と呼んでもかまいません。そして、リーフ値の集合を色々と変化させます。この節での X, Y などは色々と変化させる集合です。

  • X \mapsto LVTreeK(X) （Xは色々と変化させる集合）

という、“集合 \mapsto 集合”対応は、型構成子になります。写像 f:X → Y in Set に対して、fをツリーに適用するように“マップ化”することもできます。

  • map(f):LVTreeK(X) → LVTreeK(Y)

型構成子とマップ化高階関数の組は関手を定義するので、この関手を同じ名前で

  • LVTreeK:Set → Set

とします。

集合圏上の自己関手 LVTreeK に、2つの自然変換 η, μ を付け足して、モナドにしましょう。

  • For X∈|Set|, ηX:X → LVTreeK(X) in Set
  • For X∈|Set|, μX: LVTreeK(LVTreeK(X)) → LVTreeK(X) in Set

ηX:X → LVTreeK(X) は次のように定義します。

  • x∈X に対して、「ルートノードしかないツリーで、リーフ値がxであるリーフ値付きツリー」を対応させる。

μX: LVTreeK(LVTreeK(X)) → LVTreeK(X) は、次のように考えます。

  • LVTreeK(LVTreeK(X)) の要素は、親のツリーの各リーフに子のツリーが入れ子で入っている。“親のリーフノード”と“子のルートノード”を同一視する（糊付けする）ことにより入れ子を平坦化したツリーは LVTreeK(X) の要素になる。

ラフな定義(?)ですが、お好みのプログラミング言語で実際の処理を書いてみれば実感が湧くでしょう。(LVTreeK, η, μ) がモナドになるには、モナド法則を満たす必要がありますが、その確認は練習問題とします。

多相関数と型クラス

雑記／備忘

面白い偶然が起きることがあります。

ごく最近、次の記事を書きました。

そして9月8日と9月9日（昨日）、4年前の記事にkhibinoさんからコメントをいただきました。

これらの話題は無関係じゃないんですよね。奇遇。

4年前の記事の背景として、僕には“指標とモデルの圏”の話をしたい動機がありました。それに対して、Haskellの型クラスは用途が制限され過ぎていて気に入らない、といったことを書きました。今思えば、「気に入らない」という感情が先行していて、「君の型クラス vs ワシの型クラス」みたいになっていて、「不毛」とまでは言わないまでも、薄毛な（不毛に近い）議論だったかも知れません。ワシの型クラス（檜山好みの型クラス）とは、指標とモデルの圏を記述するのに適切なメカニズムのことです。

khibinoさんによれば、一般的な指標を記述したいならレコードを使えばいいよ、とのこと。Haskellの型クラスはオーバーロード解決が主目的だから、トレードオフとして用途が制限されるのは致し方ないのでしょう。

さて、この機会に、薄毛な議論を避けるために、次の概念を明確化しておくことにします。

  1. 多相関数
  2. パラメトリック性
  3. 指標とそのモデルの圏
  4. 指標に従うモダリティ

多相関数、パラメトリック性は、冒頭の最近の記事で説明しました（この記事でもごく短く復習します）。この記事で、指標とそのモデルの圏、指標に従うモダリティを説明します。

内容

指標：いつもの事例で

毎度毎度同じ事例で恐縮ですが、モノイドの例を使います。ただし、今までよく使っていた（伝統的な）キーワードを変更します。

従来（伝統的） より親しみやすい
sort type
operation function
equation equation

キーワードを変える理由は、sort, operation に違和感を感じる人がいるようで*1、それが理解を阻害するならより親しみやすくしよう、と*2。

signature Monoid in Set {
  type U
  function m:U×U -> U
  function e:1 -> U

  equation lunit :: (λU)-1;(e×idU);m = idU
  ‥‥ 略 ‥‥
}

次の記号は前もって集合圏内で意味が定まっています。

  • 1 : 集合圏の特定された終対象かつ単位対象。1 = {1} と思ってよい。
  • × ： 集合圏のモノイド積としての直積。
  • λU ： 直積の左単位律子〈left unitor〉*3 λU:1×U → U 。
  • (λU)-1 ： 左単位律子は可逆なので、逆射 (λU)-1:U → 1×U 。

等式的法則として、左単位律だけ書いてあって、右単位律と結合律は省略しています。面倒だからです。テキストの等式より、可換図式のほうが分かりやすいですしね、次のように。

\require{AMScd} \begin{CD} U @>{(\lambda_U)^{-1}}>> {\bf 1}\times U \\ @V{\mathrm{id}_U}VV @VV{e \times \mathrm{id}_U}V \\ U @<{m}<< U\times U \end{CD} \\ \:\\ \mbox{commutative in }{\bf Set}

モノイドであるための条件（左単位律、右単位律、結合律）を、テキストで書くなら、可換図式と等価な等式で書くより、（古典論理の）論理式を使ったほうが楽です。論理式を使うときは、キーワード condition を先頭に置くことにします。

signature Monoid in Set {
  type U
  function m:U×U -> U
  function e:1 -> U

  condition lunit_cond : ∀x∈U.( m(e(1), x) = x )
  condition runit_cond : ∀x∈U.( m(x, e(1)) = x )
  condition assoc_cond : ∀x, y, z∈U.( m(x, m(y, z)) = m(m(x, y), z) )
}

モノイドであるための条件は、モノイドの公理といったりもします*4。

条件〈公理〉を何も課さない、単なる二項演算だけを持つ構造はマグマ〈magma〉と呼びます。マグマの指標は次のようです。

signature Magma in Set {
  type U
  function m:U×U -> U
}

二項演算と、台集合（Uと書いてます）の特定要素を持つ構造は付点マグマ〈pointed magma〉と呼ぶことにします。その指標は：

signature PointedMagma in Set {
  type U
  function m:U×U -> U
  function e:1 -> U
}

台集合の特定要素は、その要素をポイントする写像 e:1 -> U で表します。

付点マグマが与えられたからといって、それがモノイドになることはまったく保証されません。

多相関数＝関手間部分変換

「蒸し返し： アドホック多相 vs パラメトリック多相 // 部分圏に相対的なパラメトリック性」の復習をします。次の状況を考えるのでした。

  1. F, G:Set → Set は関手。
  2. Kは集合の集合。同じことだが K⊆|Set| 。
  3. ψ:K → Mor(Set) つまり、ψは、Kの要素（それは集合）でインデックスされた関数の族。
  4. dom(ψX) = F(X), cod(ψX) = G(X) 。
  5. C, D などはSetの部分圏で、|C| = |D| = K 。

F, G は集合圏の自己関手ですが、部分圏Cに制限すると、Set上の関手とはいえません、C上の関手ですもんね。ψは、FからGへのある種の“変換”ですが、自然性は仮定していません。こんな状況で使う道具は次の記事で説明しています。

この過去記事から引用すると：

ここでの「非全域」は「全域ではない」という意味ではありません。「必ずしも全域とは限らない」です。「非可換」というよく使う言葉も「必ずしも可換とは限らない」の意味なので、「非」のよくある用法だと思います。「非自然」も同様な解釈をします。

「非」のよくある用法だ、とはいえ、このテの「非」が誤解をまねくのも事実です。自然性は仮定しない関手のあいだの変換（過去記事の「非自然変換」）を関手間変換〈inter-functor transformation〉と呼ぶことにします。部分圏の上でしか定義されてない関手間変換は、関手間部分変換〈inter-functor partial transformation〉です。

舞台は集合圏Setに限定することにして、多相関数〈polymorphic function〉とは、（集合圏上の）関手間部分変換のことだと定義します。これで、「多相関数」という言葉の曖昧性は（今の文脈では）排除できます。

[補足]通常の関数を（上で定義した意味の）多相関数とみなす方法を説明しておきます。f:A → B in Set に対して、F(X) := A, F(g) := idA, G(X) := B, F(g) := idB と2つの関手 F, G を定義して、K := {1} に対して、ψ:K → Mor(Set) を次のように定義します。

  • ψ1 := f

すると、ψは単元集合Kでインデックスされた関数族（実際は単一の関数）で、関手Fから関手Gへの関手間部分変換になります。1 と id1 で構成される自明な圏に対してψはパラメトリック性〈自然性〉を持ちます。
[/補足]

自然性と保存性

2つの関手 F, G:Set → Set のあいだの自然変換のプロファイルは α::F ⇒ G 、あるいはより丁寧に α::F ⇒ G:Set → Set と書きます。プロファイルについて詳しくは次の記事を参照してください（興味があれば）。

多相関数＝関手間部分変換のプロファイルは次のように書くことにします。

  • ψ:.F ⇒ G:C → Set

':.'は'::'に比べてなんか足りない感じを表します。ここで、K = |C|, ψ:K → Mor(Set) （ψを写像とみなして）です。C → Set を省略するとき、あるいはCを考えてないときは、Kの情報を添えて、

  • ψ:.(K)F ⇒ G

にしましょう。Kは、インデックス族〈indexed family〉としての多相関数ψのインデキシングセットです。

多相関数 ψ:.(K)F ⇒ G がパラメトリックであることは、部分圏C に対して相対的に決まり、パラメトリック性は ψ:.F ⇒ G:C → Set （K = |C|） が自然変換になることでした。このことを次のように書きます（「蒸し返し： アドホック多相 vs パラメトリック多相 // 部分圏に相対的なパラメトリック性」での約束）。

  • ψ is-natural-on C

lengthとは別な多相関数の例として、適当な K⊆Set 上で定義された μ:.(K)F ⇒ G を考えます。ここで、F, G :Set → Set は：

  • F(A) := A×A, F(f) := f×f
  • G(A) := A, G(f) = f

したがって、多相関数 μ:.(K)F ⇒ G の“Cに相対的なパラメトリック性＝自然性”は、次の可換図式で書けます。

\require{AMScd} \forall f:X \to Y \:\mbox{ in }\mathcal{C} \\ \:\\ \begin{CD} X \times X @>{\mu_X}>> X \\ @V{f \times f}VV @VV{f}V \\ Y \times Y @>{\mu_Y}>> Y \\ \end{CD} \\ \:\\ \mbox{commutative in }{\bf Set}

μX は、集合 X∈K（K = |C|）上の二項演算です。そして、上の図式は、fが二項演算を保存することを示しています。任意の f∈Mor(C) が二項演算（の族）を保存〈preserve〉するので、次のように書きましょう。

  • C preserves μ

もちろん、μ is-natural-on C と C preserves μ はまったく同じ意味です。多相関数ψを主語にすると自然性〈naturality〉で、部分圏Cを主語にすると保存性〈preservation property〉になります。

(X, μX) はマグマのインスタンスなので、二項演算を保存するfとはマグマの準同型写像〈homomorphism〉といえます。Cの射〈写像〉はすべてマグマの準同型写像なので、Cはマグマと準同型写像の圏です。結局、次の命題達は同じことを言ってます。

  • μ is-natural-on C
  • C preserves μ
  • Cは、マグマと準同型写像の圏（ただし、|C| = K）
  • Cは、すべてのマグマとすべてのマグマ準同型写像からなる圏Magmaの部分圏

もうひとつ ε:.(K)K1 ⇒ Id という多相関数εを考えましょう。おっと、文字'K'がコンフリクト（偶発的・不注意による衝突）してしまいましたが、んなことは気にしない。ここで：

  • K1(A) := 1, K1(f) := id1
  • Id(A) := A, Id(f) = f

多相関数 ε:.(K)K1 ⇒ Id の“Cに相対的なパラメトリック性＝自然性”は次の可換図式で書けます。

\require{AMScd} \forall f:X \to Y \:\mbox{ in }\mathcal{C} \\ \:\\ \begin{CD} {\bf 1} @>{\epsilon_X}>> X \\ @V{\mathrm{id}_{\bf 1}}VV @VV{f}V \\ {\bf 1} @>{\epsilon_Y}>> Y \\ \end{CD} \\ \:\\ \mbox{commutative in }{\bf Set}

多相関数 μ と ε を一緒に考えると、次の命題達は同じことを言ってます。

  • μ is-natural-on C かつ ε is-natural-on C
  • C preserves μ かつ C preserves ε
  • Cは、付点マグマと準同型写像の圏（ただし、|C| = K）
  • Cは、すべての付点マグマとすべての付点マグマ準同型写像からなる圏PointedMagmaの部分圏

幾つかの多相関数を固定すれば、パラメトリック性は「部分圏が準同型写像の圏であるか？」を判断する尺度となります。多相関数（の集まり）と部分圏は、互いに他を規定しあっているのです。

心にモノイド、コードは付点マグマ

指標に相当する構文は、多くのプログラミング言語がサポートしています。「指標」という名称ではなくて「インターフェイス」と呼ぶことが多いですね。Haskell, Coqの「型クラス」（名前は同じだがだいぶ違う）、Rustの「トレイト」、C++の「コンセプト」（紆余曲折で今どうなっているか知らない）とかも指標類似構文です。

最初に出した signature Monoid in Set に相当するモノイドの指標を、各プログラミング言語である程度は書けるでしょう。多くの（全部のではない）プログラミング言語では、左単位律、右単位律、結合律というモノイドの条件〈モノイドの公理〉までは書けません。モノイドの条件は、プログラマの心のなかにあり、コードとしては signature PointedMagma in Set を書くことになります。

心のなかを表すために、名前だけMonoidとしたり、コメントに気持ちを書いたり、モノイドの条件をテストするテストコードを付けたりします。条件部分（構造の公理）までキチンと扱うのは大変です。言語処理系を作るのも難しいでしょうが、仮に言語処理系があっても、それを使うにはユーザーにそれ相応のスキルが要求されます。指標に条件まで書けるのがポピュラーになるには、何十年もかかるかも知れません。

そんな事情で、次のようなインチキな指標を書くことがしばしばあります。

signature Monoid in Set {
  type U
  function m:U×U -> U
  function e:1 -> U

/* 省略しているわけではない。
   書こうとしても書けないので
   書いてない。
  */
}

名前で心のなか／気持ちを表しています。実際は付点マグマ〈PointedMagma〉の指標です。もう一度繰り返しますが：

  • 付点マグマが与えられたからといって、それがモノイドになることはまったく保証されません。

指標のモデル

指標、例えば付点マグマの指標が与えられたとしましょう。指標内に出てくる不定記号〈意味が未定の名前〉は U, m, e の3つです。不定記号'U'に実際の集合、不定記号'm'と'e'に実際の写像を割り当てたものを指標のモデル〈model〉といいます。ただし、指標内に書かれたプロファイル宣言は守る必要があります。指標内に条件も書いてあれば、モデルはその条件を満たす必要があります。

ある指標Fooが与えられたとき、指標のモデルを対象として、モデルのあいだの準同型写像を射とする圏を太字でFooと書くことにします。準同型写像の定義は自動的に出てきます（関手圏の射として）。既に太字で書く記法は使っています。

  • signature Magma のモデルの圏 ＝ Magma
  • signature PointedMagma のモデルの圏 ＝ PointedMagma

もっと簡単な指標も出しておきましょう。

signature PointedSet in Set {
  type U
  function e:1 -> U
}

この指標に対応する圏はPointedSetで*5、圏PointedSetの射は、下の図式を可換にする写像 f:X.U → Y.U in Set です。ここで、2つの付点集合〈pointed set〉X, Y に対して、その台集合は X.U, Y.U で、特定点をポイントする写像は X.e, Y.e です。詳細は「構造とその素材の書き表し方」参照。

\begin{CD} {\bf 1} @>{X.e}>> X.U \\ @| @VV{f}V \\ {\bf 1} @>{Y.e}>> Y.U \\ \end{CD}

注意すべきことは、ひとつの集合上に付点集合の構造はたくさんあることです。例えば、集合 {1, 2, 3} 上の付点集合は3つあります。

  1. X =({1, 2, 3}, e1), X.U = {1, 2, 3}, X.e = e1 = (1 \mapsto 1)
  2. Y =({1, 2, 3}, e2), Y.U = {1, 2, 3}, Y.e = e2 = (1 \mapsto 2)
  3. Z =({1, 2, 3}, e2), Z.U = {1, 2, 3}, Z.e = e3 = (1 \mapsto 3)

集合 {1, 2, 3} に対して、付点集合が自動的にひとつだけ決まるなんてことはありません。

指標に従うモダリティ

指標に相当する構文を、多くのプログラミング言語が持っていますが、構文に対応する意味的メカニズムは様々です。前節で述べた“モデルの圏”をベースにしている場合（たぶん多数派）もありますが、Haskellの型クラスは違います。特別なタイプの指標に対して、モデルの圏ではなくてモダリティを構成しています。

モダリティとは、圏の対象ごとに構造をひとつだけ対応させるメカニズムです。比較的最近、フォングとスピヴァックは、対称モノイド圏のモダリティの一種を装備〈supply〉として定式化しています*6。

しかし僕は装備〈supply〉についてあまり理解してないので、古くて曖昧な（人により意味が違う）言葉「モダリティ」を使い続けることにします。なお、興味があれば、モダリティを主題とした記事は以下です。

今まで例に出した指標は、type宣言（伝統的にはsort宣言）がひとつだけでした。このような指標を単ソート指標〈single sorted signature〉と呼びます。単ソート指標のモデル、例えば付点マグマのモデル X = (X.U, X.m, X.e) があると、X \mapsto X.U と対応させて忘却関手 USet:PointedMagma → Set を定義できます。USetは"underlying set"のつもりです。

単ソート指標である付点マグマ指標に従うモダリティ〈modality〉とは、写像 M:|C| → |PointedMagma| のことです。ただし、モダリティと忘却関手のあいだに次の関係を要求します。

  • For X∈|C|, USet(M(X)) = X

付点マグマ指標に従うモダリティを定義することは、次の2つの多相関数を定義するのと同じことです。

  1. μ:.(|C|) (-×-) ⇒ Id
  2. ε:.(|C|) K1 ⇒ Id

X∈|C| に対する M(X) は、(X, μ, εX) で与えられます。

付点マグマ指標に従うモダリティを与える2つの多相関数 μ, ε が、Setの部分圏Cに対して自然である必要があるでしょうか？ 別な言い方をすると、Cの射〈写像〉が付点マグマの準同型写像である必要があるでしょうか？ 別にどっちでもいいですよね。

  • Cの射が付点マグマの準同型写像じゃなくてもいい。準同型写像じゃない射が欲しいときもある。
  • Cの射を、付点マグマの準同型写像だけに制限したいときもある。
  • ケースバイケース、好きにすればいい。

Setの部分圏Cに「付点マグマの準同型写像じゃない射」が入っていると、多相関数 μ, ε は自然〈パラメトリック〉にはなれません。これは、なにか悪いことが起きているのではなくて、単に「そういうこともある」だけです。アドホック多相関数がパラメトリック多相関数に比べて劣っているとか、使ってはいけない、なんてことはありません。それは、次の記事に述べたことに通じます -- 関手や自然変換ではない対応を使うことは悪いことじゃないです！

今述べた形のモダリティは、オーバーロード解決には便利です。が、やはり用途が限定されていることは否めません。もっと自由度の高い構成には別な手段が必要でしょう。

*1:用語、キーワードの国語辞書的意味に拘るのはやめて欲しいけど。

*2:しかし、単ソート指標、多ソート指標の「ソート」を別途説明する必要があるかも。

*3:モノイドの単位律ではなくて、モノイド圏の単位律に関わる同型射です。

*4:モノイドであるための条件〈公理〉は指標に含めない、という立場もあります。それは「指標とは何か？」とか「指標と仕様の違い」に関わる問題です。「指標と仕様」参照。

*5:僕は、PtSetという名前もよく使います。Pointedも使ったことあるな。まっ、色々。

*6:「マルコフ圏の一族 // 様々な装備圏」で触れました。

多相関数の「パラメトリック性 vs 満足性」

雑記／備忘

「アドホック多相」「パラメトリック多相」という言葉は、ハッキリとした定義がないままに使われることが多いようです。その実情を追認、あるいは実情に迎合して「どうせ定義がイイカゲンなんだから、イイカゲンに使えばいいよね」と述べたのが「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない」です。とはいえ、同じ記事の最後のほう「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない // それでもマジメに考えたいのなら」と、昨日の記事「蒸し返し： アドホック多相 vs パラメトリック多相」では、定義をハッキリさせる試みをしました。

もともとが曖昧な概念を明確化すると、それは（広く合意を得られないので）俺流定義になってしまいます。昨日の記事で述べた「パラメトリック性 ＝ 自然性」も、「オレの思っているパラメトリック性と違う」という人はいるでしょう。僕も、「パラメトリック性」が持つ“雰囲気”は、自然性だけでは言い尽くせない気がしています。

自然性では汲み取れない性質を「満足性〈satisfaction property〉」として定式化してみます。例題は、昨日と同じlength関数です。

内容：

とりあえずパラメトリックなlength関数

多相関数のパラメトリック性〈parametricity property〉とは、関数のインデックス族〈indexed family of functions〉の自然性〈naturality〉だと定義する（そう決めて話をする）と、length関数のパラメトリック性＝自然性は次の図式の可換性として記述できます。

\require{AMScd} \forall f:X \to Y \:\mbox{ in }\mathcal{C} \\ \:\\ \begin{CD} \mathrm{List}(X) @>{length_X}>> {\bf Z} \\ @V{\mathrm{List}(f)}VV @| \\ \mathrm{List}(Y) @>{length_Y}>> {\bf Z} \\ \end{CD} \\ \:\\ \mbox{commutative in }{\bf Set}

図式の可換性の成立は、Setの部分圏Cに依存します。ある部分圏Cに関してlengthが自然であることを、次のように書きます（昨日の記事での約束）。

  • length is-natural-on C

昨日の記事で述べた、A君、B君、C君が書いた３つのlengthをまとめた多相関数lengthは、圏S1に関して自然にはなりません。

自然に〈パラメトリックに〉ならなかった理由は、C君が「長さ」に関してA君、B君とは異なる連想をしていたからです。そこで、上司のXさんは次のように言います。

  • 3人でちゃんと相談して、それぞれが書いた関数達をまとめた多相関数が、圏S1に関して自然〈パラメトリック〉になるようにしなさい。

3人は相談して、「めんどくせーから、これでいいことにしようぜ」と、次の関数を書きました。

function lengthByA = lambda(x : List<Int>){ 0 }
function lengthByB = lambda(x : List<Char>){ 0 }
function lengthByC = lambda(x : List<Real>){ 0 }

あらゆるリストの長さは0です。これらをまとめた多相関数lengthは、圏S1に関して自然になります。

Xさんは、内心不満を感じながらも3人を叱るわけにもいきません。3人は言われたことをちゃんとやってますからね。

満足性とは何か

Xさんが内心不満を感じるのは、lengthへの期待があり、それを裏切られたからです。lengthへの期待は「lengthらしさ」と言ってもいいでしょう。常に値が0ではlengthらしくないのです。

「lengthらしさ」を持っていることをパラメトリック性とは呼ばないでしょうが、雰囲気としては、パラメトリックなら「らしさ」も持っているだろうと期待します。実情としては、暗黙に（あくまで暗黙にですが）パラメトリック性が「らしさ」を持つことも含意してるかも知れません -- Xさんの内心の期待と、それを裏切られた不満のように。

さて、「らしさ」の定式化として満足性〈satisfaction property〉を定義しましょう。満足性の定義には、インスティチューション理論の道具立てを使います。が、インスティチューション理論を知っている必要はありません。

Xさんは「lengthらしさ」を内心期待してましたが、3人に伝えてません。「lengthらしさ」を何個かの文として言語化しなくてはなりません。実際の関数fが、文sで記述された性質を実際に持つとき、次のように書きます。

  • f |= s

記号'|='（TeXだと \vDash ' \vDash'）は、満足関係〈充足関係 | satisfaction relation〉の記号です。「関数fは文sを満足する」と読みます。

文sが、Xさんの思う「lengthらしさ」を記述しているとして、A君、B君、C君が書いた実際の関数が実際に「lengthらしい」ことは次のように書けます。

  • lengthByA |= s
  • lengthByB |= s
  • lengthByC |= s

Xさんの思いが単一の文ではなくて2つの文 s1, s2 で記述されているなら：

  • lengthByA |= s1, lengthByA |= s2
  • lengthByB |= s1, lengthByB |= s2
  • lengthByC |= s1, lengthByC |= s2

このように、なんらかの文（の集まり）で記述された条件を満たすことが満足性です。

思いを正確に伝える

Xさんの思う「lengthらしさ」を、A君、B君、C君に自然言語（日本語）の文で伝えてもいいですが（多くの場合はそうするでしょう）、「length〈長さ〉という言葉からの連想が人により違う」ことによる失敗は既に経験済みです（昨日の記事）。自然言語の曖昧さや連想の豊かさによるトラブルを避けるには人工的な論理言語を使うほうがいいでしょう。ここでは、常識的な（古典論理の）論理式を使うことにします。

論理式の文法は知られていますが、「lengthらしさ」を記述するための基本語彙〈ボキャブラリー〉が必要です。基本語彙の定義には指標〈signature〉と呼ばれる形式が使われます。以下が、「lengthらしさ」を記述するための基本語彙を定義する指標です*1。

signature ListAndLength{
  type X  in Set

  function nilX : 1 -> List(X)  in Set
  function consX : X×List(X) -> List(X)  in Set

  function lengthX : List(X) -> Z  in Set
}

指標〈signature〉はインスティチューション理論の用語ですが、プログラミング用語ならインターフェイス〈interface〉です。length以外に、nil, cons という名前も宣言しています。下付きのXは省略してもかまいません。

上記指標によって準備された基本語彙（nil, cons, length）を使って「lengthらしさ」を記述する文を書いてみます。

  1. 文1： length(nil(1)) = 0
  2. 文2： ∀x∈X.∀z∈List(X).( length(cons(x, z)) = lengt(z) + 1 )

1 = {1} として、nil : 1 → List(X) なので nil(1) と書いてますが、単に nil() あるいは nil だけでもかまいません。

文1, 文2 に出てくるlengthはプレースホルダーなので、A君が書いた実際の関数lengthByAが文1を満たすことは、次が成立することです。

  • lengthByA(nil(1)) = 0

ここで出てくるnilはプレースホルダーではなくて、事前に実装済みの実際の関数を指します。事前に実装済みの nil, cons が変な挙動をしたりすると話がややこしくなるので、常識的意味で nil, cons は“正しく”動くとします*2

文2の満足性ならば、次が成立することです。

  • ∀x∈Z.∀z∈List(Z).( lengthByA(cons(x, z)) = lengtByA(z) + 1 )

成立の確認には無限回のテストが必要なので、現実世界ではテストで完全な確認はできません。

もし、Xさんが文1と文2を満足させることを3人に要求していれば、「内心不満を感じながらも3人を叱るわけにもいきません」とはならなかったでしょう。

パラメトリック性と満足性

パラメトリック性＝自然性だとして、満足性は前節で説明した意味だとします。形式上は、パラメトリック性と満足性は別な性質です。しかし、「パラメトリック性が満足性も含意している」ような雰囲気があります。これは何故でしょう？

多相関数がパラメトリックであることの定義として「単一のプログラムコードで書ける」というのがあります。僕は、書くプログラミング言語／書き方によりけりなので、これは定義として使えないと思っています。が、ともかくも単一のプログラムコードで書いた多相関数があったとしましょう。その多相関数が、特定の型に対して（条件文で記述された）ある性質を持つとき、他の型に対しても同じ性質を持つことが期待できるでしょう。少なくとも、型ごとの複数のプログラムコードを寄せ集めた場合よりは期待できます。

この期待できる感じが、「パラメトリック性は満足性を含意する」雰囲気を作り出しているのではないでしょうか。

いずれにしても、「感じ」と「雰囲気」なので、正確な議論にはなりません。正確に議論するには、パラメトリック性＝自然性と満足性を別に定義して、その相互関係を調べることになります。

*1:標準的なキーワードは、type, function ではなくて、sort, operation ですが、キーワードに違和感を持つ人が多いので type, function にします。

*2:その「常識的意味で正しく」も、ほんとは論理式で定義すべきです。

蒸し返し： アドホック多相 vs パラメトリック多相

雑記／備忘

一年ほど前に「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない」という記事を書きました。多相性を二種類に分類できるわけではなくて、パラメトリック性（あるいはアドホック性）はしょせん程度問題だ、という話です。「関数定義がひとつで済む多相はパラメトリック多相」なんていう曖昧な定義はあまり意味がありません。

しょせん程度問題だとすると、その“程度”を測って比較したいとは思います。「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない // それでもマジメに考えたいのなら」に次のように書きました。

多相関数を自然変換として定式化して、自然変換のあいだの関係をアドホック性を計る尺度に用います。実際、いくつかの方法で自然変換のあいだの順序を定義できます。その順序は、アドホック性の程度とみなせます。

上記の方法でパラメトリック性（アドホック性）を実際に測って比較してみます。

内容：

例題はlength関数

例題として、リストの長さを求める関数lengthを考えます。多相関数としてのlengthを、型理論では割と標準的（でHaskell風の）書き方で導入します。

lengthの入出力の仕様〈プロファイル〉は次のように宣言されます。

  • length :: \forall\alpha. \mathrm{List}\, \alpha \to Int

コロン2個はHaskellの構文で、普通の（多数派の）記法ならコロン1個です。また、型理論の習慣として、型を表す変数はギリシャ小文字にします。なので、αは型変数〈型パラメータ〉です。関数が、単一の型ではなくて色々な型に適用可能であることを記号'∀'を使って表します。'∀'は、もともとは記号論理の全称限量子〈universal quantifier〉の記号です。僕は、ここに'∀'を使うのは好きではありません、だって論理の'∀'と似てないもんね。まー、意味ではなくて単に記号だけテキトーに借用していると解釈しましょう。「∀α. ‥‥」は、「色々な型αに関して ‥‥」と読みます。

\mathrm{List}\, \alpha は、型αの項目〈成分 | 要素〉からなるリストの型です。型構成子〈type constructor〉であるListはローマン体で書きます（そういう習慣もある、というだけ）。Intは整数型です（具体的な型名はラテン大文字始まりの名前、という約束）。よって、上の記号的表現は次のように読めます。

  • length は、色々な型αに関して、型αの項目からなるリストの型から整数型への関数である。

特定の型ξに対するlengthのインスタンス（型パラメータの具体化）は lengthξ のように書きます。下付きが書けないときは、length<ξ>, length[ξ] などとします。

多相関数lengthがパラメトリックであること〈parametricity property〉は次の等式で表現します。

  • length_\beta \,(map\, f\, x) = length_\alpha\, x \:\:\:\:\mbox{for }f :: \alpha \to \beta

ここで、map（fmapと書かれることも多い）は、List型構成子にともなうマップ化高階関数で、任意の関数 f::α → β（普通の書き方なら f:α → β）を引数として新しい関数 map f = map(f) : List α → List β を返します。

上の等式は、マップ化高階関数でマップ化した関数を適用した後でもリストの長さは変わらないことを主張しています。

自然変換としてのlength関数

List型構成子の引数となる型は集合と解釈しましょう。よく使う型は：

型 対応する集合
Bool {True, False}
Int Z
Real*1 R
Char Ch = (Unicodeのすべての文字からなる集合)

集合圏をSetとすると、List型構成子は List:|Set| → |Set| とみなせます。List(f) := map(f) とすれば、ListはSet上の自己関手になります。

  • List:Set → Set は関手。

別な関手KZを次のように定義します。

  • For X∈|Set|, KZ(X) := Z
  • For X, Y∈|Set|, f:X → Y in Set, KZ(f) := idZ

多相関数lengthは、関手Listから関手KZへの自然変換として定義します。

  • length::List ⇒ KZ:Set → Set

ここでのコロン2個は、Haskellの構文とは関係ありません。自然変換は、“圏の圏”の2-射なのでコロンを2個（矢印も二重）にしています。まったく違った習慣からのコロン2個です。lengthが自然変換であるためには、次の可換図式が要求されます。

\require{AMScd} \forall f:X \to Y \:\mbox{ in }{\bf Set} \\ \:\\ \begin{CD} \mathrm{List}(X) @>{length_X}>> \mathrm{K}_{\bf Z}(X) \\ @V{\mathrm{List}(f)}VV @VV{\mathrm{K}_{\bf Z}(f)}V \\ \mathrm{List}(Y) @>{length_Y}>> \mathrm{K}_{\bf Z}(Y) \\ \end{CD} \\ \:\\ \mbox{commutative in }{\bf Set}

関手KZの定義から簡略化できて：

\forall f:X \to Y \:\mbox{ in }{\bf Set} \\ \:\\ \begin{CD} \mathrm{List}(X) @>{length_X}>> {\bf Z} \\ @V{\mathrm{List}(f)}VV @| \\ \mathrm{List}(Y) @>{length_Y}>> {\bf Z} \\ \end{CD} \\ \:\\ \mbox{commutative in }{\bf Set}

この可換図式を等式で書けば：

  • \forall( f:X \to Y \:\mbox{ in }{\bf Set}).(length_Y \circ \mathrm{List}(f) = length_X )

これは、書き方が多少違うだけで、パラメトリック性を表す等式（下に再掲）と同じです。

  • length_\beta \,(map\, f\, x) = length_\alpha\, x \:\:\:\:\mbox{for }f :: \alpha \to \beta

つまり：

  • 多相関数とは自然変換のことである。
  • パラメトリック性とは自然性〈naturality〉のことである。

これで、多相関数とそのパラメトリック性を圏論の枠組みで議論する準備ができました。

Haskell風 vs 圏論風

二種類の書き方が混じっていたので、おおよその翻訳を示しておきます。

Haskell風 圏論風
\alpha, \beta, \cdots A, B, ..., X, Y
Int Z
Float, Double R
f:: \alpha \to \beta f:X → Y または f:1 → [X, Y]
f:: \alpha \to \beta \to \gamma f:X → [Y, Z] または f:1 → [X, [Y, Z]]
f \,x f(x) または x;f または ev(f, x)
\mathrm{List}\,\alpha List(X) （Xは対象）
map\, f List(f) （fは射）
f::\forall\alpha. \mathrm{List}\,\alpha \to \beta ψ::List ⇒ KY （自然変換）
f_\xi :: \mathrm{List}\,\xi \to \beta ψA:List(A) → Y （自然変換の成分）

前節でも注意したように圏論風のコロン2個は自然変換だからです。正確には、ψ::List ⇒ KY:Set → Set （集合圏の自己関手のあいだの自然変換）です。プログラミング言語だと関手（型構成子とマップ化関数）の域・余域を記述できる機能はあまり見かけないです*2。

実数に Float, Double があるのはコンピュータ特有の事情なので、Rに対応する型は（実際とは違い） Real とすることにします（前節でRealを既に使っている）。以下では、主に圏論風記法を使うことにします。が、プログラミング的文脈では、テキトーな疑似コードを使います。

3人のプログラマにlengthを作ってもらう

3人のプログラマ、A君、B君、C君がいます。上司のXさんが次の指示を出しました。

  • A君に： length : List<Int> -> Int という関数を書け。
  • B君に： length : List<Char> -> Int という関数を書け。（List<Char> は文字列型）
  • C君に： length : List<Real> -> Int という関数を書け。

A君とB君は、リストの項目〈要素 | 成分〉の個数を勘定する関数を書きました。C君は次の定義に基づきlength関数を書いたとします。

\mathrm{round}\left(\sqrt{ {x_1}^2 + {x_2}^2 + \cdots + {x_n}^2}\right)

つまり、List<Real>（List(R)）の要素をn次元ユークリッド空間のベクトルだと解釈し、その長さ（ユークリッド・ノルム）を求めたのです。ユークリッド・ノルムそのままだと実数なので四捨五入して整数にしています。

A君、B君、C君が作ったlength関数を、一旦それぞれ別な名前にして、Xさんが1つの関数にまとめたとしましょう。

function length<Int> = lengthByA
function length<Char> = lengthByB
function length<Real> = lengthByC

型引数の具体化は、呼び出し時に明示的に指定（length<Char>("hello") のように）してもいいし、コンパイラが型推論して補ってくれると考えてもいいです。あるいは、実行時の型場合分け〈type case〉が使えるとして：

function length = lambda(x) {
  typecase (x) {
     List<Int> => lengthByA(x)
     List<Char> => lengthByB(x)
     List<Real> => lengthByC(x)
  }
}

いずれにしても、項目の型が Int, Char, Real であるリストに適用可能な多相関数lengthができました。この多相関数は、その作り方からいってアドホックです。型ごとの担当者は、関数名の印象だけから勝手に実装しています。A君とB君が共通の仕様の関数を実装したのは偶然です*3。

今定義したlengthは、パラメトリック性 -- つまり自然性を持つでしょうか？

部分圏と自然性

多相関数lengthの自然性の条件を下に再掲します。

\forall f:X \to Y \:\mbox{ in }\mathcal{C} \\ \:\\ \begin{CD} \mathrm{List}(X) @>{length_X}>> K_{\bf Z}(X) \\ @V{\mathrm{List}(f)}VV @VV{K_{\bf Z}(f)}V \\ \mathrm{List}(Y) @>{length_Y}>> K_{\bf Z}(Y) \\ \end{CD} \\ \:\\ \mbox{commutative in }{\bf Set}

最初に出した条件と一箇所だけ違いがあって、最初の行の「圏Set」が「圏C」に変わっています。考えるべき関手 List, KZ が、Set → Set ではなくて、C → Set でもいいとしています。ただし、CはSetの部分圏であり、もとの List, KZ を部分圏に制限して考えます。

Setの部分圏S1を次のように定義します。Chは型Charに対応する集合でした。

  • |S1| := {Z, Ch, R}
  • For X, Y∈|S1|, S1(X, Y) := Set(X, Y)
  • 射の結合と恒等射はSetと同じ。

S1は3つの対象を持つSetの部分圏です（充満部分圏と呼ばれます）。すぐ上の自然性の条件において、C = S1 と置いたとき、自然性は成立するでしょうか？ ダメですね。例えば、f:Z → R として単純・常識的な埋め込み写像をとるとき length<Int>( (3, 3) ) と length<Real>( (3, 3) ) は一致しません。

「あー、やっぱりアドホックだな」と思うでしょう。しかし、部分圏S2を次のように定義することもできます。

  • |S2| := {Z, Ch, R}
  • For X, Y∈|S2|,
    S2(X, X) := {idX}
    X ≠ Y ならば S2(X, X) := {}
  • 射の結合と恒等射はSetと同じ。

S2も3つの対象を持つSetの部分圏です（離散部分圏と呼ばれます）。C = S2 と置いたとき、自然性は成立します。\forall f:X \to Y \:\mbox{ in } {\bf S2} において選べるfが、idZ, idCh, idR しかなく、図式が可換となるのは自明です。

S1とS2の中間の圏として、部分圏S3を定義してみます。

  • |S3| := {Z, Ch, R}
  • ホムセット
    • X, Y∈{Z, Ch} ならば、S3(X, Y) = Set(X, Y)
    • S3(R, R) = {idR}
    • その他の S3(X, Y) = {}
  • 射の結合と恒等射はSetと同じ。

S2 でもlengthの自然性は成立します。

多相関数を構成する関手と写像の族に対して、定義域となる圏の取り方を変えると、自然性（＝パラメトリック性）は成立したりしなかったりします。

部分圏に相対的なパラメトリック性

次の状況を考えましょう。

  1. F, G:Set → Set は関手。
  2. Kは集合の集合。同じことだが K⊆|Set| 。
  3. ψ:K → Mor(Set) つまり、ψは、Kの要素（それは集合）でインデックスされた関数の族。
  4. dom(ψX) = F(X), cod(ψX) = G(X) 。
  5. C, D などはSetの部分圏で、|C| = |D| = K 。

前節の話はこの状況になっています。

  1. List, KZ は関手。
  2. {Z, Ch, R} は集合の集合。
  3. length:{Z, Ch, R} → Mor(Set) は、{Z, Ch, R} の要素でインデックスされた関数の族。
  4. dom(lengthX) = List(X), cod(lengthX) = KZ(X) 。
  5. S1, S2, S3 はSetの部分圏で、|S1| = |S2| = |S3| = {Z, Ch, R} 。

一般的に、ψが自然性を持つか（自然変換になっているか）は、部分圏Cの選び方によります。ある部分圏Cに対してψが自然性を持つとき次のように書きましょう。

  • ψ is-natural-on C

「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない」の脚注として次のように書きました。

アドホック多相関数は自然変換にならない、と思っている人がいるかも知れません。そんなことはありません。アドホック多相関数（と呼ばれているもの）でも自然変換に仕立てることができます。

部分圏Cを離散圏に取れば、離散圏Cに対して、ψ is-natural-on C は必ず成立します。どんなにアドホックな多相関数でも、離散圏に対してはパラメトリック〈自然〉なのです。しょせん程度問題です。

今述べたセッティングでは、パラメトリックな程度（アドホックな程度）は、ψ is-natural-on C となる部分圏Cの“大きさ”で測れます。それは、そういう基準で計ると約束したからです。パラメトリック性（アドホック性）を別な基準で計ることもあるでしょう。圏論を使わない基準もあるかも知れません。ですが、基準をハッキリと決めないで「アドホック vs パラメトリック」と言っても、それは無意味です。

*1:Realについは次の節に書いてあります。

*2:自然変換の生息地〈habitat | アビタ〉は、圏の圏CATです。自然変換の記述をさらに正確にすると、ψ::List ⇒ KY:Set → Set in CAT。プログラミング言語のデータ型の世界をCATまで広げるのは大変ではあります。

*3:「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない」では、「たまたま"square"という同じ名前で呼ばれる3つの関数」「たまたま"increase"という同じ名前で呼ばれる2つの関数」の例を出しています。