多相関数と型クラス - 檜山正幸のキマイラ飼育記 (はてなBlog)

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

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

2020年9月7日蒸し返し：アドホック多相 vs パラメトリック多相
2020年9月8日多相関数の「パラメトリック性 vs 満足性」

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

2016年9月28日入門的ではない型クラスの話：Haskellの型クラスがぁ (´^｀;)

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

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

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

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

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

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

内容

指標：いつもの事例で
多相関数＝関手間部分変換
自然性と保存性
心にモノイド、コードは付点マグマ
指標のモデル
指標に従うモダリティ

指標：いつもの事例で

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

従来（伝統的）	より親しみやすい
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×id_U);m = id_U
  ‥‥ 略 ‥‥
}

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

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 パラメトリック多相 // 部分圏に相対的なパラメトリック性」の復習をします。次の状況を考えるのでした。

F, G:Set → Set は関手。
Kは集合の集合。同じことだが K⊆|Set| 。
ψ:K → Mor(Set) つまり、ψは、Kの要素（それは集合）でインデックスされた関数の族。
dom(ψ_X) = F(X), cod(ψ_X) = G(X) 。
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) := id_A, G(X) := B, F(g) := id_B と2つの関手 F, G を定義して、K := {1} に対して、ψ:K → Mor(Set) を次のように定義します。

ψ₁ := f

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

自然性と保存性

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)K₁ ⇒ Id という多相関数εを考えましょう。おっと、文字'K'がコンフリクト（偶発的・不注意による衝突）してしまいましたが、んなことは気にしない。ここで：

K₁(A) := 1, K₁(f) := id₁
Id(A) := A, Id(f) = f

多相関数 ε:.(K)K₁ ⇒ 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つあります。

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

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

指標に従うモダリティ

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

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

Title: Supplying bells and whistles in symmetric monoidal categories
Authors: Brendan Fong, David I Spivak
Pages: 17p
URL: https://arxiv.org/abs/1908.02633

しかし僕は装備〈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つの多相関数を定義するのと同じことです。

μ:.(|C|) (-×-) ⇒ Id
ε:.(|C|) K₁ ⇒ Id

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

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

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

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