2020年9月に書いた一連の記事があります。
これらは多相関数に関する記事です。昨日の記事も多相関数を扱っています。
9月のシリーズ記事と昨日の記事では、多相関数の定義が違います。これは混乱を招くかも知れないので、この記事で追加の説明をしておきます。
内容:
定義はTPO依存
同じ言葉を複数の記事で使い、それらの定義がズレていたのですが、僕はそれが悪いとは思っていません。ただ、関連性が強い記事で異なる定義を採用していると混乱を招くリスクがあるので、断り書きはするべきでしょう。
言葉と定義に関する僕のスタンスは何度か書いているので、「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない」から引用します。
「オーバーロード」、「多相」、「総称」はプログラミングの文脈で出現する(ことが多い)言葉ですが、そういう言葉はだいたい、プログラミング言語ごとに定義が違うのです。方言がたくさんあって、標準語はない状況なんですね。そんな状況で、「俺が使っている言葉こそは標準語だ」と訴えるのは無意味であり、ひんしゅくを買うだけです。
(脚注: プログラミングの文脈に限らず、専門用語の定義は、その用語を使う集団のローカルルールにより支えられています。よって、「これこそがスタンダード」のような物言いは、頭の悪さを印象付けてしまうので注意しましょう。)
TPOという古い言葉(死語か?)があります。Time Place Occasion のことです。技術的な専門用語であっても、言葉の選択と定義はTPO依存です。
9月のシリーズ記事では、「アドホック多相 vs パラメトリック多相」が主題だったので、その話題を展開しやすいように「多相関数」を定義しています。一方、昨日の記事は「依存型」を紹介したかったので、依存型との関係のなかで「多相関数」を定義しています。
そういう事情で異なる定義を採用しているのですが、大きな違いはありません。容易に統合できます。以下では、9月のシリーズ記事と昨日の記事の「多相関数」を包摂するような一般的な定義を紹介します。
関手性と自然性
本題に入る前に、ずっと困っていることがあってね、僕の愚痴を聞いてください。今日の話題に無関係な愚痴じゃないです。
C, D が圏だとして、関手 F:C → D があるとき、Fの対象パートを Fobj:|C| → |D|、Fの射パートを Fmor:Mor(C) → Mor(C) としましょう(Gでも同じ)。α::F ⇒ G:C → D は自然変換だとして、αのX-成分は αX:F(X) → G(X) in D とします。X αX という対応が自然変換の実体だとすると、αは写像 α:|C| → Mor(D) だといえます。
写像としての Fobj, Fmor, Gobj, Gmor, α のあいだには次の関係(図式の可換性)があります。図式を考える圏は、大きな集合も含む集合圏SETです。
上の図式の可換性だけでなくて、FとGが関手であること=関手性と、αが自然変換であること=自然性が要求されます。だがしかし、関手性・自然性が不要、あるいは強すぎる状況があるんですよね。
上の図式の可換性だけは仮定して、自然性を仮定しない、あるいは関手性と自然の両方とも仮定しないで議論したいことがあるのです。関手じゃないとダメ、自然変換じゃないとダメと言われると困るんです。てなことを以前に書いたことがあります。
この過去記事では、「非関手的対応」「非自然変換」という言葉を使ったのですが、どうも誤解されそう。例えば「非自然」という言葉は「自然性をまったく満たしてない、満たしてはいけない」という意味ではなくて、「必ずしも自然でなくてもよい〈... is not necessary to be natural〉」の意味です。が、「非」が持つ自然言語的印象から誤解をまねくリスクは高いですよね。
それがあって、「多相関数と型クラス // 多相関数=関手間部分変換」では、「非自然変換」の代わりに「関手間部分変換」を使いました。が、「部分」の意味がまた「必ずしも全域でなくてもよい〈... is not necessary to be total〉」なんですよねー、ウガッ。
それと、関手のあいだの非自然変換なら「関手間部分変換(全域を許容)」でいいですが、非関手対応のあいだの非自然変換を「関手間」というのはおかしいです。
ウダウダ述べましたが、僕の悩みは、「関手性は要求しない対応」「自然性は要求しない変換」を表す適切な言葉がないことです*1。「圏論的コンストラクタと圏論的オペレータ: 関手性・自然性の呪縛からの脱却」で出している言葉「コンストラクタ、オペレーター、コンビネータ」なども特殊な状況で使うもので、一般的な概念ではないです。
今回の記事では、非関手的対応は出てこないので、引き続き「関手間部分変換」あるいは「関手間変換」を使うことにします。
多相関数の少し一般的な定義
9月のシリーズ記事の「多相関数」と昨日の記事の「多相関数」を包摂するために、少し一般的な定義をします。すごく一般的ではないです。
D は集合圏Setの部分圏とします。用途によって、Dには適当な条件(例えばデカルト閉圏)を仮定します。Xは小さい圏とします。F, G:X → D は2つの(同一でもいいが)関手とします。
以上のセッティングで、fがFからGへの多相関数〈polymorphic function〉だとは、fが必ずしも自然とは限らない関手間変換であることです。自然性は要求しませんが、自然変換と同様に成分の集まりなので、次のように記述できます。
- f:|X| → Mor(D)
- dom(f(x)) = F(x)
- cod(f(x)) = G(x)
- 自然性は特に仮定しない。
習慣により f(x) を fx と書くと:
- For x∈|X|, fx:F(x) → G(x) in D
「少し一般的/すごく一般的ではない」と言ったのは、「Dは集合圏の部分圏」という条件を入れているからです。集合圏の部分圏であれば、集合と要素、写像という概念が使えて具体的な計算と議論ができます。これはメリットです。しかし、集合圏の部分圏という制約が邪魔になることはあります。
より一般的にしたいなら、Dを集合圏の部分圏に限定しない抽象的な圏(なんらかの条件を付けるのはアリ)にしたほうがいいでしょう。ときには、「Xは小さい」も外すほうがいいかも知れません。
9月の記事での多相関数
9月のシリーズ記事で使われている「多相関数」の意味は、「多相関数と型クラス // 多相関数=関手間部分変換」に端的に記述されています。
前節の“少し一般的な定義”との対応を書くと:
- D = Set と置く。
- X = C ⊆ Set
- |C| = K と置く。
- F, G:X → D は、F, G:C → Set 。ただし、F, G はSet上の自己関手のCへの制限だけを考える。
特徴的な制約は:
- Xとして一般的な(小さい)圏を考えるのではなくて、Setの部分圏だけを考える。
- X = C からの関手を、Set上の自己関手のCへの制限だけを考える。
昨日の記事での多相関数
“少し一般的な定義”との対応を書くと:
- D = C ⊆ Set
- X は離散圏に限定して、X = |X| と置く。
- F, G:X → D は、Xが離散圏なので、写像 X → |C| (型ファミリー)で考える。
特徴的な制約は:
- Xとして一般的な(小さい)圏を考えるのではなくて、離散圏だけを考える。
- Xからの関手を、|X| = X → |C| という写像(型ファミリー)で代用している。
パラメトリック性
9月のシリーズ記事の主題はパラメトリック性(あるいはアドホック性)でした。多相関数は、必ずしも自然とは限らない関手間対応なので、「どのくらい自然変換に近いのか?」が問題になります。自然変換との近さ、あるいは端的に自然性が(9月記事の文脈では)パラメトリック性です。
一方、昨日の記事はパラメトリック性=自然性を問題にしていません。多相関数=関手間変換は出てきますが、離散圏で定義された関手と関手間変換しか扱ってないので、出てくるすべての多相関数=関手間変換はパラメトリック=自然になっています。注意すべきは、離散圏におけるパラメトリック性はアドホック性でもあることです。9月のシリーズ記事で強調したように、パラメトリック性/アドホック性は程度問題なので、パラメトリック性とアドホック性が一致してしまう状況も存在します。
多相関数の定義をもっと一般化・抽象化すれば、パラメトリック性/アドホック性に関する(9月のシリーズ記事より)精密な分析も出来ます。それでも、パラメトリック性/アドホック性が相対的であり程度問題なことは変わりありません。
多相関数、パラメトリック性/アドホック性、型クラスの正確な定式化には、かなりの抽象化が必要です。曖昧で錯綜した印象は、抽象化が足りてないからでしょう。ここらの話題も気が向いたら書くかも知れません(誰も興味なさそうだが)。
*1:圏は、結合/恒等射を忘却すると反射的有向グラフ/有向グラフになるので、構造忘却した後の反射的有向グラフ射/有向グラフ射が、「関手性は要求しない対応」になります。反射的有向グラフ射/有向グラフ射のあいだの“変換”に名前を付ければいいのかな?