多相型／多相関数の表現に使われる全称記号を僕はずっと嫌っています。その理由を説明します。理屈っぽい話に興味がないなら、最後の節だけで「しゃくに障るワケ」は分かるでしょう。$`\newcommand{\mrm}[1]{\mathrm{#1} }
% \newcommand{\cat}[1]{\mathcal{#1} }
%\newcommand{\id}{\mathrm{id}}
\newcommand{\In}{\text{ in }}
\newcommand{\Iff}{\Leftrightarrow }
\require{color} % 緑色
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
\newcommand{\Where}{\Keyword{Where } }%
%`$
内容：
嫌ってる
多相関数を表すために論理の全称記号を使うことがあります。例えば次のようです。
$`\quad \mrm{length}:: \forall \alpha. \mrm{List}\;\alpha \to \mrm{Int}
`$
この全称記号を引き合いに出すたびに文句と愚痴を言っています。
2008年「型パラメータと総称：どうしたらわかりやすい構文になるのかな」より：
型の抽象に論理記号∀を使う例があったような気がしますけど、僕はそれ嫌い。
2020年「蒸し返し： アドホック多相 vs パラメトリック多相」より：
'∀'は、もともとは記号論理の全称限量子〈universal quantifier〉の記号です。僕は、ここに'∀'を使うのは好きではありません、だって論理の'∀'とあんまり似てないもんね。まー、意味ではなくて単に記号だけテキトーに借用していると解釈しましょう。
2020年「多相関数と依存型をちゃんと理解しよう」より：
'∀'は論理の全称記号ですが、単に記号を借用しているだけです。誤解と混乱を避けるためには、いったんは全称記号とのアナロジーを断ち切ったほうが無難です。
2022年「多相関数の書き方」より：
ここで論理の全称記号を流用するのはやめて欲しい。確かに雰囲気は似てるけど、でもやめて欲しい。そう思う合理的な理由はありません。感情としてイヤなのね。
2022年「Functor型クラスの型インスタンスは関手なのか？」より：
その旨を、論理の全称記号〈総称記号〉を流用して次のように書くのが習慣です（僕はこの習慣嫌いですけど）。
けっこうよく使われる記法なので、無視するわけにもいかず僕も紹介するのですが、そのたびにいまいましい気分になって一言付け加えたくなるわけです。
なぜ？
“多相／総称”の“型／関数”の文脈で出てきた全称記号を、論理の全称記号とのアナロジーで考えてみても、理解を促すことはありません。むしろ、誤解や困惑へと導かれます。ろくなもんじゃない。
さらにタチが悪い点は、論理の全称記号とは「何の関係もない」とは言い切れない、あるいは「何の関係もない」と言い切ったときに後ろめたい気分になることです。フントニモウ、しゃくに障る！
そこでこの記事で、100%無関係とも言えない微妙な部分を解説して、「それはそうなんだが、やっぱり気にいらない」と再度言っておきたい -- 「多相関数の書き方」に書いたように、もはや感情論になってしまっているようです。
パイ型としての解釈
リストの長さを求める関数と、リストの最初の成分〈要素 | 項目〉を取り出す関数を例にします。
$`\quad \mrm{length}:: \forall \alpha. \mrm{List}\;\alpha \to \mrm{Int}\\
\quad \mrm{first}:: \forall \alpha. \mrm{List}\;\alpha \to \mrm{Maybe}\; \alpha
`$
ギリシャ文字の $`\alpha`$ は型変数です。$`\mrm{List}, \mrm{Maybe}`$ はよく知られたモナドですが、モナドと考える必要はなくて、単なる自己関手と思えば十分です。さらに退化させて、単なる型構成子〈型コンストラクタ〉だとしてもかまいません、以下そう考えます。
上記の書き方はHaskell風です。「Haskellの二重コロン「::」とバインド記号「>>=」の説明」に書いたように、この記法の集合圏 $`{\bf Set}`$ における解釈は次のようです。
$`\quad \mrm{length} :{\bf 1} \to \forall \alpha. [\mrm{List}(\alpha), \mrm{Int}] \In {\bf Set}\\
\quad \mrm{first} :{\bf 1} \to \forall \alpha. [\mrm{List}(\alpha), \mrm{Maybe}(\alpha)]\In {\bf Set}
`$
ここで、$`{\bf 1}`$ は単元集合で、$`[-, -]`$ は集合の指数なので関数〈写像〉集合のことです。より分かりやすく書けば次のようです。
$`\quad \mrm{length} \in \forall \alpha. \mrm{Map}(\mrm{List}(\alpha), \mrm{Int})\\
\quad \mrm{first} \in \forall \alpha. \mrm{Map}(\mrm{List}(\alpha), \mrm{Maybe}(\alpha))
`$
ここまで来れば、論理の全称記号の形はしているがその実体が謎である $`\forall \alpha.`$ の意味をハッキリさせればいいわけです。
結論を言えば、記号 $`\forall`$ をギリシャ文字大文字 $`\Pi`$ に置き換えれば解釈が可能です。
$`\quad \mrm{length} \in \Pi \alpha. \mrm{Map}(\mrm{List}(\alpha), \mrm{Int})\\
\quad \mrm{first} \in \Pi \alpha. \mrm{Map}(\mrm{List}(\alpha), \mrm{Maybe}(\alpha))
`$
大文字パイは、依存型のパイ型を表します。パイ型については次節で簡略に説明しますが、詳しいことは「多相関数と依存型をちゃんと理解しよう」を参照してください。
パイ型のインスタンス
型変数 $`\alpha`$ はどんな範囲を動くでしょうか？ 神様なら、$`\alpha : |{\bf Set}|`$ と考えるでしょう。しかし我々人間は、すべての集合の類である $`|{\bf Set}|`$ を見渡すことはできないので、なにかささやかな集合の集合 $`{\bf T}\subseteq |{\bf Set}|`$ をとりましょう（神様のつもりになって $`{\bf T} = |{\bf Set}|`$ でもかまいませんが）。そして、 $`\alpha : {\bf T}`$ と考えます。$`{\bf T}`$ 上を走る変数としては、ギリシャ文字だけではなくて、普通の $`A, B, X`$ なども使います。ギリシャ文字を使うのは伝統ですが、伝統に特段の意味はありません。
さて、パイ型（の表現）の内側に出てくる式は集合を表します。型変数は集合変数だとすると、次のような“集合に集合を対応させる関数”があります。
$`\quad {\bf T}\ni X \mapsto \mrm{Map}(\mrm{List}(X), \mrm{Int}) \;\in |{\bf Set}|\\
\quad {\bf T}\ni X \mapsto \mrm{Map}(\mrm{List}(X), \mrm{Maybe}(X)) \;\in |{\bf Set}|
`$
集合 $`X`$ が確定すれば、値となる集合も決まります。「決まれば決まる」ので関数〈写像〉です、名前は付いてませんが。
$`a, b`$ が前節のパイ型のインスタンスであるとは、それぞれ次のような関数であることです。
$`\quad {\bf T}\ni X \mapsto a(X) \text{ where } a(X) \in \mrm{Map}(\mrm{List}(X), \mrm{Int})\\
\quad {\bf T}\ni X \mapsto b(X) \text{ where } b(X) \in \mrm{Map}(\mrm{List}(X), \mrm{Maybe}(X))
`$
変数 $`X`$ が型〈集合〉であることから、$`a_X := a(X),\; b_X := b(X)`$ と書いたほうが混乱が少ないでしょう。
$`\quad {\bf T}\ni X \mapsto a_X \text{ where } a_X : \mrm{List}(X) \to \mrm{Int}\\
\quad {\bf T}\ni X \mapsto b_X \text{ where } b_X : \mrm{List}(X) \to \mrm{Maybe}(X)
`$
上記の記述内容を自然言語〈日本語〉で書けば：
- $`a`$ が $`\Pi \alpha. \mrm{Map}(\mrm{List}(\alpha), \mrm{Int})`$ のインスタンスであるとは： 型〈集合〉の集合 $`{\bf T}`$ に属する型 $`X`$ に対して、関数 $`a_X`$ が割り当てられている。関数 $`a_X`$ のプロファイル（域と余域の仕様）は $`\mrm{List}(X) \to \mrm{Int}`$ である。
- $`b`$ が $`\Pi \alpha. \mrm{Map}(\mrm{List}(\alpha), \mrm{Maybe}(\alpha))`$ のインスタンスであるとは： 型〈集合〉の集合 $`{\bf T}`$ に属する型 $`X`$ に対して、関数 $`b_X`$ が割り当てられている。関数 $`b_X`$ のプロファイル（域と余域の仕様）は $`\mrm{List}(X) \to \mrm{Maybe}(X)`$ である。
関数 $`\mrm{length}`$ は、$`a`$ のような関数の実例であり、関数 $`\mrm{first}`$ は、$`b`$ のような関数の実例です。
論理の全称記号をそれらしく使うならば、次のような書き方のほうがいいと思いますね。
$`\forall X\in {\bf T}.\\
\quad \mrm{length}_X : \mrm{List}(X) \to \mrm{Int}\\
\forall X\in {\bf T}.\\
\quad \mrm{first}_X : \mrm{List}(X) \to \mrm{Maybe}(X)
`$
これならば、（プロファイルは、域と余域に関する命題とみなせるので）述語論理の論理式だと思えます。
$`\forall X\in {\bf T}.\\
\quad \mrm{dom}(\mrm{length}_X) = \mrm{List}(X)
\,\land\, \mrm{cod}(\mrm{length}_X) = \mrm{Int}\\
\forall X\in {\bf T}.\\
\quad \mrm{dom}(\mrm{first}_X) = \mrm{List}(X)
\,\land\, \mrm{cod}(\mrm{first}_X) = \mrm{Maybe}(X)
`$
実際は、こういう意味で全称記号を使っているわけではなくて、パイ型を作る束縛子である $`\Pi`$ を $`\forall`$ で代用しているだけです。
Σ-Δ-Π随伴
ここから先は、圏論と論理についてのある程度の予備知識が必要です。
前節で出てきた $`{\bf T}\ni X \mapsto \mrm{Map}(\mrm{List}(X), \mrm{Int})`$ などは、集合 $`{\bf T}`$ をインデックス集合（あるいはパラメータ集合）とする集合族〈{indexed | parameterized} family of sets〉です。その正体は次のような関数〈function | 写像 | map〉です。
$`\quad F:{\bf T} \to |{\bf Set}|\:\: (\text{function})`$
集合は離散圏とみなせるので、$`{\bf T}`$ を離散圏とみなした圏を $`\delta{\bf T}`$ と書くと、$`F`$ は関手〈functor〉です。
$`\quad F:\delta{\bf T} \to {\bf Set}\:\: (\text{functor})`$
圏論の言葉でいえば、この関手の極限がパイ型で、余極限がシグマ型です。
$`\quad \Pi_{\bf T}(F) = \mrm{lim}_{\delta{\bf T}}\, F\;\in |{\bf Set}|\\
\quad \Sigma_{\bf T}(F) = \mrm{colim}_{\delta{\bf T}}\, F \;\in |{\bf Set}|
`$
パイ型／シグマ型には別な圏論的見方もあります。Σ-Δ-Π随伴トリプルです。パイ型／シグマ型を作るパイ構成／シグマ構成を関手とみなすと、自明引き戻し関手Δを入れて随伴トリプル〈随伴トリオ〉を形成します。まず、随伴系のためのセッティングをしましょう。
$`{\bf T}`$ をインデックス集合とする集合族〈ファミリー〉の圏と、$`\delta{\bf T}`$ から集合圏への関手達／自然変換達の関手圏は同じものですから、次のように置きます。以下のブラケット $`[-, -]`$ は（関数集合ではなくて）関手圏です。
$`\quad {\bf Fam}[{\bf T}] = [\delta{\bf T}, {\bf Set}]`$
単元集合 $`{\bf 1}`$ 上のファミリーは単なる集合と同一視できるので、次は明らかでしょう。
$`\quad {\bf Fam}[{\bf 1}] \cong {\bf Set}`$
唯一の写像 $`!_{\bf T} : {\bf T} \to {\bf 1}`$ により、$`{\bf 1}`$ 上のファミリー（事実上単一の集合）は $`{\bf T}`$ 上のファミリーに引き戻されます。（プレ結合で）引き戻されたファミリーとは定数値ファミリーです。この引き戻し関手を $`\Delta`$ とします。
$`\quad \Delta : {\bf Fam}[{\bf 1}] \to {\bf Fam}[{\bf T}] \In {\bf CAT}`$
パイ構成／シグマ構成を行う $`\Pi_{\bf T}(-), \Sigma_{\bf T}(-)`$ を $`\Pi, \Sigma`$ と略記するとして、これらも関手になります。
$`\quad \Pi : {\bf Fam}[{\bf T}] \to {\bf Fam}[{\bf 1}] \In {\bf CAT}\\
\quad \Sigma : {\bf Fam}[{\bf T}] \to {\bf Fam}[{\bf 1}] \In {\bf CAT}
`$
これらの3つの関手達は、次のような随伴トリプルを形成します。
$`\quad \Sigma \dashv \Delta \dashv \Pi`$
随伴によるホムセット同型は次のようになります。
$`\For F \in |{\bf Fam}[{\bf T}]|\\
\For A \in |{\bf Fam}[{\bf 1}]|\\
\quad {\bf Fam}[{\bf 1}](\Sigma(F), A) \cong {\bf Fam}[{\bf T}](F, \Delta(A))\\
\quad {\bf Fam}[{\bf 1}](A, \Pi(F)) \cong {\bf Fam}[{\bf T}](\Delta(A), F)
`$
Σ-Δ-Π随伴トリプルについては、以下の過去記事でも書いています。
∃-Δ-∀随伴
二値真偽値〈ブール値〉の集合を $`{\bf B}`$ とします。$`{\bf B}`$ は普通通りにブール代数と考えて、論理順序を $`\le`$ で表します。集合 $`X`$ 上の述語の集合を $`\mrm{Pred}[X]`$ とします。
$`\quad \mrm{Pred}[X] := \mrm{Map}(X, {\bf B})`$
ブール値関数の集合である $`\mrm{Pred}[X]`$ にもブール代数の構造を入れます。論理順序は次のように定義できます。
$`\For p, q \in \mrm{Pred}[X]\\
\quad p \le q :\Iff \forall x\in X. p(x) \le q(x)
%`$
単元集合 $`{\bf 1}`$ 上の述語は単なるブール値と同一視できるので、次は明らかでしょう。
$`\quad \mrm{Pred}[{\bf 1}] \cong {\bf B}`$
唯一の写像 $`!_X : X \to {\bf 1}`$ により、$`{\bf 1}`$ 上の述語（事実上単一のブール値）は $`X`$ 上の述語に引き戻されます。引き戻された述語とは、常に真、または常に偽の定数値述語です。この引き戻し関数を $`\Delta`$ とします。
$`\quad \Delta : \mrm{Pred}[{\bf 1}] \to \mrm{Pred}[X] \In {\bf Set}`$
述語から全称命題／存在命題を作る操作を限量子記号とオーバーロードして $`\forall, \exists`$ で表すと、これらは次の関数〈写像〉になります。
$`\quad \forall : \mrm{Pred}[X] \to \mrm{Pred}[{\bf 1}] \In {\bf Set}\\
\quad \exists : \mrm{Pred}[X] \to \mrm{Pred}[{\bf 1}] \In {\bf Set}
`$
これらの3つの関数達は、次のような随伴トリプルを形成します。
$`\quad \exists \dashv \Delta \dashv \forall`$
順序による随伴系はガロア接続なので、ホムセット同型は不等式の同値性で書けます。
$`\For p \in \mrm{Pred}[X]|\\
\For a \in \mrm{Pred}[{\bf 1}]| \cong {\bf B}\\
\quad \exists(p) \le a \Iff p \le \Delta(a)\\
\quad a \le \forall(p) \Iff \Delta(a) \le p
`$
ガロア接続については：
ここまでの議論を前節と比較してもらえれば、ソックリなことが分かるでしょう。Σ-Δ-Π随伴トリプルと∃-Δ-∀随伴トリプルのあいだの具体的な対応を作ることもできます。
結局、それで
“多相／総称”の“型／関数”の文脈で出てくる全称記号 $`\forall`$ はパイ型の束縛子 $`\Pi`$ と同義でした。Σ-Δ-Π随伴トリプルと∃-Δ-∀随伴トリプルのあいだの対応では、$`\Pi`$ は $`\forall`$ に対応します。この事実をもって、$`\forall`$ 使用の正当性を主張されると、僕はグヌヌヌヌとなって言い返せないでしょう。
ここ、ここがしゃくに障るのよ。ろくでもない記法だな、と思うわけだけど、持って回った正当化の可能性は担保されているというこざかしさ。グヌヌヌヌ、しゃらくせーわい。
