全称型／存在型のことを調べていて（「全称型？ 存在型？ ‥‥？？」参照）、気になったことがありました。
some（論理記号 ∃）と any（論理記号 ∀）がほぼ同じ意味で使われていたり、用法が逆転していたりが起きていて、これは何でだろう？ と疑問を感じました。
それと、指標（インターフェイス、型クラス、プロトコル、トレイト、コンセプト … などとも呼ぶ）を、型を制約する述語のように使っている場面があって、指標は述語じゃないのに、これは何でだろう？ と。
人が概念を誤認したり誤用するときは、誤認・誤用をさせるようなメカニズムが背後にあるのでしょう。それを探ってみます。存在型と呼ばれていた型の一部をヒルベルトのイプシロン記号で説明することを目標にします。その準備として、型クラス述語という概念を導入します。$`\newcommand{\cat}[1]{ \mathcal{#1}}
\newcommand{\mrm}[1]{ \mathrm{#1}}
\newcommand{\In}{ \text{ in }}
\newcommand{\Imp}{ \Rightarrow }
\require{color} % 緑色
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
\newcommand{\Where}{\Keyword{Where } }%
%`$
内容：
相互に関連する指標
様々なプログラミング言語において、指標〈signature〉に相当する概念が言語機能として使えます。それらは様々な呼ばれ方（冒頭参照）をしていて、機能性や用途に微妙な差があります。が、ここでは、プログラミング言語中立な概念としての指標を考えます。指標に関する短い説明は「全称型？ 存在型？ ‥‥？？ // 指標とモデル」、より詳しい説明は「指標と不完全インスタンス」、高次圏の場合は「高次圏を考慮した指標の書き方」参照。
指標のモデルは集合圏 $`{\bf Set}`$ 内で考えることにします。したがって、指標の構成素〈フィールド〉の実現〈概念的実装〉は、集合圏の対象（集合）／射（写像）／2-射（等式）になります。
指標の例を3つ挙げます。純粋なプレーンテキストではなくて、視認性・表現力向上のために太字を使っています（1 だけだけど）。法則は古典論理の論理式で書いています。
// 単なるひとつの集合の指標
signature SingleSet {
sort U
}
// 付点集合の指標
signature PointedSet {
sort U
operation e : 1 → U in Set
}
// モノイドの指標
signature Monoid {
sort U
operation m : U×U → U
operation e : 1 → U
laws:
∀x, y, z∈U. m(m(x, y), z) = m(x, m(y, z))
∀x∈U. m(e(), x) = x
∀x∈U. m(x, e()) = x
}
これらの指標のあいだには関連性があるように思えます。その関連性を明示するために“継承”風な構文で書いてみます。強調のために extends は色付き。
// 単なるひとつの集合の指標
signature SingleSet {
sort U
}
// 付点集合の指標
signature PointedSet extends SingleSet {
operation e : 1 → U in Set
}
// モノイドの指標
signature Monoid extends PointedSet {
operation m : U×U → U
laws:
∀x, y, z∈U. m(m(x, y), z) = m(x, m(y, z))
∀x∈U. m(e(), x) = x
∀x∈U. m(x, e()) = x
}
こう書くと、差分記述になって、繰り返し記述（記述のコピー）を避けられます。
継承風の書き方の代わりに、次のような書き方でもいいでしょう。強調のために base （後述）は色付き。
// モノイドの指標
signature Monoid extends PointedSet {
base sort U
operation m : U×U → U
base operation e : 1 → U
laws:
∀x, y, z∈U. m(m(x, y), z) = m(x, m(y, z))
∀x∈U. m(e(), x) = x
∀x∈U. m(x, e()) = x
}
キーワード base が付いた構成素〈フィールド〉は、基底指標〈base signature〉から受け継いだことをマークします。基底指標は書いてないし、名前も持ちませんが、base が付いた構成素〈フィールド〉を抜き出せば、基底指標を作れます。
// モノイドの指標の基底指標
// 無名だが、PointedSet と同じ
signature {
sort U
operation e : 1 → U
}
次の指標では、base の付け方を変えました。
// モノイドの指標
signature Monoid extends PointedSet {
base sort U
operation m : U×U → U
operation e : 1 → U
laws:
∀x, y, z∈U. m(m(x, y), z) = m(x, m(y, z))
∀x∈U. m(e(), x) = x
∀x∈U. m(x, e()) = x
}
base が付いた構成素〈フィールド〉を抜き出せば：
// モノイドの指標の基底指標
// 無名だが、SingleSet と同じ
signature {
sort U
}
継承風の書き方をするか、base で基底から継承した構成素をマークするかはどっちでもよくて、いずれにしても指標のあいだの関係性を明示できます。その関係性を記号 $`\preceq`$ で表します。継承風の書き方なら：
$`\quad \mathscr{X} \text{ extends } \mathscr{Y} \iff \mathscr{X} \preceq \mathscr{Y}`$
不等号だと思うと、継承の親のほうが“大きい”とみなします（単に恣意的な約束）。気にいらないのなら、不等号の向きを逆にするのはどうぞご自由に。
今までの例では：
- $`\text{Monoid} \preceq \text{PointedSet} \preceq \text{SingleSet}`$ （
extendsを使って） - $`\text{Monoid} \preceq \text{PointedSet}`$ （
baseを使って） - $`\text{Monoid} \preceq \text{SingleSet}`$ （
baseを使って）
base を使う方式でも、多段階の継承をシミュレートできます。
// モノイドの指標
signature Monoid extends PointedSet {
base base sort U
operation m : U×U → U
base operation e : 1 → U
laws:
∀x, y, z∈U. m(m(x, y), z) = m(x, m(y, z))
∀x∈U. m(e(), x) = x
∀x∈U. m(x, e()) = x
}
base が2つある構成素〈フィールド〉は、基底の基底から継承されたと考えます。
[/補足]
増強とhasImplOfWrt述語
2つの指標 $`\mathscr{X}, \mathscr{Y}`$ のあいだに、$`\mathscr{X} \preceq \mathscr{Y}`$ という関係があると、モデルの圏のあいだに忘却関手が誘導されます。
$`\quad U : \mrm{Model}({\mathscr{X}}) \to \mrm{Model}(\mathscr{Y}) \In {\bf CAT}`$
例えば、$`\text{Monoid} \preceq \text{PointedSet} \preceq \text{SingleSet}`$ である場合は、次の忘却関手があります。
$`\quad U : \mrm{Model}(\text{PointedSet}) \to \mrm{Model}(\text{SingleSet}) \In {\bf CAT}\\
\quad U : \mrm{Model}( \text{Monoid} ) \to \mrm{Model}(\text{PointedSet} ) \In {\bf CAT}
%`$
忘却関手は一律に $`U`$ で書いていますが、異なる2つの関手です。指標 SingleSet のモデルの圏は集合圏と同一視して、その他のモデルの圏は比較的よく使われる固有名詞を使って書けば：
$`\quad U : {\bf PtSet} \to {\bf Set} \In {\bf CAT}\\
\quad U : {\bf Mon} \to {\bf PtSet} \In {\bf CAT}
%`$
指標の $`\preceq`$-関係から誘導された忘却関手 $`U:\cat{D} \to\cat{C}`$ があるとき、次のような関手 $`E`$ を（その忘却関手の）増強関手〈enhancement functor〉、または単に増強〈enhancement〉と呼びます。
- $`E:\cat{I} \to \cat{D} \In {\bf CAT}`$
- $`\cat{I}`$ は $`\cat{C}`$ の部分圏
- $`E * U = \mrm{Id}_{\cat{I}}`$ （$`*`$ は関手の図式順結合）
増強（以前は追憶と呼んでいた）に関して詳しいことは以下の記事参照。
ここでは、増強の域圏を離散圏に限ります。つまり、$`\cat{I}`$ は単なる集合で、$`E`$ は次のような写像です。
- $`E: \cat{I} \to |\cat{D}| \In {\bf SET}`$
- $`\mrm{dom}(E) = \cat{I} \subseteq |\cat{C}|`$
- $`E ; U_\mrm{obj} = \mrm{id}_{\cat{I}}`$ （$`;`$ は写像の図式順結合、$`U_\mrm{obj}`$ は関手の対象パート）
特に $`\cat{C} = {\bf Set}`$ のケースを考えましょう。$`\cat{D} = \mrm{Model}(\mathscr{X})`$ とします。
- $`E: \cat{I} \to |\mrm{Model}(\mathscr{X})| \In {\bf SET}`$
- $`\mrm{dom}(E) = \cat{I} \subseteq |{\bf Set}|`$
- $`E ; U_\mrm{obj} = \mrm{id}_{\cat{I}}`$ （$`;`$ は写像の図式順結合、$`U_\mrm{obj}`$ は忘却関手の対象パート）
さらにもっと具体的な例として $`\text{Monoid} \preceq \text{SingleSet}`$ の場合を考えると、忘却関手は、
$`\quad U: {\bf Mon} \to {\bf Set} \In {\bf CAT}`$
増強は：
- $`E: \cat{I} \to |{\bf Mon}| \In {\bf SET}`$
- $`\mrm{dom}(E) = \cat{I} \subseteq |{\bf Set}|`$
- $`E ; U_\mrm{obj} = \mrm{id}_{\cat{I}}`$
この場合：
- $`\cat{I}`$ は集合〈型〉の集合である。
- $`E`$ は、$`\cat{I}`$ の要素である集合〈型〉に、指標 Monoid のモデルであるモノイドを対応付ける。
- $`X\in \cat{I}`$ に対して、$`U(E(X)) = X`$ である。
- つまり、型 $`X`$ に $`E`$ で対応付けられたモノイドの台集合は $`X`$ である。
プログラミング的に解釈すれば、増強は、型にモデル〈実装〉を対応付けます。そのモデル〈実装〉の台集合がもとの型になります。増強は、指標の実装状況を表します。
指標 $`\mathscr{X}`$ があって、そのなかに台集合〈underlying set | carrier〉の情報（例えば base）が含まれるとき、忘却関手 $`U:\mrm{Model}(\mathscr{X}) \to {\bf Set} \In {\bf CAT}`$ は自動的に作れます。しかし、増強 $`E:\cat{I} \to |\mrm{Model}(\mathscr{X})| \In {\bf SET}`$ が自動的に決まるわけではありません。
指標、増強、型〈集合〉を引数とする述語 $`\text{hasImplOfWrs}`$（◯◯ has implementation of ◯◯ with reference to ◯◯）を次のように定義します。
$`\For \mathscr{X} \in {\bf SignWithCarrier}\\
\For E \in \mrm{Enh}(\mathscr{X})\\
\For A \in |{\bf Set}|\\
\quad \text{hasImplOfWrs}(A, \mathscr{X}, E) :\Leftrightarrow A \in \mrm{dom}(E)
`$
ここで、
- $`{\bf SignWithCarrier}`$ は、何らかの方法（継承、
base、単一の型パラメータなど）で、台集合〈キャリア〉が指定された指標の集合 - $`\mrm{Enh}(\mathscr{X})`$ は、指標 $`\mathscr{X}`$ から自動的に作られた忘却関手に対する増強の集合
増強〈指標の実装状況〉 $`E`$ が暗黙に決まっているときは、この述語を $`\text{hasImplOf}(A, \mathscr{X})`$ と簡潔に書くことができます。が、増強〈指標の実装状況〉が暗黙化されている事が、話を分かりにくくさせている元凶です。
集合圏への忘却関手に対して増強を定義しましたが、指標のあいだに $`\mathscr{X} \preceq \mathscr{Y}`$ という関係があれば、増強を定義できます。次の忘却関手は自動的に決まります。
$`\quad U : \mrm{Model}({\mathscr{X}}) \to \mrm{Model}(\mathscr{Y}) \In {\bf CAT}`$
増強は、$`\mrm{Model}({\mathscr{Y}})`$ の全体で定義されているとは限らないので部分関手です。増強は、部分関手であって、$`U`$ のセクションになっているので部分セクション〈partial section〉です。つまり、
- 増強 ＝ 忘却関手の部分セクション
関手の部分セクション全体の集合を $`\mrm{ParSect}(-)`$ で表すと、増強の集合は次のようになります。
$`\quad \mrm{ParSect}(U : \mrm{Model}({\mathscr{X}}) \to \mrm{Model}(\mathscr{Y}))`$
[/補足]
型クラス述語
Haskellの型クラス定義で次のようなものがあります。
class Eq a where (==) :: a -> a -> Bool class Eq a => Ord a where (<=) :: a -> a -> Bool
計算可能な等値性〈equality〉述語を備えたEqクラスと、順序比較述語を備えたOrdクラスを定義しています。ここでの順序は全順序〈total order〉です。OrdクラスはEqクラスを“継承”しています。つまりOrdクラスの（型クラスを指標と考えての）モデルは、順序比較の不等号だけでなく等値性の等号も持っています。
Ordクラスの定義に現れる Eq a => の部分を、多くの人は次のように読んでいるのではないでしょうか？
- a が Eqクラスならば
- a は Eqクラスだと仮定して
- a が Eqクラスのインスタンスである場合に限って
Eq a が論理条件として解釈されています。その論理条件は、ひとつの型〈集合〉を引数とする述語です。
型クラス（その他、指標類似物）から自動的に導かれる、型を引数とする述語を型クラス述語〈type class predicate〉と呼ぶことにします。
Eq a => Ord a に出てくる Eq, Ord を型クラス述語とみなすと、全体として含意命題（「ならば」を含む命題）のように見えます。その印象はあながち間違いではないのですが、含意記号の向きが逆である命題が要求されます（Haskell の => が含意記号というわけでもないでしょうが）。前節の $`\text{hasImplOf}`$ を使って、次の論理式が書けます。
$`\quad \forall a\in |{\bf Set}|.( \text{hasImplOf}(a, \text{Ord}) \Imp \text{hasImplOf}(a, \text{Eq}) )`$
増強（型クラスの実装状況）まで明示的に書けば：
$`\quad \forall a\in |{\bf Set}|.\\
\qquad \text{hasImplOfWrt}(a, \text{Ord}, \text{OrdEnh}) \Imp \text{hasImplOfWrt}(a, \text{Eq}, \text{EqEnh})`$
ここで、$`\text{OrdEnh}, \text{EqEnh}`$ は型クラスの実装状況を表す増強です。
何らかの型クラス Foo の型クラス述語とは、$`\text{hasImplOfWrt}(-, \text{Foo}, \text{FooEnh})`$ のことです。増強（型クラスの実装状況）FooEnh は暗黙化されますが、増強なしで型クラス述語は定義できません。
さて、2つの型クラス述語から作った含意（論理的ならば）を含む命題の意味を説明しましょう。型クラス Eq, Ord を指標と解釈すると、次の忘却関手が作れます（同じ文字を使ってますが、別な忘却関手です）。
- $`U: \mrm{Model}(\text{Eq}) \to {\bf Set} \In {\bf CAT}`$
- $`U: \mrm{Model}(\text{Ord}) \to {\bf Set}\In {\bf CAT}`$
- $`U: \mrm{Model}(\text{Ord}) \to \mrm{Model}(\text{Eq})\In {\bf CAT}`$
型クラス Eq, Ord の実装状況に応じて、2つの増強写像が存在します。
- $`\text{EqEnh} : |{\bf Set}|\supseteq \cat{I} \to |\mrm{Model}(\text{Eq})| \In{\bf SET}`$
- $`\text{OrdEnh} : |{\bf Set}|\supseteq \cat{J} \to |\mrm{Model}(\text{Ord})| \In{\bf SET}`$
これらは、次の可換図式を満たす必要があります。
$`\require{AMScd}
\begin{CD}
|\mrm{Model}(\text{Ord})| @<{\text{OrdEnh}}<< \cat{J}\\
@V{U_\mrm{obj} }VV @VVV \\
|\mrm{Model}(\text{Eq})| @<{\text{EqEnh}}<< \cat{I}
\end{CD}\\
\:\\
\text{commutative in }{\bf SET}
`$
この可換図式内の $`\cat{J} \to \cat{I}`$ は型〈集合〉の集合のあいだの包含写像で、次を意味します。
$`\quad \cat{J} \subseteq \cat{I}`$
この包含関係が、型クラス実装の整合性条件として要求される含意命題です。念のため、命題〈論理式〉の同値変形を書けば：
$`\quad \cat{J} \subseteq \cat{I}\\
\equiv \forall a\in |{\bf Set}|.( a\in \cat{J} \Imp a \in \cat{I}) \\
\equiv \forall a\in |{\bf Set}|.( a\in \mrm{dom}(\text{OrdEnh}) \Imp a \in \mrm{dom}(\text{EqEnh}) ) \\
\equiv \forall a\in |{\bf Set}|.\\
\qquad \text{hasImplOfWrt}(a, \text{Ord}, \text{OrdEnh}) \Imp
\text{hasImplOfWrt}(a, \text{Eq}, \text{EqEnh})
`$
型クラス述語を、$`\text{hasOrdImpl}, \text{hasEqImpl}`$ のように短く書くとして、継承の向き、忘却関手の向き、含意の向きは次のようになります。
- $`\text{Ord} \preceq \text{Eq}`$ （派生型クラス $`\preceq`$ 基底型クラス）
- $`U: \mrm{Model}(\text{Ord}) \to \mrm{Model}(\text{Eq})`$ （域圏 $`\to`$ 余域圏）
- $`\text{hasOrdImpl}(a) \Imp \text{hasEqImpl}(a)`$ （前件 $`\Imp`$ 後件）
台集合（キャリアとも呼ぶ）の情報を含む指標をキャリア付き指標〈signature with carrier〉と呼ぶことにします。$`\mathscr{X}`$ がキャリア付き指標なら、自動的に忘却関手
$`\quad U_\mathscr{X} :\mrm{Model}(\mathscr{X}) \to {\bf Set} \In {\bf CAT}`$
が決まり、型クラス述語
$`\quad \text{hasImplOfWrt}(-, \mathscr{X}, E)`$
も決まります。ここで、$`E`$ はキャリア付き指標の忘却関手 $`U_\mathscr{X}`$ の増強です。
プログラミング言語が使う型（Sets-as-Types の型）がありとあらゆる集合を含むことはないので、$`{\bf T} \subseteq |{\bf Set}|`$ を型の集合とします。型クラス述語は、$`{\bf T}`$ 上の述語と考えましょう。つまり：
$`\quad \text{hasImplOfWrt}(-, \mathscr{X}, E) : {\bf T} \to \{\mrm{True},\mrm{False}\} \In {\bf Set}`$
ヒルベルトのイプシロン記号
ヒルベルトのイプシロン記号については過去にも書いてます（例えば、「イプシロン計算ってなんですかぁ？ こんなもんですよぉ」）が、改めて説明します。
$`X`$ を空でない集合として、$`A`$ は $`X`$ の部分集合とします（$`A = X`$ でもよい）。$`\varepsilon\,A`$ は、集合 $`A`$ から取り出した1個の要素を表します。誰が取り出すかというと、気まぐれな神様（あるいは気まぐれな悪魔）が、その場でテキトーに1個の要素を選ぶと思ってください。
集合 $`A`$ が、$`A = \{x\in X\mid P(x)\}`$ と内包的記法で書かれているとき、$`\varepsilon\, A`$ を次のように書きます。
$`\quad \varepsilon\, x\in X.P(x)`$
例えば、$`\varepsilon\, x\in {\bf R}.(x^2 = 2)`$ は $`\sqrt{2}`$ か $`-\sqrt{2}`$ のどちらかを意味します。
$`A`$ が空集合のときの $`\varepsilon\,A`$ は、次の考え方があります。
- $`X`$ 内のテキトーな要素を気まぐれに返す。（ヒルベルトのオリジナルの定義）
- 取り出すべき要素がないのだから未定義とする。
- $`A`$ が空のときは、そもそも $`\varepsilon\,A`$ は考えないことにする。
一番目の定義は一見奇妙ですが、論理的にはうまく働きます。が、気持ち悪かったら二番目／三番目のように考えてもかまいません。
イプシロン型
Haskell／Rust／Swift において、型クラス／トレイト／プロトコルと関係付けられて“存在型”と呼ばれている型は、論理の存在限量〈existential quantification〉との関係は薄く曖昧です。ありていに言えば、雰囲気が似てる程度でしょう。ヒルベルトのイプシロン記号を使えば、ハッキリした解釈を与えることができます。
「全称型／存在型： 代替案」において、carrier some Content という書き方をしました。これをヒルベルトのイプシロン記号により解釈してみます。
$`\mathscr{X}`$ をキャリア付き指標として、some はイプシロン記号、carrier は忘却関手として解釈してみれば、次のようになります。
$`\quad \text{carrier some } \mathscr{X}\\
= U_\mathscr{X}(\varepsilon\, |\mrm{Model}(\mathscr{X})|)
`$
これだと、膨大なモデルの集合から、テキトーなモデルを気まぐれに選んでそのキャリア〈台集合〉を取ることになります。意味的に妥当ですが、超越的過ぎます。
忘却関手 $`U_\mathscr{X}`$ の増強 $`E`$ が、$`{\bf T}`$ の部分集合で定義されていることを前提とすれば、次のような解釈ができます。
$`\quad \text{carrier some } \mathscr{X}\\
= \varepsilon\, t \in {\bf T}.\text{hasImplOfWrt}(t, \mathscr{X}, E)
`$
型クラス述語に対してイプシロン記号を作用させた形です。イプシロン記号はテキトーに要素を取り出しますが、取り出す範囲は次の集合に限定されます。
$`\quad \{t \in {\bf T} \mid \text{hasImplOfWrt}(t, \mathscr{X}, E) \}`$
現実には、$`E`$ の定義域は有限集合ですから、有限集合から取り出すに過ぎません。
型の集まり（またはモデルの集まり）からテキトーに選ぶことは、存在限量ではなくてイプシロン記号による選択です。存在型よりはイプシロン型〈epsilon type〉と呼ぶほうがふさわしいでしょう。
